From 40a618b2139279e54cd7facec8cdd4e2b68473c1 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Tue, 27 Oct 2015 13:38:22 -0400 Subject: patches for galois --- _CoqProject | 1 + src/Assembly/ConstrainedComputation.v | 6 ++--- src/Galois/GaloisExamples.v | 21 +++++++-------- src/Galois/GaloisTheory.v | 9 +------ src/Galois/ZGaloisField.v | 50 +++++++++++++++++++++++++++++++++-- src/Rep/WordEquivalence.v | 4 +-- 6 files changed, 64 insertions(+), 27 deletions(-) diff --git a/_CoqProject b/_CoqProject index 9c07ea0dd..538b6efc9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4,6 +4,7 @@ src/Tactics/VerdiTactics.v src/Galois/Galois.v src/Galois/GaloisTheory.v +src/Galois/GaloisExamples.v src/Galois/AbstractGaloisField.v src/Galois/ComputationalGaloisField.v src/Galois/ZGaloisField.v diff --git a/src/Assembly/ConstrainedComputation.v b/src/Assembly/ConstrainedComputation.v index f36b75187..aa5702506 100644 --- a/src/Assembly/ConstrainedComputation.v +++ b/src/Assembly/ConstrainedComputation.v @@ -1,12 +1,11 @@ Require Import Bedrock.Word. +(* Expression *) (* THEORY: if we permit operations on joined types, we can represent * vector operations without searching *) Inductive CType: Set := - | Int32: CType - | Int64: CType - | Join: CType -> CType -> CType . + | Words | list word Definition cTypeToWord(type: CType): Type := match type with @@ -44,6 +43,7 @@ Inductive CExpr (type: CType) := Inductive Sub (inType: CType) (outType: CType) := | CRet : Expr outType -> Sub inType outType + (* | Repeat *) | CCompose : forall medType, (Sub inType medType) -> (Sub medType outType) diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index 35faf3f03..f649701b7 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -1,8 +1,7 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.ComputationalGaloisField. -Require Import Crypto.Galois.AbstractGaloisField. +Require Import Crypto.Galois.ZGaloisField. Definition two_5_1 := (two_p 5) - 1. Lemma two_5_1_prime : prime two_5_1. @@ -21,9 +20,8 @@ Module Modulus127_1 <: Modulus. End Modulus127_1. Module Example31. - Module Field := Galois Modulus31. - Module Theory := ComputationalGaloisField Modulus31. - Import Modulus31 Theory Field. + Module Theory := ZGaloisField Modulus31. + Import Theory. Local Open Scope GF_scope. Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2). @@ -32,13 +30,13 @@ Module Example31. field; trivial. Qed. - Lemma example2: forall x: GF, x * (ZToGF 2) = x + x. + Lemma example2: forall x: GF, x * (inject 2) = x + x. Proof. intros; simpl. field. Qed. - Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2. + Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2. Proof. intros; simpl. field; trivial. @@ -47,8 +45,8 @@ Module Example31. End Example31. Module TimesZeroTransparentTestModule. - Module Theory := ComputationalGaloisField Modulus127_1. - Import Modulus127_1 Theory Theory.Field. + Module Theory := ZGaloisField Modulus127_1. + Import Theory. Local Open Scope GF_scope. Lemma timesZero : forall a, a*0 = 0. @@ -58,13 +56,12 @@ Module TimesZeroTransparentTestModule. End TimesZeroTransparentTestModule. Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := AbstractGaloisField M. - Import M Theory Theory.Field. + Module Theory := ZGaloisField M. + Import Theory. Local Open Scope GF_scope. Lemma timesZero : forall a, a*0 = 0. intros. field. - ring. (* field doesn't work but ring does :) *) Qed. End TimesZeroParametricTestModule. diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index e95eed864..8fa1b4113 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -158,14 +158,7 @@ Module GaloisTheory (M: Modulus). (* Ring properties *) - Ltac GFexp_tac t := - match t with - | Z0 => N0 - | Zpos ?n => Ncst (Npos n) - | Z_of_N ?n => Ncst n - | NtoZ ?n => Ncst n - | _ => NotConstant - end. + Ltac GFexp_tac t := Ncst t. Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. Proof. diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v index 23b1c8dd8..bf9efa964 100644 --- a/src/Galois/ZGaloisField.v +++ b/src/Galois/ZGaloisField.v @@ -1,6 +1,6 @@ Require Import BinInt BinNat ZArith Znumtheory. -Require Import BoolEq. +Require Import BoolEq Field_theory. Require Import Galois GaloisTheory. Module ZGaloisField (M: Modulus). @@ -26,13 +26,59 @@ Module ZGaloisField (M: Modulus). symmetry; apply Zeq_bool_eq; trivial. Qed. + Lemma GFmorph_div_theory: + div_theory eq Zplus Zmult inject Z.quotrem. + Proof. + constructor; intros; intuition. + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + eq_remove_proofs; demod; + rewrite <- (Z.quot_rem' a b); + destruct a; simpl; trivial. + Qed. + + Lemma injectZeroIsGFZero : + GFzero = inject 0. + Proof. + apply gf_eq; simpl; trivial. + Qed. + + Lemma injectOneIsGFOne : + GFone = inject 1. + Proof. + apply gf_eq; simpl; intuition. + symmetry; apply Zmod_small; destruct modulus; simpl; + apply prime_ge_2 in p; intuition. + Qed. + + Ltac GFpreprocess := + repeat rewrite injectZeroIsGFZero; + repeat rewrite injectOneIsGFOne. + + Ltac GFpostprocess := + repeat rewrite <- injectZeroIsGFZero; + repeat rewrite <- injectOneIsGFOne. + + Ltac GFconstant t := + match t with + | inject ?x => x + | _ => NotConstant + end. + Add Ring GFring_Z : GFring_theory (morphism GFring_morph, + constants [GFconstant], + div GFmorph_div_theory, power_tac GFpower_theory [GFexp_tac]). Add Field GFfield_Z : GFfield_theory (morphism GFring_morph, - power_tac GFpower_theory [GFexp_tac]). + preprocess [GFpreprocess], + postprocess [GFpostprocess], + constants [GFconstant], + div GFmorph_div_theory, + power_tac GFpower_theory [GFexp_tac]). End ZGaloisField. diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v index 4005adc2a..840919a49 100644 --- a/src/Rep/WordEquivalence.v +++ b/src/Rep/WordEquivalence.v @@ -37,13 +37,13 @@ Module GFBits (M: Modulus). wordEq a b := wordToN (combineAll a) = wordToN (combineAll b) Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)). - Definition toGF (b: BinGF) := ZToGF ((toZ b) mod modulus) + Definition toGF (b: BinGF) := inject ((toZ b) mod modulus) Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x)) Definition fromGF (x: GF) := fromZ (proj1_sig x). toZ a + toZ b = toZ (a ^+ b) - + Lemma equivalent_GF : BinEquiv x y <-> x = toGF y. Admitted. -- cgit v1.2.3 From a7a2d882691af1cddd729f1f871c467900b9ac4e Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Oct 2015 00:53:26 -0400 Subject: remove SearchAbouts --- src/Galois/BaseSystem.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index 55b7b66dd..e818660e8 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -46,7 +46,6 @@ Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, Z.pos x ^ Z.of_nat n > 0. do 2 (intros; induction n; subst; simpl in *; auto with zarith). - SearchAbout Pos.succ. rewrite <- Pos.add_1_r, Zpower_pos_is_exp. apply Zmult_gt_0_compat; auto; reflexivity. Qed. @@ -215,7 +214,6 @@ Module BaseSystem (Import B:BaseCoefs). rewrite plus_0_r. ring_simplify. replace (nth_default 0 base n * nth_default 0 base 0) with (nth_default 0 base 0 * nth_default 0 base n) by ring. - SearchAbout Z.div. rewrite Z_div_mult; try ring. apply base_positive. -- cgit v1.2.3 From 2cb694b68c8d28b2049936f1c20349200eb121c2 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 26 Oct 2015 00:54:22 -0400 Subject: remove resolved todo --- src/Curves/PointFormats.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index baa6bd2a7..8ab81e0a8 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -66,8 +66,6 @@ Module PointFormats. Parameter projY : point -> GF. Parameter unifiedAdd : point -> point -> point. - (* TODO: split module here? *) - Parameter rep : point -> Spec.point -> Prop. Local Notation "P '~=' rP" := (rep P rP) (at level 70). Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y. -- cgit v1.2.3 From 72ab8f39357da607557eec92a7a4b7398a212cfd Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Thu, 29 Oct 2015 14:33:50 -0400 Subject: bingf --- src/Assembly/Asm.v | 66 +++++++++++++ src/Assembly/AsmComputation.v | 66 ------------- src/Assembly/Computation.v | 175 ++++++++++++++++++++++++++++++++++ src/Assembly/ConstrainedComputation.v | 154 ------------------------------ src/Assembly/ConstrainedDSL.v | 28 ------ src/Assembly/DSL.v | 28 ++++++ src/Rep/BinGF.v | 119 +++++++++++++++++++++++ src/Rep/WordEquivalence.v | 52 ---------- 8 files changed, 388 insertions(+), 300 deletions(-) create mode 100644 src/Assembly/Asm.v delete mode 100644 src/Assembly/AsmComputation.v create mode 100644 src/Assembly/Computation.v delete mode 100644 src/Assembly/ConstrainedComputation.v delete mode 100644 src/Assembly/ConstrainedDSL.v create mode 100644 src/Assembly/DSL.v create mode 100644 src/Rep/BinGF.v delete mode 100644 src/Rep/WordEquivalence.v diff --git a/src/Assembly/Asm.v b/src/Assembly/Asm.v new file mode 100644 index 000000000..e2186df81 --- /dev/null +++ b/src/Assembly/Asm.v @@ -0,0 +1,66 @@ + +Require Export Bedrock.Word. + +Inductive AsmType: Set := + | Int32 | Int64 + | Float80 | Int128 + | Pointer. + +Definition Name := String. + +Inductive AsmVar (type: AsmType) := + | StackAsmVar : Name -> AsmVar + | MemoryAsmVar : Name -> AsmVar + | Register : Name -> AsmVar. + +Definition bits (type: AsmType): nat := + match type with + | Int32 => 32 + | Int64 => 64 + | Float80 => 80 + | Int128 => 128 + | Pointer => 64 + end. + +Definition isDouble (a b: AsmType): Prop := + match (a, b) with + | (Int32, Int64) => True + | (Int64, Int128) => True + | _ => False + end. + +Inductive UnaryOp := + | AsmId | AsmNot | AsmOpp. + +Inductive BinaryOp := + | AsmPlus | AsmMinus | AsmMult + | AsmDiv | AsmAnd | AsmOr + | AsmXor | AsmRShift | AsmLShift. + +Inductive AsmTerm (type: AsmType) := + | AsmConst : (word (bits type)) -> (AsmTerm type) + | AsmVarTerm : AsmVar type -> AsmTerm type + | AsmRef: AsmVar type -> AsmTerm Pointer + | AsmDeref: AsmVar Pointer -> AsmTerm type. + +Inductive AsmExpr (type: AsmType) := + | Unary : UnaryOp -> (AsmTerm type) -> (AsmExpr type) + | Binary : BinaryOp -> (AsmTerm type) -> (AsmTerm type) -> (AsmExpr type). + +Inductive AsmComputation := + | AsmDeclare : forall t, AsmVar t -> AsmComputation + | AsmSet : forall t, AsmVar t -> Expr t -> AsmComputation + | AsmDestruct : forall t1 t2, + isDouble t1 t2 -> AsmVar t1 -> AsmVar t1 -> AsmExpr t2 + -> Unit. + | AsmConstruct : forall t1 t2, + isDouble t1 t2 -> AsmVar t2 -> AsmExpr t1 -> AsmExpr t1 + -> Unit. + | AsmSeq : AsmComputation -> AsmComputation -> AsmComputation + | AsmLabel : String -> AsmComputation -> AsmComputation + | AsmGoto : String -> AsmComputation + | AsmIf : forall t, (AsmTerm t) -> AsmComputation -> AsmComputation. + +Inductive AsmSub := + | Asm: forall t, + list ((AsmVar t) * (AsmTerm t)) -> AsmComputation -> AsmTerm t. diff --git a/src/Assembly/AsmComputation.v b/src/Assembly/AsmComputation.v deleted file mode 100644 index e2186df81..000000000 --- a/src/Assembly/AsmComputation.v +++ /dev/null @@ -1,66 +0,0 @@ - -Require Export Bedrock.Word. - -Inductive AsmType: Set := - | Int32 | Int64 - | Float80 | Int128 - | Pointer. - -Definition Name := String. - -Inductive AsmVar (type: AsmType) := - | StackAsmVar : Name -> AsmVar - | MemoryAsmVar : Name -> AsmVar - | Register : Name -> AsmVar. - -Definition bits (type: AsmType): nat := - match type with - | Int32 => 32 - | Int64 => 64 - | Float80 => 80 - | Int128 => 128 - | Pointer => 64 - end. - -Definition isDouble (a b: AsmType): Prop := - match (a, b) with - | (Int32, Int64) => True - | (Int64, Int128) => True - | _ => False - end. - -Inductive UnaryOp := - | AsmId | AsmNot | AsmOpp. - -Inductive BinaryOp := - | AsmPlus | AsmMinus | AsmMult - | AsmDiv | AsmAnd | AsmOr - | AsmXor | AsmRShift | AsmLShift. - -Inductive AsmTerm (type: AsmType) := - | AsmConst : (word (bits type)) -> (AsmTerm type) - | AsmVarTerm : AsmVar type -> AsmTerm type - | AsmRef: AsmVar type -> AsmTerm Pointer - | AsmDeref: AsmVar Pointer -> AsmTerm type. - -Inductive AsmExpr (type: AsmType) := - | Unary : UnaryOp -> (AsmTerm type) -> (AsmExpr type) - | Binary : BinaryOp -> (AsmTerm type) -> (AsmTerm type) -> (AsmExpr type). - -Inductive AsmComputation := - | AsmDeclare : forall t, AsmVar t -> AsmComputation - | AsmSet : forall t, AsmVar t -> Expr t -> AsmComputation - | AsmDestruct : forall t1 t2, - isDouble t1 t2 -> AsmVar t1 -> AsmVar t1 -> AsmExpr t2 - -> Unit. - | AsmConstruct : forall t1 t2, - isDouble t1 t2 -> AsmVar t2 -> AsmExpr t1 -> AsmExpr t1 - -> Unit. - | AsmSeq : AsmComputation -> AsmComputation -> AsmComputation - | AsmLabel : String -> AsmComputation -> AsmComputation - | AsmGoto : String -> AsmComputation - | AsmIf : forall t, (AsmTerm t) -> AsmComputation -> AsmComputation. - -Inductive AsmSub := - | Asm: forall t, - list ((AsmVar t) * (AsmTerm t)) -> AsmComputation -> AsmTerm t. diff --git a/src/Assembly/Computation.v b/src/Assembly/Computation.v new file mode 100644 index 000000000..33af0974e --- /dev/null +++ b/src/Assembly/Computation.v @@ -0,0 +1,175 @@ + +Require Import EqNat Peano_dec. +Require Import Bedrock.Word. + +(* Very basic definitions *) + +Definition wordSize := 32. + +Definition Name := nat. + +Definition WordCount := nat. + +Definition WordList (words: WordCount) := + {x: list (word wordSize) | length x = words}. + +Inductive Pointer := + | ListPtr: forall n, WordList n -> Pointer. + +Definition TypeBindings := Name -> option WordCount. + +Definition Bindings := Name -> option Pointer. + +(* Primary inductive language definitions *) + +Inductive CTerm (words: WordCount) := + | CConst : WordList words -> CTerm words + | CVar : Name -> CTerm words + | CConcat: forall t1 t2, t1 + t2 = words -> CTerm t1 -> CTerm t2 -> CTerm words + | CHead: forall n: nat, gt n words -> CTerm n -> CTerm words + | CTail: forall n: nat, gt n words -> CTerm n -> CTerm words. + +Inductive CExpr (words: WordCount) := + | CLift : (CTerm words) -> (CExpr words) + | CNot : (CExpr words) -> (CExpr words) + | COpp : (CExpr words) -> (CExpr words) + | COr : (CExpr words) -> (CExpr words) -> (CExpr words) + | CAnd : (CExpr words) -> (CExpr words) -> (CExpr words) + | CXor : (CExpr words) -> (CExpr words) -> (CExpr words) + | CRShift : forall n: nat, (CExpr words) -> (CExpr words) + | CLShift : forall n: nat, (CExpr words) -> (CExpr words) + | CPlus : (CExpr words) -> (CExpr words) -> (CExpr words) + | CMinus : (CExpr words) -> (CExpr words) -> (CExpr words) + | CMult : forall n: nat, n*2 = words -> + (CExpr n) -> (CExpr n) -> (CExpr words) + | CDiv : (CExpr words) -> (CExpr words) -> (CExpr words) + | CMod : (CExpr words) -> (CExpr words) -> (CExpr words). + +Definition bindType (name: Name) (type: WordCount) (bindings: TypeBindings) + : Name -> option WordCount := + fun x => if (beq_nat x name) then Some type else bindings x. + +Inductive Sub (inputs: TypeBindings) (output: WordCount) := + | CRet : CExpr output -> Sub inputs output + | CCompose : forall resultName resultSize, + inputs resultName = None + -> (Sub inputs resultSize) + -> (Sub (bindType resultName resultSize inputs) output) + -> (Sub inputs output) + | CIte : (Sub inputs 1) (* condition *) + -> (Sub inputs output) (* then *) + -> (Sub inputs output) (* else *) + -> (Sub inputs output) + | CLet : forall (name: Name) (n: WordCount), + CExpr n + -> (Sub (bindType name n inputs) output) + -> (Sub inputs output) + | CRepeat : forall (bindOutputTo: Name) (n: nat), + inputs bindOutputTo <> None + -> (Sub (bindType bindOutputTo output inputs) output) + -> (Sub inputs output). + +(* Some simple option-monad sugar *) + +Definition optionReturn {A} (x : A) := Some x. + +Definition optionBind {A B} (a : option A) (f : A -> option B) : option B := + match a with + | Some x => f x + | None => None + end. + +Notation "'do' A <- B ; C" := (optionBind B (fun A => C)) + (at level 200, X ident, A at level 100, B at level 200). + +Definition optionType {n m} (w: WordList n): option (WordList m). + destruct (eq_nat_dec n m); + abstract (try rewrite e in *; first [exact (Some w) | exact None]). +Defined. + +Definition wordListConcat {t1 t2 words}: + t1 + t2 = words -> WordList t1 -> WordList t2 -> WordList words. + intros; exists ((proj1_sig H0) ++ (proj1_sig H1))%list. + abstract (destruct H0, H1; simpl; + rewrite List.app_length; intuition). +Defined. + +Definition wordListHead {n words}: + gt n words -> WordList n -> WordList words. + intros; exists (List.firstn words (proj1_sig H0)). + abstract (destruct H0; simpl; + rewrite List.firstn_length; intuition). +Defined. + +Lemma skipnLength: forall A m (x: list A), + ge (length x) m -> + length (List.skipn m x) = length x - m. +Proof. + intros; assert (length x = length (List.firstn m x ++ List.skipn m x)%list). + - rewrite List.firstn_skipn; trivial. + - rewrite H0; rewrite List.app_length; rewrite List.firstn_length. + replace (min m (length x)) with m; try rewrite min_l; intuition. +Qed. + +Definition wordListTail {n words}: + gt n words -> WordList n -> WordList words. + intros; exists (List.skipn (n - words) (proj1_sig H0)). + abstract (destruct H0; simpl; + rewrite skipnLength; rewrite e; intuition). +Defined. + +(* Now some basic evaluation routines *) + +Fixpoint evalTerm {n} (bindings: Bindings) (term: CTerm n): + option (WordList n) := + match term with + | CConst lst => Some lst + | CVar name => + do p <- bindings name ; + match p with + | ListPtr m lst => optionType lst + end + | CConcat t1 t2 pf term1 term2 => + do a <- evalTerm bindings term1; + do b <- evalTerm bindings term2; + Some (wordListConcat pf a b)%list + | CHead n pf t => + do x <- evalTerm bindings t; + Some (wordListHead pf x) + | CTail n pf t => + do x <- evalTerm bindings t; + Some (wordListTail pf x) + end. + +Fixpoint evalExpr {n} (expr: CExpr n): option (word n) := + match expr with + | CLift term => None + | CNot a => None + | COpp a => None + | COr a b => + do x <- evalExpr a; + do y <- evalExpr b; + Some (x |^ y)%word + | CAnd a b => None + | CXor a b => None + | CRShift shift a => None + | CLShift shift a => None + | CPlus a b => None + | CMinus a b => None + | CMult _ _ a b => None + | CDiv a b => None + | CMod a b => None + end. + +Fixpoint evalSub (inputs: Name -> option WordCount) (output: WordCount) (sub: Sub inputs output) + : word output := + match sub with + | CRet e => natToWord output 0 + | CCompose resName resSize _ a b => natToWord output 0 + | CIte cond thenSub elseSub => natToWord output 0 + | CLet name wordCount expr inside => natToWord output 0 + | CRepeat inName times _ inside => natToWord output 0 + end. + +(* Equivalence Lemmas *) + diff --git a/src/Assembly/ConstrainedComputation.v b/src/Assembly/ConstrainedComputation.v deleted file mode 100644 index aa5702506..000000000 --- a/src/Assembly/ConstrainedComputation.v +++ /dev/null @@ -1,154 +0,0 @@ - -Require Import Bedrock.Word. -(* Expression *) - -(* THEORY: if we permit operations on joined types, we can represent - * vector operations without searching *) -Inductive CType: Set := - | Words | list word - -Definition cTypeToWord(type: CType): Type := - match type with - | Int32 => word 32 - | Int64 => word 64 - | Join a b => (cTypeToWord a) * (cTypeToWord b) - end. - -Definition bits(type: CType): nat := - match type with - | Int32 => 32 - | Int64 => 64 - | Join a b => (bits a) + (bits b) - end. - -Inductive UnaryOp := - | CNot | COpp. - -Inductive BinaryOp := - | CPlus | CMinus | CMult - | CDiv | CAnd | COr - | CXor | CRShift | CLShift. - -Inductive CTerm (type: CType) := - | CConst : (word (bits type)) -> (CTerm type) - | CVar : Name -> CTerm type - | CJoin : forall t1 t2, CTerm t1 -> CTerm t2 -> CTerm (Join t1 t2) - | CLeft : CTerm (Join type _) -> CTerm type - | CRight : CTerm (Join _ type) -> CTerm type. - -Inductive CExpr (type: CType) := - | TermExpr : (CTerm type) -> (CExpr type) - | UnaryExpr : UnaryOp -> (CTerm type) -> (CExpr type) - | BinaryExpr : BinaryOp -> (CTerm type) -> (CTerm type) -> (CExpr type). - -Inductive Sub (inType: CType) (outType: CType) := - | CRet : Expr outType -> Sub inType outType - (* | Repeat *) - | CCompose : forall medType, - (Sub inType medType) - -> (Sub medType outType) - -> (Sub inType outType) - | CIte : (Sub inType Int32) (* condition *) - -> (Sub inType outType) (* then *) - -> (Sub inType outType) (* else *) - -> (Sub inType outType) - | CLet : Name -> CTerm -> - -> (Sub inType outType) - -> (Sub inType outType). - -Definition bindTerm {valueType objectType} (var: Name) (value: CTerm valueType) (object: CTerm objectType): CTerm objectType := - match valueType with - | objectType => - match object with - | CConst _ => object - | CVar name => if (name = var) then value else object end - | CJoin left right => - CJoin (bindTerm var value left) (bindTerm var value right) - | CLeft from => CLeft (bindTerm var value larger) - | CRight from => CRight (bindTerm var value larger) - end - | _ => object. - -Definition bindExpr {valueType objectType} (var: Name) (value: CTerm valueType) (object: CExpr objectType): CExpr objectType := - match object with - | TermExpr term => TermExpr (bindTerm var value term) - | UnaryExpr op term => UnaryExpr op (bindTerm var value term) - | BinaryExpr op term1 term2 => - BinaryExpr op (bindTerm var value term1) (bindTerm var value term2) - end. - -Definition bind {valueType fromType toType} (var: Name) (value: CTerm) (object: Sub fromType toType): Sub fromType toType := - match object with - | CRet expr => CRet (bindExpr var value expr) - | CCompose left right => - CCompose (bind var value left) (bind var value right) - | CIte cond thenSub elseSub => - CIte (bind var value cond) - (bind var value thenSub) - (bind var value elseSub) - | CLet name bindTo sub => - CLet name bindTo (bind var value sub) - end. - -Inductive TermEquiv {t} (left: CTerm t) (right: (cTypeToWord t)) := - | EquivInt32: forall (w: (word (bits Int32))), TermEquiv (CConst w) w - | EquivInt64: forall (w: (word (bits Int64))), TermEquiv (CConst w) w - | EquivJoin: forall aComp bComp aGallina bGallina, - TermEquiv aComp aGallina - -> TermEquiv bComp bGallina - -> TermEquiv (CJoin aComp bComp) (aGallina, bGallina) - | EquivLeft: forall aComp aGallina, - TermEquiv aComp aGallina - -> TermEquiv (CLeft aComp) (fst aGallina) - | EquivRight: forall aComp aGallina, - TermEquiv aComp aGallina - -> TermEquiv (CRight aComp) (snd aGallina). - -Definition applyBinaryOp {n: nat} (op: UnaryOp) (a b: word n) := - match op with - | CPlus => Word.plus a b - | CMinus => Word.minus a b - | CMult => Word.mult a b - | CDiv => Word.div a b - | CAnd => Word.and a b - | COr => Word.or a b - | CXor => Word.xor a b - | CRShift => Word.rshift a b - | CLShift => Word.lshift a b - end. - -Definition applyUnaryOp {n: nat} (op: UnaryOp) (w: word n) := - match op with - | CNot => Word.not w - | COpp => Word.opp w - end. - -Inductive ExprEquiv {t} (left: CExpr t) (right: (cTypeToWord t)) := - | EquivNop: forall aComp aGallina, - TermEquiv aComp aGallina - -> ExprEquiv (TermExpr aComp) aGallina - | EquivNot: forall aComp aGallina op, - TermEquiv aComp aGallina - -> ExprEquiv (UnaryExpr op aComp) (applyUnaryOp op aGallina) - | EquivPlus: forall aComp aGallina bComp bGallina op, - TermEquiv aComp aGallina - -> TermEquiv bComp bGallina - -> ExprEquiv (BinaryExpr op aComp bComp) (applyBinaryOp aGallina bGallina). - -Inductive SubEquiv {fromType toType} (left: Sub fromType toType) (right: (cTypeToWord fromType) -> (cTypeToWord toType)) := - | EquivRet: forall aComp aGallina, - ExprEquiv aComp aGallina - -> SubEquiv (CRet aComp) (fun x => aGallina) - | EquivComp: forall fComp fGallina gComp gGallina, - SubEquiv fComp fGallina - -> SubEquiv gComp gGallina - -> SubEquiv (CCompose fComp gComp) (fun x => gGallina (fGallina x)) - | EquivIte: forall (fComp: Sub fromType Int32) fGallina gComp gGallina, - SubEquiv fComp fGallina - -> SubEquiv gComp gGallina - -> SubEquiv hComp hGallina - -> SubEquiv (CIte fComp gComp hComp) - (fun x => if (neq 0 (fGallina x)) then gGallina x else hGallina x) - | EquivLet: forall name bindTo sub fGallina, - SubEquiv (bind name bindTo sub) fGallina - -> SubEquiv (CLet name bindTo sub) fGallina. diff --git a/src/Assembly/ConstrainedDSL.v b/src/Assembly/ConstrainedDSL.v deleted file mode 100644 index 2cb07a5d4..000000000 --- a/src/Assembly/ConstrainedDSL.v +++ /dev/null @@ -1,28 +0,0 @@ - -Require Export ConstrainedComputation. - -Notation "const A" := CConst A. -Notation "var A" := CVar A. -Notation "A : B" := CJoin A B. -Notation "left A" := CLeft A. -Notation "right A" := CRight A. - -Notation "~ A" := UnaryExpr CNot A. -Notation "- A" := UnaryExpr COpp A. -Notation "A + B" := BinaryExpr CPlus A B. -Notation "A - B" := BinaryExpr CMinus A B. -Notation "A * B" := BinaryExpr CMult A B. -Notation "A / B" := BinaryExpr CDiv A B. -Notation "A & B" := BinaryExpr CAnd A B. -Notation "A | B" := BinaryExpr COr A B. -Notation "A ^ B" := BinaryExpr CXor A B. -Notation "A >> B" := BinaryExpr CRShift A B. -Notation "A << B" := BinaryExpr CLShift A B. - -Definition toExpr {type} (term: CTerm type) = TermExpr term. -Coersion toExpr: {type} CTerm type >-> CExpr type. - -Notation "ret A" := CRet A -Notation "A . B" := CCompose A B -Notation "A ? B : C" := CIte A B C -Notation "set A to B in C" := CLet A B C diff --git a/src/Assembly/DSL.v b/src/Assembly/DSL.v new file mode 100644 index 000000000..2cb07a5d4 --- /dev/null +++ b/src/Assembly/DSL.v @@ -0,0 +1,28 @@ + +Require Export ConstrainedComputation. + +Notation "const A" := CConst A. +Notation "var A" := CVar A. +Notation "A : B" := CJoin A B. +Notation "left A" := CLeft A. +Notation "right A" := CRight A. + +Notation "~ A" := UnaryExpr CNot A. +Notation "- A" := UnaryExpr COpp A. +Notation "A + B" := BinaryExpr CPlus A B. +Notation "A - B" := BinaryExpr CMinus A B. +Notation "A * B" := BinaryExpr CMult A B. +Notation "A / B" := BinaryExpr CDiv A B. +Notation "A & B" := BinaryExpr CAnd A B. +Notation "A | B" := BinaryExpr COr A B. +Notation "A ^ B" := BinaryExpr CXor A B. +Notation "A >> B" := BinaryExpr CRShift A B. +Notation "A << B" := BinaryExpr CLShift A B. + +Definition toExpr {type} (term: CTerm type) = TermExpr term. +Coersion toExpr: {type} CTerm type >-> CExpr type. + +Notation "ret A" := CRet A +Notation "A . B" := CCompose A B +Notation "A ? B : C" := CIte A B C +Notation "set A to B in C" := CLet A B C diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v new file mode 100644 index 000000000..a19ae788b --- /dev/null +++ b/src/Rep/BinGF.v @@ -0,0 +1,119 @@ + +Require Import ZArith. +Require Import Bedrock.Word. +Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. +Require Import Crypto.Galois.ZGaloisField. +Require Import Eqdep_dec. + +Module Type BitSpec. + Parameter wordSize: nat. + Parameter numWords: nat. +End BitSpec. + +Module GFBits (M: Modulus) (Spec: BitSpec). + Module Field := ZGaloisField M. + Import Field Spec. + Local Open Scope GF_scope. + Local Open Scope list. + + Definition bits {k} (x: word k) := k. + + Definition BinGF := {lst: list (word wordSize) | length lst = numWords}. + + Definition convertWordSize {a b: nat} (x: word a): a = b -> word b. + intro H; rewrite H in x; exact x. + Defined. + + Lemma convert_invertible: + forall (a b: nat) (x: word a) (H1: a = b) (H2: b = a), + convertWordSize (convertWordSize x H1) H2 = x. + Proof. + intros; destruct H2; simpl. + replace H1 with (eq_refl b); simpl; intuition. + apply UIP_dec; exact eq_nat_dec. + Qed. + + Fixpoint splitWords' (sz: nat) (len: nat) (x: word sz): list (word wordSize). + induction len, (gt_dec sz wordSize). + + - refine nil. + + - refine nil. + + - assert (sz = wordSize + (sz - wordSize))%nat. intuition. + assert (z := convertWordSize x H). + refine ( + cons (split1 wordSize (sz - wordSize) z) + (splitWords' (sz - wordSize)%nat len + (split2 wordSize (sz - wordSize) z))). + + - assert (sz + (wordSize - sz) = wordSize)%nat. intuition. + assert (z := convertWordSize (zext x (wordSize - sz)) H). + refine (cons z nil). + + Admitted. + + Definition splitWords {sz} (len: nat) (x: word sz): + {x: list (word wordSize) | length x = len}. + exists (splitWords' sz len x). + + induction len, (gt_dec sz wordSize). + Admitted. + + Definition splitGF (x: GF) := + splitWords numWords (NToWord (numWords * wordSize)%nat (Z.to_N (proj1_sig x))). + + Fixpoint combineAll' (b: list (word wordSize)): word (wordSize * (length b)). + induction b. + + - simpl. + replace (wordSize * 0)%nat with 0%nat; intuition. + exact (natToWord 0 0). + + - replace (wordSize * length (a :: b))%nat + with (wordSize + wordSize * length b)%nat. + + exact (combine a IHb). + + simpl; rewrite mult_succ_r; intuition. + Defined. + + Definition combineAll (b: BinGF): GF := + inject (Z.of_N (wordToN (combineAll' (proj1_sig b)))). + + Definition binEquiv a b := combineAll a = combineAll b. + + Lemma combine_split: + forall (x: GF) (len: nat), + combineAll (splitGF x) = x. + Admitted. + + Record unaryOp: Set := mkUnary { + f : GF -> GF; + binF : BinGF -> BinGF; + + unaryCompat : forall (a b: GF), + a = b -> f a = f b; + + unaryBinCompat : forall (a b: BinGF), + binEquiv a b -> binEquiv (binF a) (binF b); + + unaryCorrect: forall (a: GF), + f a = combineAll (binF (splitGF a)) + }. + + Record binaryOp: Set := mkBinary { + g : GF -> GF -> GF; + binG : BinGF -> BinGF -> BinGF; + + binaryCompat : forall (a b c d: GF), + a = b -> c = d -> g a c = g b d; + + binaryBinCompat : forall (a b c d: BinGF), + binEquiv a b -> binEquiv c d -> + binEquiv (binG a c) (binG b d); + + binaryCorrect: forall (a b: GF), + g a b = combineAll (binG (splitGF a) (splitGF b)) + }. + +End GFBits. + diff --git a/src/Rep/WordEquivalence.v b/src/Rep/WordEquivalence.v deleted file mode 100644 index 840919a49..000000000 --- a/src/Rep/WordEquivalence.v +++ /dev/null @@ -1,52 +0,0 @@ - -Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. - -Module GFBits (M: Modulus). - Module T := GaloisTheory Modulus31. - Import M T T.Field. - Local Open Scope GF_scope. - - Definition wordSize: nat := 32. - Definition bits {k} (word k) := k. - - (* I think we shouldn't fix this, but rather have a lemma for how - * many bits we need to represent a given prime *) - Definition numWords: nat := - let b := (bits (NtoWord (Z.to_N modulus))) - in (1 + b / 32)%nat. - - Definition BinGF := - {lst: list (word wordSize) | length lst = numWords}. - - Fixpoint splitWords {sz} (len: nat) (x: word sz): {x: list (word wordSize) | length x = len} := - match len with - | O => [] - | S len' => - if(sz - wordSize >? 0) - then Cons (split1 wordSize (sz - wordSize) x) - (splitWords len' (split2 wordSize (sz - wordSize) x)) - else zext x wordSize - end. - - Fixpoint combineAll (b: BinGF) := - match (proj1_sig b) with - | [] => natToWord 0 - | Cons x xs => combine x (combineAll xs) - end. - - wordEq a b := wordToN (combineAll a) = wordToN (combineAll b) - - Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)). - Definition toGF (b: BinGF) := inject ((toZ b) mod modulus) - - Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x)) - Definition fromGF (x: GF) := fromZ (proj1_sig x). - - toZ a + toZ b = toZ (a ^+ b) - - Lemma equivalent_GF : BinEquiv x y <-> x = toGF y. - Admitted. - - Lemma equivalent_word : BinEquiv x y <-> weq y (fromGF x). - Admitted. -End GFBits. -- cgit v1.2.3 From 9882ffed11619425880c87fe11d2357569a58203 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 Oct 2015 20:14:52 -0400 Subject: BaseSystem to Util.ListUtil: separate out generic list lemmas --- _CoqProject | 1 + src/Galois/BaseSystem.v | 40 +--------------------------------------- src/Util/ListUtil.v | 49 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 51 insertions(+), 39 deletions(-) create mode 100644 src/Util/ListUtil.v diff --git a/_CoqProject b/_CoqProject index bbb167dc3..3b45e81b9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,7 @@ -R fiat/src Fiat -R bedrock/Bedrock Bedrock src/Tactics/VerdiTactics.v +src/Util/ListUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v src/Galois/GaloisExamples.v diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v index e818660e8..77428e549 100644 --- a/src/Galois/BaseSystem.v +++ b/src/Galois/BaseSystem.v @@ -1,46 +1,8 @@ Require Import List. +Require Import Util.ListUtil. Require Import ZArith.ZArith ZArith.Zdiv. Require Import Omega. -Ltac nth_tac' := - intros; simpl in *; unfold error,value in *; repeat progress (match goal with - | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros - | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) - | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) - | [ H: _ /\ _ |- _ ] => destruct H - | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst - | [ H: None = Some _ |- _ ] => inversion H - | [ H: Some _ = None |- _ ] => inversion H - | [ |- Some _ = Some _ ] => apply f_equal - end); eauto; try (autorewrite with list in *); try omega; eauto. -Lemma nth_error_map : forall A B (f:A->B) i xs y, - nth_error (map f xs) i = Some y -> - exists x, nth_error xs i = Some x /\ f x = y. -Proof. - induction i; destruct xs; nth_tac'. -Qed. - -Lemma nth_error_seq : forall i start len, - nth_error (seq start len) i = - if lt_dec i len - then Some (start + i) - else None. - induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. -Qed. - -Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None -> - i >= length xs. -Proof. - induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. -Qed. - -Ltac nth_tac := - repeat progress (try nth_tac'; try (match goal with - | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H - | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H - | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H - end)). - Local Open Scope Z. Lemma pos_pow_nat_pos : forall x n, diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v new file mode 100644 index 000000000..7c203a320 --- /dev/null +++ b/src/Util/ListUtil.v @@ -0,0 +1,49 @@ +Require Import List. +Require Import Omega. + +Ltac nth_tac' := + intros; simpl in *; unfold error,value in *; repeat progress (match goal with + | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros + | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) + | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ H: _ /\ _ |- _ ] => destruct H + | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst + | [ H: None = Some _ |- _ ] => inversion H + | [ H: Some _ = None |- _ ] => inversion H + | [ |- Some _ = Some _ ] => apply f_equal + end); eauto; try (autorewrite with list in *); try omega; eauto. +Lemma nth_error_map : forall A B (f:A->B) i xs y, + nth_error (map f xs) i = Some y -> + exists x, nth_error xs i = Some x /\ f x = y. +Proof. + induction i; destruct xs; nth_tac'. +Qed. + +Lemma nth_error_seq : forall i start len, + nth_error (seq start len) i = + if lt_dec i len + then Some (start + i) + else None. + induction i; destruct len; nth_tac'; erewrite IHi; nth_tac'. +Qed. + +Lemma nth_error_length_error : forall A i (xs:list A), nth_error xs i = None -> + i >= length xs. +Proof. + induction i; destruct xs; nth_tac'; try specialize (IHi _ H); omega. +Qed. + +Ltac nth_tac := + repeat progress (try nth_tac'; try (match goal with + | [ H: nth_error (map _ _) _ = Some _ |- _ ] => destruct (nth_error_map _ _ _ _ _ _ H); clear H + | [ H: nth_error (seq _ _) _ = Some _ |- _ ] => rewrite nth_error_seq in H + | [H: nth_error _ _ = None |- _ ] => specialize (nth_error_length_error _ _ _ H); intro; clear H + end)). + +Lemma app_cons_app_app : forall T xs (y:T) ys, xs ++ y :: ys = (xs ++ (y::nil)) ++ ys. +Proof. + induction xs; simpl; repeat match goal with + | [ H : _ |- _ ] => rewrite H; clear H + | _ => progress intuition + end; eauto. +Qed. -- cgit v1.2.3 From 1d34b00840bcf77969412c0ffc9a194dde1291ef Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 Oct 2015 20:14:52 -0400 Subject: word bound propagation examples --- _CoqProject | 1 + src/Assembly/WordBounds.v | 122 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 123 insertions(+) create mode 100644 src/Assembly/WordBounds.v diff --git a/_CoqProject b/_CoqProject index 3b45e81b9..ca6ca21f9 100644 --- a/_CoqProject +++ b/_CoqProject @@ -11,4 +11,5 @@ src/Galois/ComputationalGaloisField.v src/Galois/ZGaloisField.v src/Galois/BaseSystem.v src/Curves/PointFormats.v +src/Assembly/WordBounds.v src/Curves/Curve25519.v diff --git a/src/Assembly/WordBounds.v b/src/Assembly/WordBounds.v new file mode 100644 index 000000000..e05fcb1d4 --- /dev/null +++ b/src/Assembly/WordBounds.v @@ -0,0 +1,122 @@ +Require Import Bedrock.Word. +Import BinNums PArith.BinPos NArith.BinNat NArith.Ndigits. + +Definition wordUn (f : N -> N) {sz : nat} (x : word sz) := + NToWord sz (f (wordToN x)). +Definition wshr {l} n := @wordUn (fun x => N.shiftr x n) l. +Lemma wshr_test : (wordToN (wshr 3 (NToWord 32 (128- 19)))) = 13%N. + reflexivity. +Qed. + +Module WordBoundsExamples. + Definition u31 := word 31. + Definition U31 := NToWord 31. + Definition u64 := word 64. + Definition U64 := NToWord 64. + + Definition c2 : u64 := NToWord _ 2. + Definition c19_31 : u31 := NToWord _ 19. + Definition c19 : u64 := NToWord _ 19. + Definition c38 : u64 := NToWord _ 38. + Definition t25_31 : u31 := NToWord _ (Npos (2^25)). + Definition t26_31 : u31 := NToWord _ (Npos (2^26)). + Definition t25 : u64 := NToWord _ (Npos (2^25)). + Definition t26 : u64 := NToWord _ (Npos (2^26)). + Definition t27 : u64 := NToWord _ (Npos (2^26)). + Definition m25 : u64 := t25^-(NToWord _ 1). + Definition m26 : u64 := t26^-(NToWord _ 1). + Definition r25 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 25 hk, wand m25 hk). + Definition r26 (hSk hk:u64) : (u64 * u64) := (hSk ^+ wshr 26 hk, wand m26 hk). + Definition r25mod (hSk hk:u64) : (u64 * u64) := (hSk ^+ c19^*wshr 25 hk, wand m25 hk). + + Lemma simple_add_rep : forall (a b c d:N), + (a < Npos(2^29) -> b < Npos(2^29) -> c < Npos(2^29) -> d < Npos(2^29))%N -> + wordToN(U31 a ^+ U31 b ^+ U31 c ^+ U31 d) = (a + b + c + d)%N. + Admitted. + + Lemma simple_add_bound : forall (a b c d:u64), + a < t25 -> b < t25 -> c < t25 -> d < t25 -> + (a ^+ b ^+ c ^+ d) < t27. + Admitted. + + (* the bounds can as well be stated in N if the _rep lemma works. + I am not sure whether it is a better idea to propagate the bounds in word or + in N, though -- proving rep requires propagating bounds for the subexpressions. + *) + + Lemma simple_linear_rep : forall (a b:N), (a < Npos(2^25) + Npos(2^26) -> b < Npos(2^25))%N -> + wordToN((U31 a)^*c19_31 ^+ U31 b) = (a*19 + b)%N. + Admitted. + + Lemma simple_linear_bound : forall (a b:u31), a < t25_31 ^+ t26_31 -> b < t25_31 -> + a^*c19_31 ^+ b < (NToWord _ 1946157056). (* (2**26+2**25)*19 + 2**25 = 1946157056 *) + Admitted. + + Lemma simple_mul_carry_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26) -> c < Npos(2^26))%N -> + wordToN(wshr 26 (U64 a ^* U64 b) ^+ U64 c) = ((a*b)/(2^26) + c)%N. + Admitted. + + Lemma simple_mul_carry_bound : forall (a b c:u64), a < t26 -> b < t26 -> c < t26 -> + wshr 26 (a ^* b) ^+ c < t27. + Admitted. + + Lemma simple_mul_reduce_rep : forall (a b c:N), (a < Npos(2^26) -> b < Npos(2^26))%N -> + wordToN(wand m26 (U64 a ^* U64 b)) = ((a*b) mod (2^26) + c)%N. + Admitted. + + Lemma sandy2x_bound : forall + (* this example is transcribed by hand from section 2.2. + it is very representative of the bounds check / absence-of-overflow proofs we actually + want to do. However, given its size, presence of transcription errors is totally plausible. + A corresponding _rep proof will also necessary.*) + (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 : u64) + (g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 : u64), + f0 < t26 -> g0 < t26 -> + f1 < t25 -> g1 < t25 -> + f2 < t26 -> g2 < t26 -> + f3 < t25 -> g3 < t25 -> + f4 < t26 -> g4 < t26 -> + f5 < t25 -> g5 < t25 -> + f6 < t26 -> g6 < t26 -> + f7 < t25 -> g7 < t25 -> + f8 < t26 -> g8 < t26 -> + f9 < t25 -> g9 < t25 -> + + let h0 := f0^*g0 ^+ c38^*f1^*g9 ^+ c19^*f2^*g8 ^+ c38^*f3^*g7 ^+ c19^*f4^*g6 ^+ c38^*f5^*g5 ^+ c19^*f6^*g4 ^+ c38^*f7^*g3 ^+ c19^*f8^*g2 ^+ c38^*f9^*g1 in + let h1 := f0^*g1 ^+ f1^*g0 ^+ c19^*f2^*g9 ^+ c19^*f3^*g8 ^+ c19^*f4^*g7 ^+ c19^*f5^*g6 ^+ c19^*f6^*g5 ^+ c19^*f7^*g4 ^+ c19^*f8^*g3 ^+ c19^*f9^*g2 in + let h2 := f0^*g2 ^+ c2^* f1^*g1 ^+ f2^*g0 ^+ c38^*f3^*g9 ^+ c19^*f4^*g8 ^+ c38^*f5^*g7 ^+ c19^*f6^*g6 ^+ c38^*f7^*g5 ^+ c19^*f8^*g4 ^+ c38^*f9^*g3 in + let h3 := f0^*g3 ^+ f1^*g2 ^+ f2^*g1 ^+ f3^*g0 ^+ c19^*f4^*g9 ^+ c19^*f5^*g8 ^+ c19^*f6^*g7 ^+ c19^*f7^*g6 ^+ c19^*f8^*g5 ^+ c19^*f9^*g4 in + let h4 := f0^*g4 ^+ c2^* f1^*g3 ^+ f2^*g2 ^+ c2^* f3^*g1 ^+ f4^*g0 ^+ c38^*f5^*g9 ^+ c19^*f6^*g8 ^+ c38^*f7^*g7 ^+ c19^*f8^*g6 ^+ c38^*f9^*g5 in + let h5 := f0^*g5 ^+ f1^*g4 ^+ f2^*g3 ^+ f3^*g2 ^+ f4^*g1 ^+ f5^*g0 ^+ c19^*f6^*g9 ^+ c19^*f7^*g8 ^+ c19^*f8^*g7 ^+ c19^*f9^*g6 in + let h6 := f0^*g6 ^+ c2^* f1^*g5 ^+ f2^*g4 ^+ c2^* f3^*g3 ^+ f4^*g2 ^+ c2^* f5^*g1 ^+ f6^*g0 ^+ c38^*f7^*g9 ^+ c19^*f8^*g8 ^+ c38^*f9^*g7 in + let h7 := f0^*g7 ^+ f1^*g6 ^+ f2^*g5 ^+ f3^*g4 ^+ f4^*g3 ^+ f5^*g2 ^+ f6^*g1 ^+ f7^*g0 ^+ c19^*f8^*g9 ^+ c19^*f9^*g8 in + let h8 := f0^*g8 ^+ c2^* f1^*g7 ^+ f2^*g6 ^+ c2^* f3^*g5 ^+ f4^*g4 ^+ c2^* f5^*g3 ^+ f6^*g2 ^+ c2^* f7^*g1 ^+ f8^*g0 ^+ c38^*f9^*g9 in + let h9 := f0^*g9 ^+ f1^*g8 ^+ f2^*g7 ^+ f3^*g6 ^+ f4^*g5 ^+ f5^*g4 ^+ f6^*g3 ^+ f7^*g2 ^+ f8^*g1 ^+ f9^*g0 in + + let (h1_1, h0_1) := r26 h1 h0 in + let (h2_1, h1_2) := r25 h2 h1_1 in + let (h3_1, h2_2) := r26 h3 h2_1 in + let (h4_1, h3_2) := r25 h4 h3_1 in + + let (h6_1, h5_1) := r25 h6 h5 in + let (h7_1, h6_2) := r26 h7 h6_1 in + let (h8_1, h7_2) := r25 h8 h7_1 in + let (h9_1, h8_2) := r26 h9 h8_1 in + let (h0_2, h9_2) := r25mod h0_1 h9_1 in + let (h1_3, h0_2) := r26 h1_2 h0_1 in + + let (h5_2, h4_2) := r26 h5_1 h4_1 in + let (h6_2, h5_3) := r25 h6_1 h5_2 in + + h0_2 < t26 /\ + h1_3 < t27 /\ + h2_2 < t26 /\ + h3_2 < t25 /\ + h4_2 < t26 /\ + h5_3 < t25 /\ + h6_2 < t27 /\ + h7_2 < t25 /\ + h8_2 < t26 /\ + h9_2 < t25. + Admitted. +End WordBoundsExamples. -- cgit v1.2.3 From 6db9640e6ff581c8c16eac3f1bddb95dcc762492 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 30 Oct 2015 10:47:20 -0400 Subject: Beautified BinGF.splitWords --- _CoqProject | 2 +- src/Rep/BinGF.v | 82 +++++++++++++++++++++++++++++++++++---------------------- 2 files changed, 52 insertions(+), 32 deletions(-) diff --git a/_CoqProject b/_CoqProject index ca6ca21f9..7f2624ee8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -5,10 +5,10 @@ src/Tactics/VerdiTactics.v src/Util/ListUtil.v src/Galois/Galois.v src/Galois/GaloisTheory.v +src/Galois/ZGaloisField.v src/Galois/GaloisExamples.v src/Galois/AbstractGaloisField.v src/Galois/ComputationalGaloisField.v -src/Galois/ZGaloisField.v src/Galois/BaseSystem.v src/Curves/PointFormats.v src/Assembly/WordBounds.v diff --git a/src/Rep/BinGF.v b/src/Rep/BinGF.v index a19ae788b..138277870 100644 --- a/src/Rep/BinGF.v +++ b/src/Rep/BinGF.v @@ -8,6 +8,8 @@ Require Import Eqdep_dec. Module Type BitSpec. Parameter wordSize: nat. Parameter numWords: nat. + + Axiom wordSize_pos : (wordSize > 0)%nat. End BitSpec. Module GFBits (M: Modulus) (Spec: BitSpec). @@ -20,45 +22,64 @@ Module GFBits (M: Modulus) (Spec: BitSpec). Definition BinGF := {lst: list (word wordSize) | length lst = numWords}. - Definition convertWordSize {a b: nat} (x: word a): a = b -> word b. - intro H; rewrite H in x; exact x. - Defined. - - Lemma convert_invertible: - forall (a b: nat) (x: word a) (H1: a = b) (H2: b = a), - convertWordSize (convertWordSize x H1) H2 = x. + Definition splitGt {n m} {H : (n > m)%nat} (w : word n) : word m * word (n - m). Proof. - intros; destruct H2; simpl. - replace H1 with (eq_refl b); simpl; intuition. - apply UIP_dec; exact eq_nat_dec. - Qed. + refine (let w' := match _ : (n = m + (n - m))%nat in _ = N return word N with + | eq_refl => w + end in + (split1 m (n - m) w', split2 m (n - m) w')); + abstract omega. + Defined. - Fixpoint splitWords' (sz: nat) (len: nat) (x: word sz): list (word wordSize). - induction len, (gt_dec sz wordSize). + Fixpoint copies {A} (x : A) (n : nat) : list A := + match n with + | O => nil + | S n' => x :: copies x n' + end. - - refine nil. + Definition splitWords' : forall (len : nat) {sz: nat} (x: word sz), list (word wordSize). + Proof. + refine (fix splitWords' (len : nat) {sz : nat} (w : word sz) {struct len} : list (word wordSize) := + match len with + | O => nil + | S len' => + if gt_dec sz wordSize + then let (w1, w2) := splitGt w in + w1 :: splitWords' len' w2 + else match _ in _ = N return list (word N) with + | eq_refl => zext w (wordSize - sz) :: copies (wzero _) len' + end + end)%nat; clear splitWords'; abstract omega. + Defined. - - refine nil. + Lemma length_cast : forall A (F : A -> Type) x1 x2 (pf : x1 = x2) x xs, + length (match pf in _ = X return list (F X) with + | eq_refl => x :: xs + end) = S (length xs). + Proof. + destruct pf; auto. + Qed. - - assert (sz = wordSize + (sz - wordSize))%nat. intuition. - assert (z := convertWordSize x H). - refine ( - cons (split1 wordSize (sz - wordSize) z) - (splitWords' (sz - wordSize)%nat len - (split2 wordSize (sz - wordSize) z))). + Lemma length_copies : forall A (x : A) n, length (copies x n) = n. + Proof. + induction n; simpl; auto. + Qed. - - assert (sz + (wordSize - sz) = wordSize)%nat. intuition. - assert (z := convertWordSize (zext x (wordSize - sz)) H). - refine (cons z nil). + Hint Rewrite length_cast length_copies. - Admitted. + Lemma length_splitWords' : forall len sz (w : word sz), length (splitWords' len w) = len. + Proof. + induction len; simpl; intuition; + match goal with + | [ |- context[match ?E with _ => _ end] ] => destruct E + end; simpl; try rewrite IHlen; autorewrite with core; reflexivity. + Qed. Definition splitWords {sz} (len: nat) (x: word sz): - {x: list (word wordSize) | length x = len}. - exists (splitWords' sz len x). - - induction len, (gt_dec sz wordSize). - Admitted. + {x: list (word wordSize) | length x = len}. + Proof. + exists (splitWords' len x); apply length_splitWords'. + Defined. Definition splitGF (x: GF) := splitWords numWords (NToWord (numWords * wordSize)%nat (Z.to_N (proj1_sig x))). @@ -116,4 +137,3 @@ Module GFBits (M: Modulus) (Spec: BitSpec). }. End GFBits. - -- cgit v1.2.3 From d2edf784f94d01a238f56e0ce4983739c43a77f1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 1 Nov 2015 21:25:38 -0500 Subject: set_nth --- src/Util/ListUtil.v | 39 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 7c203a320..5604ebcc3 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,11 +1,14 @@ Require Import List. Require Import Omega. +Require Import Arith.Peano_dec. Ltac nth_tac' := intros; simpl in *; unfold error,value in *; repeat progress (match goal with | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] => case_eq (nth_error xs i); intros - | [ |- context[if lt_dec ?a ?b then _ else _] ] => destruct (lt_dec a b) - | [ H: context[if lt_dec ?a ?b then _ else _] |- _ ] => destruct (lt_dec a b) + | [ |- context[(if lt_dec ?a ?b then _ else _) = _] ] => destruct (lt_dec a b) + | [ |- context[_ = (if lt_dec ?a ?b then _ else _)] ] => destruct (lt_dec a b) + | [ H: context[(if lt_dec ?a ?b then _ else _) = _] |- _ ] => destruct (lt_dec a b) + | [ H: context[_ = (if lt_dec ?a ?b then _ else _)] |- _ ] => destruct (lt_dec a b) | [ H: _ /\ _ |- _ ] => destruct H | [ H: Some _ = Some _ |- _ ] => injection H; clear H; intros; subst | [ H: None = Some _ |- _ ] => inversion H @@ -47,3 +50,35 @@ Proof. | _ => progress intuition end; eauto. Qed. + +(* xs[n] := x *) +Fixpoint set_nth {T} n x (xs:list T) {struct n} := + match n with + | O => match xs with + | nil => nil + | x'::xs' => x::xs' + end + | S n' => match xs with + | nil => nil + | x'::xs' => x'::set_nth n' x xs' + end + end. + +Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) (x x':T), + nth_error (set_nth m x xs) n = + if eq_nat_dec n m + then (if lt_dec n (length xs) then Some x else None) + else nth_error xs n. +Proof. + induction m. + + destruct n, xs; auto. + + intros; destruct xs, n; auto. + simpl; unfold error; match goal with + [ |- None = if ?x then None else None ] => destruct x + end; auto. + + simpl nth_error; erewrite IHm by auto; clear IHm. + destruct (eq_nat_dec n m), (eq_nat_dec (S n) (S m)); nth_tac. +Qed. -- cgit v1.2.3