From 732e7c1a79d3f76bd50c3ced56510dcb50140a13 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Sep 2016 11:05:07 -0700 Subject: Address code review, add come comments and cleanup --- src/Experiments/FancyMachine256.v | 33 +++++++++++++++----------------- src/Experiments/FancyMachineBarrett256.v | 13 ++++++------- 2 files changed, 21 insertions(+), 25 deletions(-) (limited to 'src') diff --git a/src/Experiments/FancyMachine256.v b/src/Experiments/FancyMachine256.v index 4fc6e3d1e..d11cfe6ad 100644 --- a/src/Experiments/FancyMachine256.v +++ b/src/Experiments/FancyMachine256.v @@ -1,3 +1,4 @@ +(** * A Fancy Machine with 256-bit registers *) Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. Require Export Coq.ZArith.ZArith. Require Export Crypto.BoundedArithmetic.Interface. @@ -17,6 +18,7 @@ Local Notation eta x := (fst x, snd x). Local Notation eta3 x := (eta (fst x), snd x). Local Notation eta3' x := (fst x, eta (snd x)). +(** ** Reflective Assembly Syntax *) Section reflection. Context (ops : fancy_machine.instructions (2 * 128)). Local Set Boolean Equality Schemes. @@ -92,24 +94,6 @@ Section reflection. Definition CSE {t} e := @CSE base_type SConstT op_code base_type_beq SConstT_beq op_code_beq internal_base_type_dec_bl interp_base_type op symbolicify_const symbolicify_op t e (fun _ => nil). End reflection. -Section instances. - Context {ops : fancy_machine.instructions (2 * 128)}. - Global Instance: reify_op op (@Interface.ldi) 1 OPldi := I. - Global Instance: reify_op op (@Interface.shrd) 3 OPshrd := I. - Global Instance: reify_op op (@Interface.shl) 2 OPshl := I. - Global Instance: reify_op op (@Interface.shr) 2 OPshr := I. - Global Instance: reify_op op (@Interface.mkl) 2 OPmkl := I. - Global Instance: reify_op op (@Interface.adc) 3 OPadc := I. - Global Instance: reify_op op (@Interface.subc) 3 OPsubc := I. - Global Instance: reify_op op (@Interface.mulhwll) 2 OPmulhwll := I. - Global Instance: reify_op op (@Interface.mulhwhl) 2 OPmulhwhl := I. - Global Instance: reify_op op (@Interface.mulhwhh) 2 OPmulhwhh := I. - Global Instance: reify_op op (@Interface.selc) 3 OPselc := I. - Global Instance: reify_op op (@Interface.addm) 3 OPaddm := I. - Global Instance: reify type Z := TZ. - Global Instance: reify type bool := Tbool. - Global Instance: reify type fancy_machine.W := TW. -End instances. Ltac base_reify_op op op_head ::= lazymatch op_head with @@ -139,6 +123,14 @@ Ltac Reify e := constr:(CSE _ (InlineConst (Linearize v))). (*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*) +(** ** Raw Syntax Trees *) +(** These are used solely for pretty-printing the expression tree in a + form that can be basically copy-pasted into other languages which + can be compiled for the Fancy Machine. Hypothetically, we could + add support for custom named identifiers, by carrying around + [string] identifiers and using them for pretty-printing... It + might also be possible to verify this layer, too, by adding a + partial interpretation function... *) Section syn. Context {var : base_type -> Type}. Inductive syntax := @@ -265,6 +257,8 @@ Notation "'λ' x .. y , t" := (cAbs (fun x => .. (cAbs (fun y => t)) ..)) Definition Syntax := forall var, @syntax var. +(** Assemble a well-typed easily interpretable expression into a + syntax tree we can use for pretty-printing. *) Section assemble. Context (ops : fancy_machine.instructions (2 * 128)). @@ -291,6 +285,9 @@ Section assemble. | Syntax.Var _ x => x | Syntax.Op t1 tR op args => let v := @assemble_syntaxf t1 args in + (* handle both associativities of pairs in 3-ary + operators, in case we ever change the + associativity *) match op, v with | OPldi , cConstZ 0 => RegZero | OPldi , cConstZ v => cINVALID v diff --git a/src/Experiments/FancyMachineBarrett256.v b/src/Experiments/FancyMachineBarrett256.v index 5ca25fdb4..0243c284f 100644 --- a/src/Experiments/FancyMachineBarrett256.v +++ b/src/Experiments/FancyMachineBarrett256.v @@ -2,12 +2,12 @@ Require Import Crypto.Experiments.FancyMachine256. Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded. Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook. +(** Useful for arithmetic in the field of integers modulo the order of the curve25519 base point *) Section expression. Let b : Z := 2. Let k : Z := 253. Let offset : Z := 3. Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops). - (** 25519 dsa *) Context (m μ : Z) (m_pos : 0 < m). Let base_pos : 0 < b. reflexivity. Qed. @@ -29,7 +29,7 @@ Section expression. (@ZLikeOps_of_ArchitectureBoundedOps 128 ops m _)). Definition ldi' : load_immediate SmallT := _. Let isldi : is_load_immediate ldi' := _. - Axiom (μ_range : 0 <= b ^ (2 * k) / m < b ^ (k + offset)). + Context (μ_range : 0 <= b ^ (2 * k) / m < b ^ (k + offset)). Definition μ' : SmallT := ldi' μ. Let μ'_eq : ZBounded.decode_small μ' = μ. Proof. @@ -54,7 +54,7 @@ Section expression. let RegZero := fancy_machine.ldi 0 in expression' v. - Definition expression_eq v H : fancy_machine.decode (expression v) = _ + Definition expression_eq v (H : 0 <= _ < _) : fancy_machine.decode (expression v) = _ := proj1 (proj2_sig (pre_f v) H). End expression. @@ -88,14 +88,13 @@ Section reflected. (H2 : 3 * m <= b^(k + offset)) (H3 : b^(k - offset) <= m + 1) (H4 : 0 <= m < 2^(k + offset)) + (H5 : 0 <= b^(2 * k) / m < b^(k + offset)) (v : tuple fancy_machine.W 2) - (H5 : 0 <= decode v < b^(2 * k)) + (H6 : 0 <= decode v < b^(2 * k)) : fancy_machine.decode (result v) = decode v mod m. Proof. rewrite sanity; destruct v. - eapply expression_eq; assumption. - Grab Existential Variables. - assumption. + apply expression_eq; assumption. Qed. End reflected. -- cgit v1.2.3