Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto

6 files changed, 294 insertions, 206 deletions

diff --git a/src/Assembly/AsmComputation.v b/src/Assembly/Asm.v
index e2186df81..e2186df81 100644
--- a/src/Assembly/AsmComputation.v
+++ b/src/Assembly/Asm.v
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/DSL.v
index 2cb07a5d4..2cb07a5d4 100644
--- a/src/Assembly/ConstrainedDSL.v
+++ b/src/Assembly/DSL.v
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.