diff options
Diffstat (limited to 'src/Assembly')
| -rw-r--r-- | src/Assembly/Asm.v | 66 | ||||
| -rw-r--r-- | src/Assembly/AsmDSL.v | 34 | ||||
| -rw-r--r-- | src/Assembly/Computation.v | 175 | ||||
| -rw-r--r-- | src/Assembly/DSL.v | 28 | ||||
| -rw-r--r-- | src/Assembly/WordBounds.v | 122 |
5 files changed, 0 insertions, 425 deletions
diff --git a/src/Assembly/Asm.v b/src/Assembly/Asm.v deleted file mode 100644 index e2186df81..000000000 --- a/src/Assembly/Asm.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/AsmDSL.v b/src/Assembly/AsmDSL.v deleted file mode 100644 index 791b07391..000000000 --- a/src/Assembly/AsmDSL.v +++ /dev/null @@ -1,34 +0,0 @@ - -Require Import AsmComputation. - -Notation "stack32 A" := StackAsmVar A. -Notation "int32 A" := MemoryAsmVar A. -Notation "reg32 A" := Register A. - -Notation "{{ A }}" := AsmConst A. - -Notation "** A" := AsmRef A. -Notation "&& A" := AsmDeref A. - -Notation "~ A" := Unary AsmNot A. -Notation "- A" := Unary AsmOpp A. -Notation "A + B" := Binary AsmPlus A B. -Notation "A - B" := Binary AsmMinus A B. -Notation "A * B" := Binary AsmMult A B. -Notation "A / B" := Binary AsmDiv A B. -Notation "A & B" := Binary AsmAnd A B. -Notation "A | B" := Binary AsmOr A B. -Notation "A ^ B" := Binary AsmXor A B. -Notation "A >> B" := Binary AsmRShift A B. -Notation "A << B" := Binary AsmLShift A B. - -Notation "declare A" := AsmDeclare A -Notation "A ::= B" := AsmSet A B -Notation "(A B) =:= C" := AsmDestruct A B C -Notation "A =:= (B C)" := AsmConstruct A B C -Notation "A ;; B" := AsmSeq A B -Notation "A :: B" := AsmLabel A B -Notation "goto A" := AsmGoto A -Notation "A ? B" := AsmIf A B - -Notation "enter A do B" := Asm A B diff --git a/src/Assembly/Computation.v b/src/Assembly/Computation.v deleted file mode 100644 index 33af0974e..000000000 --- a/src/Assembly/Computation.v +++ /dev/null @@ -1,175 +0,0 @@ - -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/DSL.v b/src/Assembly/DSL.v deleted file mode 100644 index 2cb07a5d4..000000000 --- a/src/Assembly/DSL.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/WordBounds.v b/src/Assembly/WordBounds.v deleted file mode 100644 index e05fcb1d4..000000000 --- a/src/Assembly/WordBounds.v +++ /dev/null @@ -1,122 +0,0 @@ -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 <https://eprint.iacr.org/2015/943.pdf> 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. |