aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Specific/GF25519Reflective/Common.v43
-rw-r--r--src/Specific/GF25519Reflective/Reified/CarryAdd.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/CarryOpp.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/CarrySub.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/Freeze.v7
-rw-r--r--src/Specific/GF25519Reflective/Reified/GeModulus.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/Mul.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/Pack.v5
-rw-r--r--src/Specific/GF25519Reflective/Reified/Unpack.v5
-rwxr-xr-xsrc/Specific/GF25519Reflective/Reified/rebuild-reified.py19
10 files changed, 88 insertions, 16 deletions
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index e0c28fe77..24d114f96 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -310,10 +310,13 @@ Local Opaque Interp.
Lemma ExprBinOp_correct_and_bounded
ropW op (ropZ_sig : rexpr_binop_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
- (H0 : forall x y
- (Hx : is_bounded (fe25519WToZ x) = true)
- (Hy : is_bounded (fe25519WToZ y) = true),
- let args := binop_args_to_bounded (x, y) Hx Hy in
+ (H0 : forall xy
+ (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
+ (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
+ /\ is_bounded (fe25519WToZ (snd xy)) = true),
+ let Hx := let (Hx, Hy) := Hxy in Hx in
+ let Hy := let (Hx, Hy) := Hxy in Hy in
+ let args := binop_args_to_bounded xy Hx Hy in
match LiftOption.of'
(ApplyInterpedAll (Interp (@BoundedWord64.interp_op) (MapInterp BoundedWord64.of_word64 ropW))
(LiftOption.to' (Some args)))
@@ -321,10 +324,13 @@ Lemma ExprBinOp_correct_and_bounded
| Some _ => True
| None => False
end)
- (H1 : forall x y
- (Hx : is_bounded (fe25519WToZ x) = true)
- (Hy : is_bounded (fe25519WToZ y) = true),
- let args := binop_args_to_bounded (x, y) Hx Hy in
+ (H1 : forall xy
+ (xy := (eta_fe25519W (fst xy), eta_fe25519W (snd xy)))
+ (Hxy : is_bounded (fe25519WToZ (fst xy)) = true
+ /\ is_bounded (fe25519WToZ (snd xy)) = true),
+ let Hx := let (Hx, Hy) := Hxy in Hx in
+ let Hy := let (Hx, Hy) := Hxy in Hy in
+ let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy in
let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.to_bounds') args in
match LiftOption.of'
(ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_word64 ropW)) (LiftOption.to' (Some x')))
@@ -336,18 +342,18 @@ Lemma ExprBinOp_correct_and_bounded
Proof.
intros x y Hx Hy.
pose x as x'; pose y as y'.
- specialize (H0 x' y' Hx Hy).
- specialize (H1 x' y' Hx Hy).
hnf in x, y; destruct_head' prod.
+ specialize (H0 (x', y') (conj Hx Hy)).
+ specialize (H1 (x', y') (conj Hx Hy)).
let args := constr:(binop_args_to_bounded (x', y') Hx Hy) in
t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
Qed.
-
Lemma ExprUnOp_correct_and_bounded
ropW op (ropZ_sig : rexpr_unop_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
(H0 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
match LiftOption.of'
@@ -358,6 +364,7 @@ Lemma ExprUnOp_correct_and_bounded
| None => False
end)
(H1 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.to_bounds') args in
@@ -371,9 +378,9 @@ Lemma ExprUnOp_correct_and_bounded
Proof.
intros x Hx.
pose x as x'.
+ hnf in x; destruct_head' prod.
specialize (H0 x' Hx).
specialize (H1 x' Hx).
- hnf in x; destruct_head' prod.
let args := constr:(unop_args_to_bounded x' Hx) in
t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
Qed.
@@ -382,6 +389,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
ropW op (ropZ_sig : rexpr_unop_FEToWire_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
(H0 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
match LiftOption.of'
@@ -392,6 +400,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
| None => False
end)
(H1 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.to_bounds') args in
@@ -405,9 +414,9 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
Proof.
intros x Hx.
pose x as x'.
+ hnf in x; destruct_head' prod.
specialize (H0 x' Hx).
specialize (H1 x' Hx).
- hnf in x; destruct_head' prod.
let args := constr:(unop_args_to_bounded x' Hx) in
t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
Qed.
@@ -416,6 +425,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
ropW op (ropZ_sig : rexpr_unop_WireToFE_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
(H0 : forall x
+ (x := eta_wire_digitsW x)
(Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
let args := unopWireToFE_args_to_bounded x Hx in
match LiftOption.of'
@@ -426,6 +436,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
| None => False
end)
(H1 : forall x
+ (x := eta_wire_digitsW x)
(Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
let args := unopWireToFE_args_to_bounded x Hx in
let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.to_bounds') args in
@@ -439,9 +450,9 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
Proof.
intros x Hx.
pose x as x'.
+ hnf in x; destruct_head' prod.
specialize (H0 x' Hx).
specialize (H1 x' Hx).
- hnf in x; destruct_head' prod.
let args := constr:(unopWireToFE_args_to_bounded x' Hx) in
t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
Qed.
@@ -450,6 +461,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
ropW op (ropZ_sig : rexpr_unop_FEToZ_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
(H0 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
match LiftOption.of'
@@ -460,6 +472,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
| None => False
end)
(H1 : forall x
+ (x := eta_fe25519W x)
(Hx : is_bounded (fe25519WToZ x) = true),
let args := unop_args_to_bounded x Hx in
let x' := SmartVarfMap (fun _ : base_type => BoundedWord64.to_bounds') args in
@@ -473,9 +486,9 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
Proof.
intros x Hx.
pose x as x'.
+ hnf in x; destruct_head' prod.
specialize (H0 x' Hx).
specialize (H1 x' Hx).
- hnf in x; destruct_head' prod.
let args := constr:(unop_args_to_bounded x' Hx) in
t_correct_and_bounded ropZ_sig Hbounds H0 H1 args.
Qed.
diff --git a/src/Specific/GF25519Reflective/Reified/CarryAdd.v b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
index cc93a5bef..0ff563a8c 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryAdd.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryAdd.v
@@ -5,6 +5,11 @@ Definition rcarry_addW := Eval vm_compute in rword_of_Z rcarry_addZ_sig.
Lemma rcarry_addW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_addW rcarry_addZ_sig.
Proof. rexpr_correct. Qed.
Definition rcarry_add_output_bounds := Eval vm_compute in compute_bounds rcarry_addW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_addW_correct_and_bounded
+ := ExprBinOp_correct_and_bounded
+ rcarry_addW carry_add rcarry_addZ_sig rcarry_addW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Carry_Add", compute_bounds_for_display rcarry_addW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/CarryOpp.v b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
index 130e55329..4c21fbeb8 100644
--- a/src/Specific/GF25519Reflective/Reified/CarryOpp.v
+++ b/src/Specific/GF25519Reflective/Reified/CarryOpp.v
@@ -5,6 +5,11 @@ Definition rcarry_oppW := Eval vm_compute in rword_of_Z rcarry_oppZ_sig.
Lemma rcarry_oppW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_oppW rcarry_oppZ_sig.
Proof. rexpr_correct. Qed.
Definition rcarry_opp_output_bounds := Eval vm_compute in compute_bounds rcarry_oppW ExprUnOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_oppW_correct_and_bounded
+ := ExprUnOp_correct_and_bounded
+ rcarry_oppW carry_opp rcarry_oppZ_sig rcarry_oppW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Carry_Opp", compute_bounds_for_display rcarry_oppW ExprUnOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/CarrySub.v b/src/Specific/GF25519Reflective/Reified/CarrySub.v
index b09960a18..3acfb1f45 100644
--- a/src/Specific/GF25519Reflective/Reified/CarrySub.v
+++ b/src/Specific/GF25519Reflective/Reified/CarrySub.v
@@ -5,6 +5,11 @@ Definition rcarry_subW := Eval vm_compute in rword_of_Z rcarry_subZ_sig.
Lemma rcarry_subW_correct_and_bounded_gen : correct_and_bounded_genT rcarry_subW rcarry_subZ_sig.
Proof. rexpr_correct. Qed.
Definition rcarry_sub_output_bounds := Eval vm_compute in compute_bounds rcarry_subW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rcarry_subW_correct_and_bounded
+ := ExprBinOp_correct_and_bounded
+ rcarry_subW carry_sub rcarry_subZ_sig rcarry_subW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Carry_Sub", compute_bounds_for_display rcarry_subW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Freeze.v b/src/Specific/GF25519Reflective/Reified/Freeze.v
index 4158a5277..47cc290b3 100644
--- a/src/Specific/GF25519Reflective/Reified/Freeze.v
+++ b/src/Specific/GF25519Reflective/Reified/Freeze.v
@@ -5,6 +5,13 @@ 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 admit : forall {T}, T.
+(** 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
+ admit admit.
Local Open Scope string_scope.
Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/GeModulus.v b/src/Specific/GF25519Reflective/Reified/GeModulus.v
index 776219f96..73ee6904a 100644
--- a/src/Specific/GF25519Reflective/Reified/GeModulus.v
+++ b/src/Specific/GF25519Reflective/Reified/GeModulus.v
@@ -5,6 +5,11 @@ Definition rge_modulusW := Eval vm_compute in rword_of_Z rge_modulusZ_sig.
Lemma rge_modulusW_correct_and_bounded_gen : correct_and_bounded_genT rge_modulusW rge_modulusZ_sig.
Proof. rexpr_correct. Qed.
Definition rge_modulus_output_bounds := Eval vm_compute in compute_bounds rge_modulusW ExprUnOpFEToZ_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rge_modulusW_correct_and_bounded
+ := ExprUnOpFEToZ_correct_and_bounded
+ rge_modulusW ge_modulus rge_modulusZ_sig rge_modulusW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Ge_Modulus", compute_bounds_for_display rge_modulusW ExprUnOpFEToZ_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Mul.v b/src/Specific/GF25519Reflective/Reified/Mul.v
index 1643a6610..a206f02a1 100644
--- a/src/Specific/GF25519Reflective/Reified/Mul.v
+++ b/src/Specific/GF25519Reflective/Reified/Mul.v
@@ -5,6 +5,11 @@ Definition rmulW := Eval vm_compute in rword_of_Z rmulZ_sig.
Lemma rmulW_correct_and_bounded_gen : correct_and_bounded_genT rmulW rmulZ_sig.
Proof. rexpr_correct. Qed.
Definition rmul_output_bounds := Eval vm_compute in compute_bounds rmulW ExprBinOp_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rmulW_correct_and_bounded
+ := ExprBinOp_correct_and_bounded
+ rmulW mul rmulZ_sig rmulW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Mul", compute_bounds_for_display rmulW ExprBinOp_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Pack.v b/src/Specific/GF25519Reflective/Reified/Pack.v
index 7f0f46494..a7cf4fc13 100644
--- a/src/Specific/GF25519Reflective/Reified/Pack.v
+++ b/src/Specific/GF25519Reflective/Reified/Pack.v
@@ -5,6 +5,11 @@ Definition rpackW := Eval vm_compute in rword_of_Z rpackZ_sig.
Lemma rpackW_correct_and_bounded_gen : correct_and_bounded_genT rpackW rpackZ_sig.
Proof. rexpr_correct. Qed.
Definition rpack_output_bounds := Eval vm_compute in compute_bounds rpackW ExprUnOpFEToWire_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition rpackW_correct_and_bounded
+ := ExprUnOpFEToWire_correct_and_bounded
+ rpackW pack rpackZ_sig rpackW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Pack", compute_bounds_for_display rpackW ExprUnOpFEToWire_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/Unpack.v b/src/Specific/GF25519Reflective/Reified/Unpack.v
index 701115388..027eedf39 100644
--- a/src/Specific/GF25519Reflective/Reified/Unpack.v
+++ b/src/Specific/GF25519Reflective/Reified/Unpack.v
@@ -5,6 +5,11 @@ Definition runpackW := Eval vm_compute in rword_of_Z runpackZ_sig.
Lemma runpackW_correct_and_bounded_gen : correct_and_bounded_genT runpackW runpackZ_sig.
Proof. rexpr_correct. Qed.
Definition runpack_output_bounds := Eval vm_compute in compute_bounds runpackW ExprUnOpWireToFE_bounds.
+Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition runpackW_correct_and_bounded
+ := ExprUnOpWireToFE_correct_and_bounded
+ runpackW unpack runpackZ_sig runpackW_correct_and_bounded_gen
+ _ _.
Local Open Scope string_scope.
Compute ("Unpack", compute_bounds_for_display runpackW ExprUnOpWireToFE_bounds).
diff --git a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
index 992bc7a7e..c51e2d7f2 100755
--- a/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
+++ b/src/Specific/GF25519Reflective/Reified/rebuild-reified.py
@@ -7,6 +7,23 @@ for name, opkind in ([(name, 'BinOp') for name in ('Add', 'Carry_Add', 'Sub', 'C
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'):
+ extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
+Program Definition r%(lname)sW_correct_and_bounded
+ := Expr%(uopkind)s_correct_and_bounded
+ r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
+ _ _.
+""" % locals()
+ elif name == 'Freeze':
+ extra = r"""Local Obligation Tactic := intros; vm_compute; constructor.
+Axiom admit : forall {T}, T.
+(** XXX TODO: Fix bounds analysis on freeze *)
+Definition r%(lname)sW_correct_and_bounded
+ := Expr%(uopkind)s_correct_and_bounded
+ r%(lname)sW %(lname)s r%(lname)sZ_sig r%(lname)sW_correct_and_bounded_gen
+ admit admit.
+""" % locals()
with open(name.replace('_', '') + '.v', 'w') as f:
f.write(r"""Require Import Crypto.Specific.GF25519Reflective.Common.
@@ -15,7 +32,7 @@ Definition r%(lname)sW := Eval vm_compute in rword_of_Z r%(lname)sZ_sig.
Lemma r%(lname)sW_correct_and_bounded_gen : correct_and_bounded_genT r%(lname)sW r%(lname)sZ_sig.
Proof. rexpr_correct. Qed.
Definition r%(lname)s_output_bounds := Eval vm_compute in compute_bounds r%(lname)sW Expr%(uopkind)s_bounds.
-
+%(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).*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 12:13:41 +0000