diff options
-rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 11 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Add.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryAdd.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarryOpp.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/CarrySub.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Freeze.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/GeModulus.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Mul.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Opp.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Pack.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Sub.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519Reflective/Reified/Unpack.v | 1 | ||||
-rwxr-xr-x | src/Specific/GF25519Reflective/Reified/rebuild-reified.py | 1 |
13 files changed, 23 insertions, 0 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 20e19392a..f847ddac0 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -157,7 +157,18 @@ 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 + | Tbase TZ => fun v => match v with + | overflow => false + | in_range _ _ => true + 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_check opW bounds + := (eq_refl true <: no_overflow (SmartVarfMap ZBounds_to_bounds_on (compute_bounds opW bounds)) = true) (only parsing). End PrettyPrinting. diff --git a/src/Specific/GF25519Reflective/Reified/Add.v b/src/Specific/GF25519Reflective/Reified/Add.v index 96fe51ab2..36357fcb7 100644 --- a/src/Specific/GF25519Reflective/Reified/Add.v +++ b/src/Specific/GF25519Reflective/Reified/Add.v @@ -8,3 +8,4 @@ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v index 8df627632..cc93a5bef 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v +++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v @@ -8,3 +8,4 @@ Definition rcarry_add_output_bounds := Eval vm_compute in compute_bounds rcarry_ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v index 79e6e29a1..130e55329 100644 --- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v +++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v @@ -8,3 +8,4 @@ Definition rcarry_opp_output_bounds := Eval vm_compute in compute_bounds rcarry_ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v index e7c2c53ab..b09960a18 100644 --- a/src/Specific/GF25519Reflective/Reified/CarrySub.v +++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v @@ -8,3 +8,4 @@ Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v index 72032bb36..4158a5277 100644 --- a/src/Specific/GF25519Reflective/Reified/Freeze.v +++ b/src/Specific/GF25519Reflective/Reified/Freeze.v @@ -8,3 +8,4 @@ Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW E 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 75ff2bfdc..776219f96 100644 --- a/src/Specific/GF25519Reflective/Reified/GeModulus.v +++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v @@ -8,3 +8,4 @@ Definition rge_modulus_output_bounds := Eval vm_compute in compute_bounds rge_mo 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v index f1b775754..1643a6610 100644 --- a/src/Specific/GF25519Reflective/Reified/Mul.v +++ b/src/Specific/GF25519Reflective/Reified/Mul.v @@ -8,3 +8,4 @@ Definition rmul_output_bounds := Eval vm_compute in compute_bounds rmulW ExprBin Local Open Scope string_scope. Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds). +(*Compute ("Mul overflows? ", sanity_check rmulW ExprBinOp_bounds).*) diff --git a/src/Specific/GF25519Reflective/Reified/Opp.v b/src/Specific/GF25519Reflective/Reified/Opp.v index c561f5bf0..907771b14 100644 --- a/src/Specific/GF25519Reflective/Reified/Opp.v +++ b/src/Specific/GF25519Reflective/Reified/Opp.v @@ -8,3 +8,4 @@ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v index 8e943649d..7f0f46494 100644 --- a/src/Specific/GF25519Reflective/Reified/Pack.v +++ b/src/Specific/GF25519Reflective/Reified/Pack.v @@ -8,3 +8,4 @@ Definition rpack_output_bounds := Eval vm_compute in compute_bounds rpackW ExprU Local Open Scope string_scope. Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds). +(*Compute ("Pack overflows? ", sanity_check rpackW ExprUnOpFEToWire_bounds).*) diff --git a/src/Specific/GF25519Reflective/Reified/Sub.v b/src/Specific/GF25519Reflective/Reified/Sub.v index 334d1db7e..9b684248d 100644 --- a/src/Specific/GF25519Reflective/Reified/Sub.v +++ b/src/Specific/GF25519Reflective/Reified/Sub.v @@ -8,3 +8,4 @@ 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).*) diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v index 7caa18c54..701115388 100644 --- a/src/Specific/GF25519Reflective/Reified/Unpack.v +++ b/src/Specific/GF25519Reflective/Reified/Unpack.v @@ -8,3 +8,4 @@ Definition runpack_output_bounds := Eval vm_compute in compute_bounds runpackW E Local Open Scope string_scope. Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds). +(*Compute ("Unpack overflows? ", sanity_check runpackW ExprUnOpWireToFE_bounds).*) diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py index e1c090105..992bc7a7e 100755 --- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py +++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py @@ -18,4 +18,5 @@ Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lnam 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).*) """ % locals()) |