diff options
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Compile.v | 12 | ||||
| -rw-r--r-- | src/Assembly/Evaluables.v | 18 | ||||
| -rw-r--r-- | src/Assembly/GF25519.v | 161 | ||||
| -rw-r--r-- | src/Assembly/GF25519BoundedInstantiation.v | 73 | ||||
| -rw-r--r-- | src/Assembly/LL.v | 2 |
5 files changed, 126 insertions, 140 deletions
diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v index 2ff50e0e1..91eb37a16 100644 --- a/src/Assembly/Compile.v +++ b/src/Assembly/Compile.v @@ -1,6 +1,6 @@ Require Import Coq.Logic.Eqdep. -Require Import Compare_dec Sumbool. -Require Import PeanoNat Omega. +Require Import Coq.Arith.Compare_dec Coq.Bool.Sumbool. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. Require Import Crypto.Assembly.PhoasCommon. Require Import Crypto.Assembly.HL. @@ -120,7 +120,7 @@ Module CompileLL. option (Reg n * list Assignment * Operation) := let mov := if (EvalUtil.mapping_dec (regM _ out) in1) - then [] + then [] else makeA (regM _ out) in1 in match op with @@ -138,7 +138,7 @@ Module CompileLL. | _ => None end - | OPmul => + | OPmul => match in2 with | regM r1 => Some (out, mov, DOp Mult out r1 None) | constM c => Some (out, mov ++ (makeA (regM _ tmp) in2), DOp Mult out tmp None) @@ -152,7 +152,7 @@ Module CompileLL. | _ => None end - | OPshiftr => + | OPshiftr => match in2 with | constM (constant _ _ w) => Some (out, mov, ROp Shr out (indexize (wordToNat w))) @@ -244,7 +244,7 @@ Module CompileLL. | TT => Const (@wzero n) | Prod t0 t1 => Pair (zeros t0) (zeros t1) end. - + Fixpoint exprF {t} (nextRegName: nat) (p: WExpr t) {struct p}: option Out := match p with | LetBinop t1 t2 t3 op x y t' eC => diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v index 0b19b5237..2b606c858 100644 --- a/src/Assembly/Evaluables.v +++ b/src/Assembly/Evaluables.v @@ -69,7 +69,7 @@ Section Z. (* Comparisons *) eltb := Z.ltb; - eeqb := Z.eqb; + eeqb := Z.eqb }. End Z. @@ -126,7 +126,7 @@ Section RangeUpdate. Qed. Lemma bWSub_lem: forall (x0 x1: word n) (low0 high1: N), - (low0 <= wordToN x0)%N -> (wordToN x1 <= high1)%N -> + (low0 <= wordToN x0)%N -> (wordToN x1 <= high1)%N -> (low0 - high1 <= & (x0 ^- x1))%N. Proof. intros. @@ -198,7 +198,7 @@ Section RangeUpdate. transitivity low0; try assumption. apply N.le_sub_le_add_r. apply N.le_add_r. - Qed. + Qed. End BoundedSub. Section LandOnes. @@ -288,11 +288,11 @@ Section RangeUpdate. Proof. unfold validBinaryWordOp; intros. - Ltac kill_preds := + Ltac kill_preds := repeat match goal with | [|- (N.pred _ < _)%N] => rewrite <- (N.pred_succ (Npow2 n)); - apply -> N.pred_lt_mono; + apply -> N.pred_lt_mono; instantiate; rewrite N.pred_succ; [ apply N.lt_succ_diag_r | apply N.neq_0_lt_0; apply Npow2_gt0] @@ -311,7 +311,7 @@ Section RangeUpdate. | [|- (0 <= _)%N] => apply N_ge_0 end; try eassumption. - - apply N.le_ge. + - apply N.le_ge. transitivity high1; [assumption|]. transitivity low0; [|assumption]. apply N.ge_le; assumption. @@ -410,7 +410,7 @@ Section RangeUpdate. - destruct (Nge_dec high0 (Npow2 n)). + rewrite <- (N.pred_succ (Npow2 n)). - apply -> N.pred_lt_mono; + apply -> N.pred_lt_mono; instantiate; rewrite (N.pred_succ (Npow2 n)); [nomega|]. apply N.neq_0_lt_0. @@ -474,7 +474,7 @@ Section RangeUpdate. - destruct (Nge_dec _ (Npow2 n)); [|assumption]. rewrite <- (N.pred_succ (Npow2 n)). - apply -> N.pred_lt_mono; + apply -> N.pred_lt_mono; instantiate; rewrite (N.pred_succ (Npow2 n)); [nomega|]. apply N.neq_0_lt_0. @@ -731,4 +731,4 @@ Section RangeWithValue. | _ => false end; }. -End RangeWithValue.
\ No newline at end of file +End RangeWithValue. diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v index d5b093161..091aa8008 100644 --- a/src/Assembly/GF25519.v +++ b/src/Assembly/GF25519.v @@ -20,9 +20,10 @@ Module GF25519. Section DefaultBounds. Import ListNotations. - Local Notation rr exp := (2^exp + 2^exp/10)%N. - Definition feBound: list N := + Local Notation rr exp := (2^exp + 2^exp/10)%Z. + + Definition feBound: list Z := [rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27; rr 26; rr 27]. End DefaultBounds. @@ -45,10 +46,10 @@ Module GF25519. Definition inputBounds := feBound ++ feBound. Definition ge25519_add_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in add. + Eval cbv beta delta [fe25519 carry_add mul carry_sub Let_In] in carry_add. Definition ge25519_add' (P Q: @interp_type Z FE) : - { r: @HL.expr Z FE | HL.Interp (t := FE) r = ge25519_add_expr P Q }. + { r: @HL.expr Z (@interp_type Z) FE | HL.interp (t := FE) r = ge25519_add_expr P Q }. Proof. vm_compute in P, Q; repeat match goal with @@ -64,8 +65,8 @@ Module GF25519. cbv beta delta [ge25519_add_expr]. let R := HL.rhs_of_goal in - let X := HL.Reify R in - transitivity (HL.Interp (t := ResultType) X); [reflexivity|]. + let X := HL.reify (@interp_type Z) R in + transitivity (HL.interp (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ interp_type interp_binop HL.interp @@ -76,119 +77,10 @@ Module GF25519. Definition ge25519_add (P Q: @interp_type Z ResultType) := proj1_sig (ge25519_add' P Q). - Definition hlProg': NAry 20 Z (@HL.Expr Z ResultType) := + Definition hlProg: NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := liftFE (fun p => (liftFE (fun q => ge25519_add p q))). - - Definition hlProg: NAry 20 Z (@CompileHL.Expr' Z ResultType) := - Eval vm_compute in (liftN (fun P => (fun T => P (@LL.arg Z T))) hlProg'). End AddExpr. - Module SubExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_sub_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in sub. - - Definition ge25519_sub' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_sub_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_sub_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_sub (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_sub' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_sub p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End SubExpr. - - Module MulExpr <: Expression. - Definition bits: nat := bits. - Definition inputs: nat := 20. - Definition width: Width bits := width. - Definition ResultType := FE. - Definition inputBounds := feBound ++ feBound. - - Definition ge25519_mul_expr := - Eval cbv beta delta [fe25519 add mul sub Let_In] in mul. - - Definition ge25519_mul' (P Q: @interp_type Z FE) : - { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_mul_expr P Q }. - Proof. - vm_compute in P, Q; repeat - match goal with - | [x:?T |- _] => - lazymatch T with - | Z => fail - | prod _ _ => destruct x - | _ => clear x - end - end. - - eexists. - cbv beta delta [ge25519_mul_expr]. - - let R := HL.rhs_of_goal in - let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); - [reflexivity|]. - - cbv iota beta delta [ - interp_type interp_binop HL.interp - Z.land ZEvaluable eadd esub emul eshiftr eand]. - reflexivity. - Defined. - - Definition ge25519_mul (P Q: @interp_type Z ResultType) := - proj1_sig (ge25519_mul' P Q). - - Definition hlProg'': NAry 20 Z (@HL.expr Z (@interp_type Z) ResultType) := - liftFE (fun p => (liftFE (fun q => ge25519_mul p q))). - - Definition hlProg': NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType). - refine (liftN (HLConversions.mapVar _ _) hlProg''); intro t; - [ refine LL.uninterp_arg | refine LL.interp_arg ]. - Defined. - - Definition hlProg: NAry 20 Z (@HL.expr Z (@LL.arg Z Z) ResultType) := - Eval vm_compute in hlProg'. - End MulExpr. - Module OppExpr <: Expression. Definition bits: nat := bits. Definition inputs: nat := 10. @@ -197,11 +89,11 @@ Module GF25519. Definition inputBounds := feBound. Definition ge25519_opp_expr := - Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp. + Eval cbv beta delta [fe25519 carry_add mul carry_sub carry_opp Let_In] in carry_opp. Definition ge25519_opp' (P: @interp_type Z FE) : { r: @HL.expr Z (@interp_type Z) FE - | HL.interp (E := ZEvaluable) (t := FE) r = ge25519_opp_expr P }. + | HL.interp (E := @ZEvaluable bits) (t := FE) r = ge25519_opp_expr P }. Proof. vm_compute in P; repeat match goal with @@ -218,7 +110,7 @@ Module GF25519. let R := HL.rhs_of_goal in let X := HL.reify (@interp_type Z) R in - transitivity (HL.interp (E := ZEvaluable) (t := ResultType) X); + transitivity (HL.interp (E := @ZEvaluable bits) (t := ResultType) X); [reflexivity|]. cbv iota beta delta [ @@ -235,12 +127,33 @@ Module GF25519. End OppExpr. Module Add := Pipeline AddExpr. - Module Sub := Pipeline SubExpr. - Module Mul := Pipeline MulExpr. Module Opp := Pipeline OppExpr. + + Section Operations. + Definition wfe: Type := @interp_type (word bits) FE. + + Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE). + Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE). + + Existing Instance WordEvaluable. + + Definition interp_bexpr (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + z. + + Definition interp_uexpr (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in + z. + + Definition radd : ExprBinOp := Add.wordProg. + Definition ropp : ExprUnOp := Opp.wordProg. + End Operations. End GF25519. Extraction "GF25519Add" GF25519.Add. -Extraction "GF25519Sub" GF25519.Sub. -Extraction "GF25519Mul" GF25519.Mul. -Extraction "GF25519Opp" GF25519.Opp.
\ No newline at end of file +Extraction "GF25519Opp" GF25519.Opp. diff --git a/src/Assembly/GF25519BoundedInstantiation.v b/src/Assembly/GF25519BoundedInstantiation.v new file mode 100644 index 000000000..83b0dd4bf --- /dev/null +++ b/src/Assembly/GF25519BoundedInstantiation.v @@ -0,0 +1,73 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Assembly.PhoasCommon. +Require Import Crypto.Assembly.QhasmCommon. +Require Import Crypto.Assembly.Compile. +Require Import Crypto.Assembly.LL. +Require Import Crypto.Assembly.GF25519. +Require Import Crypto.Specific.GF25519. +Require Import Crypto.Specific.GF25519BoundedCommon. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Tuple. + +(* Totally fine to edit these definitions; DO NOT change the type signatures at all *) +Section Operations. + Import Assembly.GF25519.GF25519. + Definition wfe: Type := @interp_type (word bits) FE. + + Definition ExprBinOp : Type := NAry 20 Z (@CompileLL.WExpr bits FE). + Definition ExprUnOp : Type := NAry 10 Z (@CompileLL.WExpr bits FE). + + Local Existing Instance WordEvaluable. + + Definition interp_bexpr' (op: ExprBinOp) (x y: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let '(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9) := y in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + z. + + Definition interp_uexpr' (op: ExprUnOp) (x: tuple (word bits) 10): tuple (word bits) 10 := + let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in + let op' := NArgMap (fun v => Z.of_N (@wordToN bits v)) op in + let z := LL.interp' (fun x => NToWord bits (Z.to_N x)) (op' x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) in + z. + + Definition radd : ExprBinOp := GF25519.Add.wordProg. + Definition ropp : ExprUnOp := GF25519.Opp.wordProg. +End Operations. + + +Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := interp_bexpr'. +Definition interp_uexpr : ExprUnOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W + := interp_uexpr'. +Axiom rfreeze : ExprUnOp. + +Local Notation binop_correct_and_bounded rop op + := (ibinop_correct_and_bounded (interp_bexpr rop) op) (only parsing). +Local Notation unop_correct_and_bounded rop op + := (iunop_correct_and_bounded (interp_uexpr rop) op) (only parsing). + +Local Ltac start_correct_and_bounded_t op op_expr lem := + intros; hnf in *; destruct_head' prod; simpl in * |- ; + repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end; + change op with op_expr; + rewrite <- lem. + +Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add. +Proof. + intros; hnf in *; destruct_head' prod; simpl in * |- . + repeat match goal with H : is_bounded _ = true |- _ => unfold_is_bounded_in H end. +Admitted. +Lemma rsub_correct_and_bounded : binop_correct_and_bounded rsub carry_sub. +Proof. +Admitted. +Lemma rmul_correct_and_bounded : binop_correct_and_bounded rmul mul. +Proof. +Admitted. +Lemma ropp_correct_and_bounded : unop_correct_and_bounded ropp carry_opp. +Proof. +Admitted. +Lemma rfreeze_correct_and_bounded : unop_correct_and_bounded rfreeze freeze. +Proof. +Admitted. diff --git a/src/Assembly/LL.v b/src/Assembly/LL.v index e08b752fe..fd0a92f96 100644 --- a/src/Assembly/LL.v +++ b/src/Assembly/LL.v @@ -108,7 +108,7 @@ Module LL. (C: arg t -> expr tC) (C_Proper : forall a1 a2, interp_arg a1 = interp_arg a2 -> interp (C a1) = interp (C a2)) : forall a, interp_arg a = interp e -> interp (under_lets e C) = interp (C a). - Proof. induction e; repeat (intuition (congruence || eauto) + simpl + rewrite_hyp !*). Qed. + Proof. induction e; repeat (intuition (congruence || eauto); simpl). Qed. Section match_arg. Context {T : Type}. |