diff options
Diffstat (limited to 'src/Specific/GF25519Reflective/Reified')
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Add.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryAdd.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryOpp.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarrySub.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Freeze.v | 18 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/GeModulus.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Mul.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Opp.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Pack.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/PreFreeze.v | 17 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Sub.v | 3 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Unpack.v | 3 | ||||
-rwxr-xr-x | src/Specific/GF25519Reflective/Reified/rebuild-reified.py | 7 |
13 files changed, 41 insertions, 31 deletions
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()) |