diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-10 18:31:41 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
commit | 188c1cb99886853d452925ae513a44d3da6151dd (patch) | |
tree | 98617ce17df26ee3f5e314a6b85b92a94cdeec07 /src | |
parent | 20482796154100307af995bc8445ec6f674531d0 (diff) |
Freeze stubs
Diffstat (limited to 'src')
18 files changed, 129 insertions, 53 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 2d83b8dbd..f09b843f0 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -50,7 +50,7 @@ Local Arguments interp_radd / _ _. Local Arguments interp_rsub / _ _. Local Arguments interp_rmul / _ _. Local Arguments interp_ropp / _. -Local Arguments interp_rfreeze / _. +Local Arguments interp_rprefreeze / _. Local Arguments interp_rge_modulus / _. Local Arguments interp_rpack / _. Local Arguments interp_runpack / _. @@ -58,10 +58,11 @@ Definition addW (f g : fe25519W) : fe25519W := Eval simpl in interp_radd f g. Definition subW (f g : fe25519W) : fe25519W := Eval simpl in interp_rsub f g. Definition mulW (f g : fe25519W) : fe25519W := Eval simpl in interp_rmul f g. Definition oppW (f : fe25519W) : fe25519W := Eval simpl in interp_ropp f. -Definition freezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rfreeze f. +Definition prefreezeW (f : fe25519W) : fe25519W := Eval simpl in interp_rprefreeze f. Definition ge_modulusW (f : fe25519W) : word64 := Eval simpl in interp_rge_modulus f. Definition packW (f : fe25519W) : wire_digitsW := Eval simpl in interp_rpack f. Definition unpackW (f : wire_digitsW) : fe25519W := Eval simpl in interp_runpack f. +Definition freezeW (f : fe25519W) : fe25519W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f). Local Transparent Let_In. Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW chain [f]. @@ -81,14 +82,22 @@ Lemma mulW_correct_and_bounded : ibinop_correct_and_bounded mulW mul. Proof. port_correct_and_bounded interp_rmul_correct mulW interp_rmul rmul_correct_and_bounded. Qed. Lemma oppW_correct_and_bounded : iunop_correct_and_bounded oppW carry_opp. Proof. port_correct_and_bounded interp_ropp_correct oppW interp_ropp ropp_correct_and_bounded. Qed. -Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze. -Proof. port_correct_and_bounded interp_rfreeze_correct freezeW interp_rfreeze rfreeze_correct_and_bounded. Qed. +Lemma prefreezeW_correct_and_bounded : iunop_correct_and_bounded prefreezeW prefreeze. +Proof. port_correct_and_bounded interp_rprefreeze_correct prefreezeW interp_rprefreeze rprefreeze_correct_and_bounded. Qed. Lemma ge_modulusW_correct : iunop_FEToZ_correct ge_modulusW ge_modulus. Proof. port_correct_and_bounded interp_rge_modulus_correct ge_modulusW interp_rge_modulus rge_modulus_correct_and_bounded. Qed. Lemma packW_correct_and_bounded : iunop_FEToWire_correct_and_bounded packW pack. Proof. port_correct_and_bounded interp_rpack_correct packW interp_rpack rpack_correct_and_bounded. Qed. Lemma unpackW_correct_and_bounded : iunop_WireToFE_correct_and_bounded unpackW unpack. Proof. port_correct_and_bounded interp_runpack_correct unpackW interp_runpack runpack_correct_and_bounded. Qed. +Lemma freezeW_correct_and_bounded : iunop_correct_and_bounded freezeW freeze. +Proof. + intros f H; rewrite <- freeze_prepost_freeze. + change (freezeW f) with (postfreezeW (prefreezeW f)). + destruct (prefreezeW_correct_and_bounded f H) as [H0 H1]. + destruct (postfreezeW_correct_and_bounded _ H1) as [H0' H1']. + rewrite H1', H0', H0; split; reflexivity. +Qed. Lemma powW_correct_and_bounded chain : iunop_correct_and_bounded (fun x => powW x chain) (fun x => pow x chain). Proof. diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index f9ee444dc..4f0c9b4de 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -689,3 +689,51 @@ Notation iunop_WireToFE_correct_and_bounded irop op wire_digits_is_bounded (wire_digitsWToZ x) = true -> fe25519WToZ (irop x) = op (wire_digitsWToZ x) /\ is_bounded (fe25519WToZ (irop x)) = true) (only parsing). + +(** TODO(andreser): Remove me in favor of a GF25519.v definition *) +Definition prefreeze := +fun '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) => +dlet a := f9 in +dlet a0 := (Z.shiftr a 26 + f8)%Z in +dlet a1 := (Z.shiftr a0 25 + f7)%Z in +dlet a2 := (Z.shiftr a1 26 + f6)%Z in +dlet a3 := (Z.shiftr a2 25 + f5)%Z in +dlet a4 := (Z.shiftr a3 26 + f4)%Z in +dlet a5 := (Z.shiftr a4 25 + f3)%Z in +dlet a6 := (Z.shiftr a5 26 + f2)%Z in +dlet a7 := (Z.shiftr a6 25 + f1)%Z in +dlet a8 := (Z.shiftr a7 26 + f0)%Z in +dlet a9 := (19 * Z.shiftr a8 25 + Z.land a 67108863)%Z in +dlet a10 := (Z.shiftr a9 26 + Z.land a0 33554431)%Z in +dlet a11 := (Z.shiftr a10 25 + Z.land a1 67108863)%Z in +dlet a12 := (Z.shiftr a11 26 + Z.land a2 33554431)%Z in +dlet a13 := (Z.shiftr a12 25 + Z.land a3 67108863)%Z in +dlet a14 := (Z.shiftr a13 26 + Z.land a4 33554431)%Z in +dlet a15 := (Z.shiftr a14 25 + Z.land a5 67108863)%Z in +dlet a16 := (Z.shiftr a15 26 + Z.land a6 33554431)%Z in +dlet a17 := (Z.shiftr a16 25 + Z.land a7 67108863)%Z in +dlet a18 := (Z.shiftr a17 26 + Z.land a8 33554431)%Z in +dlet a19 := (19 * Z.shiftr a18 25 + Z.land a9 67108863)%Z in +dlet a20 := (Z.shiftr a19 26 + Z.land a10 33554431)%Z in +dlet a21 := (Z.shiftr a20 25 + Z.land a11 67108863)%Z in +dlet a22 := (Z.shiftr a21 26 + Z.land a12 33554431)%Z in +dlet a23 := (Z.shiftr a22 25 + Z.land a13 67108863)%Z in +dlet a24 := (Z.shiftr a23 26 + Z.land a14 33554431)%Z in +dlet a25 := (Z.shiftr a24 25 + Z.land a15 67108863)%Z in +dlet a26 := (Z.shiftr a25 26 + Z.land a16 33554431)%Z in +dlet a27 := (Z.shiftr a26 25 + Z.land a17 67108863)%Z in +dlet a28 := (Z.shiftr a27 26 + Z.land a18 33554431)%Z in + +((Z.land a28 33554431 )%Z, (Z.land a27 67108863 )%Z, +(Z.land a26 33554431 )%Z, (Z.land a25 67108863 )%Z, +(Z.land a24 33554431 )%Z, (Z.land a23 67108863 )%Z, +(Z.land a22 33554431 )%Z, (Z.land a21 67108863 )%Z, +(Z.land a20 33554431 )%Z, ( Z.land a19 67108863 )%Z). + +Axiom postfreeze : GF25519.fe25519 -> GF25519.fe25519. +Axiom freeze_prepost_freeze : forall x, postfreeze (prefreeze x) = GF25519.freeze x. +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Definition postfreezeW : fe25519W -> fe25519W. +Proof. admit. Defined. +Axiom postfreezeW_correct_and_bounded : iunop_correct_and_bounded postfreezeW postfreeze. diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v index 4405eefa9..5e306d61d 100644 --- a/src/Specific/GF25519Reflective.v +++ b/src/Specific/GF25519Reflective.v @@ -36,7 +36,7 @@ Definition radd : ExprBinOp := Eval vm_compute in rcarry_addW. Definition rsub : ExprBinOp := Eval vm_compute in rcarry_subW. Definition rmul : ExprBinOp := Eval vm_compute in rmulW. Definition ropp : ExprUnOp := Eval vm_compute in rcarry_oppW. -Definition rfreeze : ExprUnOp := Eval vm_compute in rfreezeW. +Definition rprefreeze : ExprUnOp := Eval vm_compute in rprefreezeW. Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW. Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW. Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW. @@ -48,7 +48,7 @@ Declare Reduction asm_interp := cbv beta iota delta [id interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE - radd rsub rmul ropp rfreeze rge_modulus rpack runpack + radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW Word64.interp_op Word64.interp_base_type Z.interp_op Z.interp_base_type @@ -59,7 +59,7 @@ Ltac asm_interp := cbv beta iota delta [id interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE - radd rsub rmul ropp rfreeze rge_modulus rpack runpack + radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW Word64.interp_op Word64.interp_base_type Z.interp_op Z.interp_base_type @@ -84,10 +84,10 @@ Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25 := Eval asm_interp in interp_uexpr (rword64ize ropp). (*Print interp_ropp.*) Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl. -Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W - := Eval asm_interp in interp_uexpr (rword64ize rfreeze). -(*Print interp_rfreeze.*) -Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl. +Definition interp_rprefreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := Eval asm_interp in interp_uexpr (rword64ize rprefreeze). +(*Print interp_rprefreeze.*) +Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl. Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64 := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus). @@ -109,8 +109,8 @@ Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. Proof. exact rmulW_correct_and_bounded. Qed. Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. Proof. exact rcarry_oppW_correct_and_bounded. Qed. -Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. -Proof. exact rfreezeW_correct_and_bounded. Qed. +Lemma rprefreeze_correct_and_bounded : unop_correct_and_bounded rprefreeze prefreeze. +Proof. exact rprefreezeW_correct_and_bounded. Qed. Lemma rge_modulus_correct_and_bounded : unop_FEToZ_correct rge_modulus ge_modulus. Proof. exact rge_modulusW_correct_and_bounded. Qed. Lemma rpack_correct_and_bounded : unop_FEToWire_correct_and_bounded rpack pack. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 3d448f97c..c302926d6 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -1,7 +1,7 @@ Require Export Coq.ZArith.ZArith. Require Export Coq.Strings.String. Require Export Crypto.Specific.GF25519. -Require Import Crypto.Specific.GF25519BoundedCommon. +Require Export Crypto.Specific.GF25519BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Z.Interpretations. @@ -395,7 +395,11 @@ Notation compute_bounds opW bounds Module Export PrettyPrinting. - Inductive bounds_on := overflow | in_range (lower upper : Z). + Section bounds_not_set. + Let T := let T := Type in let enforce := Set : T in T. + Inductive bounds_on : T := overflow | in_range (lower upper : Z). + End bounds_not_set. + Inductive result := yes | no. Definition ZBounds_to_bounds_on := fun t : base_type @@ -408,18 +412,23 @@ Module Export PrettyPrinting. end end. - Fixpoint no_overflow {t} : interp_flat_type (fun t => match t with TZ => bounds_on end) t -> bool - := match t return interp_flat_type (fun t => match t with TZ => bounds_on end) t -> bool with + Fixpoint does_it_overflow {t} : interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result + := match t return interp_flat_type (fun t => match t with TZ => bounds_on end) t -> result with | Tbase TZ => fun v => match v with - | overflow => false - | in_range _ _ => true + | overflow => yes + | in_range _ _ => no + end + | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with + | no, no => no + | _, _ => yes end - | Prod x y => fun v => andb (@no_overflow _ (fst v)) (@no_overflow _ (snd v)) end. (** This gives a slightly easier to read version of the bounds *) Notation compute_bounds_for_display opW bounds := (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) (only parsing). + Notation sanity_compute opW bounds + := (does_it_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds))) (only parsing). Notation sanity_check opW bounds - := (eq_refl true <: no_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) = true) (only parsing). + := (eq_refl (sanity_compute opW bounds) <: no = no) (only parsing). End PrettyPrinting. diff --git a/src/Specific/GF25519Reflective/Reified.v b/src/Specific/GF25519Reflective/Reified.v index 98edc1282..aa50ad33f 100644 --- a/src/Specific/GF25519Reflective/Reified.v +++ b/src/Specific/GF25519Reflective/Reified.v @@ -7,7 +7,7 @@ Require Export Crypto.Specific.GF25519Reflective.Reified.CarrySub. Require Export Crypto.Specific.GF25519Reflective.Reified.Mul. Require Export Crypto.Specific.GF25519Reflective.Reified.Opp. Require Export Crypto.Specific.GF25519Reflective.Reified.CarryOpp. -Require Export Crypto.Specific.GF25519Reflective.Reified.Freeze. +Require Export Crypto.Specific.GF25519Reflective.Reified.PreFreeze. Require Export Crypto.Specific.GF25519Reflective.Reified.GeModulus. Require Export Crypto.Specific.GF25519Reflective.Reified.Pack. Require Export Crypto.Specific.GF25519Reflective.Reified.Unpack. diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v index ae3a6a4c6..f2700aca7 100644 --- a/src/Specific/GF25519Reflective/Reified/Add.v +++ b/src/Specific/GF25519Reflective/Reified/Add.v @@ -8,4 +8,5 @@ Definition radd_output_bounds := Eval vm_compute in compute_bounds raddW ExprBin Local Open Scope string_scope. Compute ("Add", compute_bounds_for_display raddW ExprBinOp_bounds). -(*Compute ("Add overflows? ", sanity_check raddW ExprBinOp_bounds).*) +Compute ("Add overflows? ", sanity_compute raddW ExprBinOp_bounds). +Compute ("Add overflows (error if it does)? ", sanity_check raddW ExprBinOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v index 3051121c0..6e05303e5 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v +++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v @@ -13,4 +13,5 @@ Program Definition rcarry_addW_correct_and_bounded Local Open Scope string_scope. Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds). -(*Compute ("Carry_Add overflows? ", sanity_check rcarry_addW ExprBinOp_bounds).*) +Compute ("Carry_Add overflows? ", sanity_compute rcarry_addW ExprBinOp_bounds). +Compute ("Carry_Add overflows (error if it does)? ", sanity_check rcarry_addW ExprBinOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v index 571b9db97..52814dca9 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v +++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v @@ -13,4 +13,5 @@ Program Definition rcarry_oppW_correct_and_bounded Local Open Scope string_scope. Compute ("Carry_Opp", compute_bounds_for_display rcarry_oppW ExprUnOp_bounds). -(*Compute ("Carry_Opp overflows? ", sanity_check rcarry_oppW ExprUnOp_bounds).*) +Compute ("Carry_Opp overflows? ", sanity_compute rcarry_oppW ExprUnOp_bounds). +Compute ("Carry_Opp overflows (error if it does)? ", sanity_check rcarry_oppW ExprUnOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v index fda466861..946a4ed67 100644 --- a/src/Specific/GF25519Reflective/Reified/CarrySub.v +++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v @@ -13,4 +13,5 @@ Program Definition rcarry_subW_correct_and_bounded Local Open Scope string_scope. Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds). -(*Compute ("Carry_Sub overflows? ", sanity_check rcarry_subW ExprBinOp_bounds).*) +Compute ("Carry_Sub overflows? ", sanity_compute rcarry_subW ExprBinOp_bounds). +Compute ("Carry_Sub overflows (error if it does)? ", sanity_check rcarry_subW ExprBinOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v deleted file mode 100644 index 0dcea29e4..000000000 --- a/src/Specific/GF25519Reflective/Reified/Freeze.v +++ /dev/null @@ -1,18 +0,0 @@ -Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. - -Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined. -Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig. -Lemma rfreezeW_correct_and_bounded_gen : correct_and_bounded_genT rfreezeW rfreezeZ_sig. -Proof. rexpr_correct. Qed. -Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW ExprUnOp_bounds. -Local Obligation Tactic := intros; vm_compute; constructor. -Axiom proof_admitted : False. -(** XXX TODO: Fix bounds analysis on freeze *) -Definition rfreezeW_correct_and_bounded - := ExprUnOp_correct_and_bounded - rfreezeW freeze rfreezeZ_sig rfreezeW_correct_and_bounded_gen - match proof_admitted with end match proof_admitted with end. - -Local Open Scope string_scope. -Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds). -(*Compute ("Freeze overflows? ", sanity_check rfreezeW ExprUnOp_bounds).*) diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v index 69eb3ba41..8bbcf0dc4 100644 --- a/src/Specific/GF25519Reflective/Reified/GeModulus.v +++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v @@ -13,4 +13,5 @@ Program Definition rge_modulusW_correct_and_bounded Local Open Scope string_scope. Compute ("Ge_Modulus", compute_bounds_for_display rge_modulusW ExprUnOpFEToZ_bounds). -(*Compute ("Ge_Modulus overflows? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds).*) +Compute ("Ge_Modulus overflows? ", sanity_compute rge_modulusW ExprUnOpFEToZ_bounds). +Compute ("Ge_Modulus overflows (error if it does)? ", sanity_check rge_modulusW ExprUnOpFEToZ_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v index 0c298134d..0388c626a 100644 --- a/src/Specific/GF25519Reflective/Reified/Mul.v +++ b/src/Specific/GF25519Reflective/Reified/Mul.v @@ -13,4 +13,5 @@ Program Definition rmulW_correct_and_bounded Local Open Scope string_scope. Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds). -(*Compute ("Mul overflows? ", sanity_check rmulW ExprBinOp_bounds).*) +Compute ("Mul overflows? ", sanity_compute rmulW ExprBinOp_bounds). +Compute ("Mul overflows (error if it does)? ", sanity_check rmulW ExprBinOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v index 58f2a6fbb..36a0b907e 100644 --- a/src/Specific/GF25519Reflective/Reified/Opp.v +++ b/src/Specific/GF25519Reflective/Reified/Opp.v @@ -8,4 +8,5 @@ Definition ropp_output_bounds := Eval vm_compute in compute_bounds roppW ExprUnO Local Open Scope string_scope. Compute ("Opp", compute_bounds_for_display roppW ExprUnOp_bounds). -(*Compute ("Opp overflows? ", sanity_check roppW ExprUnOp_bounds).*) +Compute ("Opp overflows? ", sanity_compute roppW ExprUnOp_bounds). +Compute ("Opp overflows (error if it does)? ", sanity_check roppW ExprUnOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v index cd85d0cd7..9645cf24c 100644 --- a/src/Specific/GF25519Reflective/Reified/Pack.v +++ b/src/Specific/GF25519Reflective/Reified/Pack.v @@ -13,4 +13,5 @@ Program Definition rpackW_correct_and_bounded Local Open Scope string_scope. Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds). -(*Compute ("Pack overflows? ", sanity_check rpackW ExprUnOpFEToWire_bounds).*) +Compute ("Pack overflows? ", sanity_compute rpackW ExprUnOpFEToWire_bounds). +Compute ("Pack overflows (error if it does)? ", sanity_check rpackW ExprUnOpFEToWire_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/PreFreeze.v b/src/Specific/GF25519Reflective/Reified/PreFreeze.v new file mode 100644 index 000000000..6b3bce924 --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/PreFreeze.v @@ -0,0 +1,17 @@ +Require Import Crypto.Specific.GF25519Reflective.CommonUnOp. + +Definition rprefreezeZ_sig : rexpr_unop_sig prefreeze. Proof. reify_sig. Defined. +Definition rprefreezeW := Eval vm_compute in rword_of_Z rprefreezeZ_sig. +Lemma rprefreezeW_correct_and_bounded_gen : correct_and_bounded_genT rprefreezeW rprefreezeZ_sig. +Proof. rexpr_correct. Qed. +Definition rprefreeze_output_bounds := Eval vm_compute in compute_bounds rprefreezeW ExprUnOp_bounds. +Local Obligation Tactic := intros; vm_compute; constructor. +Program Definition rprefreezeW_correct_and_bounded + := ExprUnOp_correct_and_bounded + rprefreezeW prefreeze rprefreezeZ_sig rprefreezeW_correct_and_bounded_gen + _ _. + +Local Open Scope string_scope. +Compute ("PreFreeze", compute_bounds_for_display rprefreezeW ExprUnOp_bounds). +Compute ("PreFreeze overflows? ", sanity_compute rprefreezeW ExprUnOp_bounds). +Compute ("PreFreeze overflows (error if it does)? ", sanity_check rprefreezeW ExprUnOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v index 03356cd50..aae3af64b 100644 --- a/src/Specific/GF25519Reflective/Reified/Sub.v +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -8,4 +8,5 @@ Definition rsub_output_bounds := Eval vm_compute in compute_bounds rsubW ExprBin Local Open Scope string_scope. Compute ("Sub", compute_bounds_for_display rsubW ExprBinOp_bounds). -(*Compute ("Sub overflows? ", sanity_check rsubW ExprBinOp_bounds).*) +Compute ("Sub overflows? ", sanity_compute rsubW ExprBinOp_bounds). +Compute ("Sub overflows (error if it does)? ", sanity_check rsubW ExprBinOp_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v index a96f87d96..f8ab40383 100644 --- a/src/Specific/GF25519Reflective/Reified/Unpack.v +++ b/src/Specific/GF25519Reflective/Reified/Unpack.v @@ -13,4 +13,5 @@ Program Definition runpackW_correct_and_bounded Local Open Scope string_scope. Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds). -(*Compute ("Unpack overflows? ", sanity_check runpackW ExprUnOpWireToFE_bounds).*) +Compute ("Unpack overflows? ", sanity_compute runpackW ExprUnOpWireToFE_bounds). +Compute ("Unpack overflows (error if it does)? ", sanity_check runpackW ExprUnOpWireToFE_bounds). diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py index 404afc1ea..8b0da4c35 100755 --- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py +++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py @@ -2,13 +2,13 @@ from __future__ import with_statement for name, opkind in ([(name, 'BinOp') for name in ('Add', 'Carry_Add', 'Sub', 'Carry_Sub', 'Mul')] - + [(name, 'UnOp') for name in ('Opp', 'Carry_Opp', 'Freeze')] + + [(name, 'UnOp') for name in ('Opp', 'Carry_Opp', 'PreFreeze')] + [('Ge_Modulus', 'UnOp_FEToZ'), ('Pack', 'UnOp_FEToWire'), ('Unpack', 'UnOp_WireToFE')]): lname = name.lower() lopkind = opkind.replace('UnOp', 'unop').replace('BinOp', 'binop') uopkind = opkind.replace('_', '') extra = '' - if name in ('Carry_Add', 'Carry_Sub', 'Mul', 'Carry_Opp', 'Pack', 'Unpack', 'Ge_Modulus'): + if name in ('Carry_Add', 'Carry_Sub', 'Mul', 'Carry_Opp', 'Pack', 'Unpack', 'Ge_Modulus', 'PreFreeze'): extra = r"""Local Obligation Tactic := intros; vm_compute; constructor. Program Definition r%(lname)sW_correct_and_bounded := Expr%(uopkind)s_correct_and_bounded @@ -35,5 +35,6 @@ Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lnam %(extra)s Local Open Scope string_scope. Compute ("%(name)s", compute_bounds_for_display r%(lname)sW Expr%(uopkind)s_bounds). -(*Compute ("%(name)s overflows? ", sanity_check r%(lname)sW Expr%(uopkind)s_bounds).*) +Compute ("%(name)s overflows? ", sanity_compute r%(lname)sW Expr%(uopkind)s_bounds). +Compute ("%(name)s overflows (error if it does)? ", sanity_check r%(lname)sW Expr%(uopkind)s_bounds). """ % locals()) |