Merge changes from the thesis branch.

src/Verse/AnnotatedCode.v

@@ -45,7 +45,7 @@ Section AnnotatedCode.
   Definition repCodeDenote sc (ls : forall v, Scope.scoped v sc (Repeat (line v)))
     : mline sc tyD
     := let srls := HlistMachine.specialise sc ls in
-       unroll (@linesDenote sc) srls.
+       @linesDenote sc (flatR srls).
 
 End AnnotatedCode.
 
@@ -57,16 +57,23 @@ Arguments repCodeDenote [tyD sc].
 
 (* Mapping instances for custom syntax notations *)
 
-#[export] Instance statement_line tyD (v : VariableT) : AST_maps (list (statement v)) (repeated (list (line tyD v)))
+#[export] Instance statement_line tyD (v : VariableT) : AST_maps (list (statement v)) (line tyD v)
+  := {|
+    CODE := List.map (@inst _ _)
+  |}.
+
+#[export] Instance statement_repLine tyD (v : VariableT) : AST_maps (list (statement v)) (repeated (list (line tyD v)))
   := {|
     CODE := fun ls => [ Repeat.repeat 1 (List.map (@inst _ _) ls) ]
   |}.
 
-#[export] Instance ann_line tyD (v : VariableT) : AST_maps (ann tyD v) (repeated (list (line tyD v)))
+#[export] Instance ann_line tyD (v : VariableT) : AST_maps (ann tyD v) (line tyD v)
+  := {| CODE := fun an => [ annot an ] |}.
+
+#[export] Instance ann_repLine tyD (v : VariableT) : AST_maps (ann tyD v) (repeated (list (line tyD v)))
   := {| CODE := fun an => [ Repeat.repeat 1 [ annot an ] ] |}.
 
 
-(*Notation "'CODE' c" := (List.map (@inst _ _) c) (at level 58).*)
 (* Notations for annotations *)
 
 Class Evaluate (v : VariableT) tyD varType
@@ -88,10 +95,10 @@ Definition VecVar n (x : VariableT) [k] ty := Vector.t (x (existT _ k ty)) n.
   : Evaluate v tyD (VecVar n)
   := fun _ _ f x => Vector.map (eval f (Evaluate := eVar)) x.
 
-
 Notation "'ASSERT' P" := (CODE ((fun _ : StoreP (Str _ _) => P) : ann _ _)) (at level 100).
 
 Require Import Verse.Scope.
+
 Section CodeGen.
 
   Variable sc : Scope.type verse_type_system.
@@ -149,11 +156,11 @@ Arguments tpt sc [tyD].
 
 (* Extracting Prop object from annotated code *)
 
-Ltac getProp func
-  := (let cv := constr:(fun v => curry_vec (func v)) in
-      let level0 := constr:(Scope.Cookup.specialise cv) in
-      let level0break := (eval hnf in (Scope.inferNesting level0)) in
-      let pvs := constr:(fst level0break) in
-      let level1 := constr:(snd level0break) in
-      let lvs := (eval hnf in (fst (Scope.inferNesting level1))) in
-      exact (tpt (pvs ++ lvs)%list cv)).
+Ltac vc_gen func
+  := let cv := constr:(fun v => curry_vec (func v)) in
+     let level0 := constr:(Scope.Cookup.specialise cv) in
+     let level0break := (eval hnf in (Scope.inferNesting level0)) in
+     let pvs := constr:(fst level0break) in
+     let level1 := constr:(snd level0break) in
+     let lvs := (eval hnf in (fst (Scope.inferNesting level1))) in
+     exact (tpt (pvs ++ lvs)%list cv).

src/Verse/Ast.v

@@ -115,8 +115,6 @@ Arguments statement [ts].
 (* We provide a coercion from `code` to `Repeat statement` so to still
    be able to use old code
 *)
-Coercion mapRep ts (v : Variables.U ts) (c : code v) : Repeat (statement v)
-  := [repeat 1 c]%list.
 
 (**
 
@@ -450,7 +448,7 @@ Module RepStatement.
              (tr : TypeSystem.translator src tgt)
              (v : Variables.U tgt)
     : repeated (code (Variables.Universe.coTranslate tr v)) -> repeated (code v)
-    :=  (push (Code.translate (v := v)tr)).
+    :=  (Repeat.map (Code.translate (v := v)tr)).
 
   Arguments translate [src tgt] tr [v].
 
@@ -463,7 +461,7 @@ Module RepStatement.
              (cr : TypeSystem.compiler src tgt)
              (v : Variables.U tgt)
              (c : repeated (code (Variables.Universe.coCompile cr v))) : result v
-    := pullOutRep (push (Code.compile cr (v := v)) c).
+    := pullOutRep (Repeat.map (Code.compile cr (v := v)) c).
 
   Arguments compile [src tgt] cr [v].
 

src/Verse/BitVector.v

@@ -180,10 +180,10 @@ Require Export setoid_ring.Algebra_syntax.
 used when writing bitvector annotations. Typeclass unification
 allowing delayed unification is the favored theory as to why.
  *)
-Class AND A := and : A -> A -> A.
-Class OR  A := or  : A -> A -> A.
-Class XOR A := xor : A -> A -> A.
-Class NOT A := not : A -> A.
+Class AND A := And : A -> A -> A.
+Class OR  A := Or  : A -> A -> A.
+Class XOR A := Xor : A -> A -> A.
+Class NOT A := Not : A -> A.
 
 #[export] Instance BV_and sz : AND (Bvector sz) := @BVand sz.
 #[export] Instance BV_or  sz : OR (Bvector sz)  := @BVor sz.
@@ -223,9 +223,9 @@ Infix "=?" := (bveq) (at level 70): bitvector_scope.
 Infix "/"           := BVquot      (at level 40, left associativity) : bitvector_scope.
 Infix "%"           := BVrem       (at level 40, left associativity) : bitvector_scope.
 
-Infix "&" := and (at level 56).
-Infix "⊕" := xor (at level 57).
-Infix "∣"  := or (at level 59, left associativity).
+Infix "&" := And (at level 56).
+Infix "⊕" := Xor (at level 57).
+Infix "∣"  := Or (at level 59, left associativity).
 
 Infix "&" := BVand (at level 56, only printing) : bitvector_scope.
 Infix "⊕" := BVxor (at level 57, only printing) : bitvector_scope.
@@ -234,7 +234,9 @@ Infix "∣"  := BVor (at level 59, left associativity, only printing) : bitvecto
 
 (* TODO : `~` should be < level 40. But conformance with some other
           `~` makes it 75 here *)
-Notation "~ E" := (not E)  (at level 75, right associativity).
+Notation "~ E" := (Not E)  (at level 75, right associativity).
+
+Notation "~ E" := (BVcomp E)  (at level 75, right associativity, only printing) : bitvector_scope.
 
 (* TODO : Why do we have bitvector_scope at all? These notations don't
           really overload any existing notations.

src/Verse/BitVector/Facts.v

@@ -663,7 +663,14 @@ the bitvector size.
 
 *)
 
-Lemma Bv2N_shiftR : forall sz n (vec : Bvector sz), Bv2N (BVshiftR n vec) = (Bv2N vec / 2^N.of_nat n)%N.
+(* TODO : Prove this! *)
+Lemma Bv2N_shiftL : forall sz n (vec : Bvector sz),
+    (Bv2N (BVshiftL n vec) = (2^N.of_nat n * Bv2N vec) mod 2^(N.of_nat sz))%N.
+Proof.
+Admitted.
+
+Lemma Bv2N_shiftR : forall sz n (vec : Bvector sz),
+    Bv2N (BVshiftR n vec) = (Bv2N vec / 2^N.of_nat n)%N.
 Proof.
   #[local] Hint Rewrite inj_shiftR : bitvector.
   #[export] Hint Resolve N.shiftr_div_pow2 : bitvector.

src/Verse/BitVector/Reflection.v

@@ -5,6 +5,9 @@ Require Import Verse.BitVector.
 Require Import Verse.BitVector.Facts.
 Require Import Verse.Modular.Equation.
 
+From Coq Require Import ssreflect ssrfun ssrbool.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
 
 Create HintDb bitvector_reflection.
 Lemma two_power_non_zero : forall n : N, (2^n)%N <> 0%N.
@@ -129,6 +132,7 @@ work in other modules that import this one.
 #[export] Instance add_N  : Addition N := N.add.
 #[export] Instance mul_N  : Multiplication := N.mul.
 
+#[export] Hint Unfold addition add_N multiplication mul_N : algebra.
 
 (** * Reified expressions of a
 
@@ -174,8 +178,10 @@ Module Exp.
     | Mul e1 e2 => denote e1 * denote e2
     end.
 
-  #[export] Instance add_exp A : Addition (t A) := Plus.
-  #[export] Instance mul_exp A : @Multiplication (t A) (t A):= Mul.
+  (* The following need global visibility for reflection tactics to work
+  elsewhere without an `Export Exp` *)
+  #[global] Instance add_exp A : Addition (t A) := Plus.
+  #[global] Instance mul_exp A : @Multiplication (t A) (t A):= Mul.
 
 End Exp.
 Import Exp.
@@ -285,25 +291,39 @@ Module Tactics.
          apply (N.lt_trans _ _ _ Hineq); simpl; lia
     end.
 
+  Ltac assert_arithmetic_mod H e sz :=
+    let eA := arithm e in
+    assert (H: Bv2N e <==[mod 2^N.of_nat sz] eA) by crush_modular e eA sz.
+
   Ltac assert_arithmetic H e sz :=
     let eA := arithm e in
     assert(H:Bv2N e = eA) by
-     ( let HM := fresh "HM" in
+      (let HM := fresh "HM" in
        assert (HM: Bv2N e <==[mod 2^N.of_nat sz] eA) by crush_modular e eA sz;
        try (rewrite HM; apply N.mod_small);
-       try (crush_ineq)).
+       try crush_ineq).
 
-  Ltac arithmetise sz :=
+  Ltac arithmetise_mod sz :=
     match goal with
     | [ |- context[Bv2N ?E] ] =>
         match E with
         | _ + _ => let H := fresh "HA" in
-                  try (assert_arithmetic H E sz; rewrite H)
+                   try (assert_arithmetic_mod H E sz; rewrite H; clear H)
         | _ * _ => let H := fresh "HA" in
-                  try (assert_arithmetic H E sz; rewrite H)
+                   try (assert_arithmetic_mod H E sz; rewrite H; clear H)
         end
     end.
 
+  Ltac arithmetise sz :=
+    match goal with
+    | [ |- context[Bv2N ?E] ] =>
+        match E with
+        | _ + _ => let H := fresh "HA" in
+                   try (assert_arithmetic H E sz; rewrite H; clear H)
+        | _ * _ => let H := fresh "HA" in
+                   try (assert_arithmetic H E sz; rewrite H; clear H)
+        end
+    end.
 
 End Tactics.
 

src/Verse/CryptoLib/blake2/c/portable.v

@@ -216,7 +216,7 @@ Module Blake2 (C : CONFIG).
       Variable byteCount : A.
 
 
-      Definition UPDATE_COUNTER (u l : progvar of type Word) : Repeat (statement progvar) :=
+      Definition UPDATE_COUNTER (u l : progvar of type Word) : code progvar :=
         [code| (* We first ensure that the variable C gets the carry that overflows
              when l is added bsize. For this we first need to get the msb of l
              into the lsb position
@@ -269,7 +269,7 @@ Module Blake2 (C : CONFIG).
 
      *)
 
-    Definition G (a b c d m0 m1 : progvar of type Word) : Repeat (statement progvar) :=
+    Definition G (a b c d m0 m1 : progvar of type Word) : code progvar :=
       [code|
         a += b; a += m0; d ⊕= a; d := d ⋙ R0;
         c += d;          b ⊕= c; b := b ⋙ R1;
@@ -332,7 +332,7 @@ Module Blake2 (C : CONFIG).
                                 (@Vector.nth_order _ _ RoundPerms (r mod 10) _))).
       Defined.
 
-      Definition BLAKE_ROUND : Repeat (statement progvar).
+      Definition BLAKE_ROUND : code progvar.
         verse (G v0 v4 v8  v12 (M 0 _) (M 1 _) ++
                G v1 v5 v9  v13 (M 2 _) (M 3 _) ++
                G v2 v6 v10 v14 (M 4 _) (M 5 _) ++
@@ -349,7 +349,7 @@ Module Blake2 (C : CONFIG).
     Definition ALL_ROUNDS := iterate (fun r (_ : r < ROUNDS) => BLAKE_ROUND r).
 
 
-    Definition SETUP : Repeat (statement progvar).
+    Definition SETUP : code progvar.
       verse ( [code| U := UpperRef [ 0 ]; L := LowerRef [ 0 ] |] ++ loadCache hash H )%list.
     Defined.
 
@@ -361,7 +361,7 @@ Module Blake2 (C : CONFIG).
         initialisation code.
 
      *)
-    Definition INIT_STATE : Repeat (statement progvar).
+    Definition INIT_STATE : code progvar.
       verse
         [code|
           v0  := H[0];
@@ -383,7 +383,7 @@ Module Blake2 (C : CONFIG).
         |].
     Defined.
 
-    Definition INIT_STATE_LAST : Repeat (statement progvar).
+    Definition INIT_STATE_LAST : code progvar.
       verse
         [code|
           v0 := H[0];
@@ -414,7 +414,7 @@ Module Blake2 (C : CONFIG).
      *)
     Definition W : VarIndex progvar BLOCK_SIZE Word := varIndex message_variables.
     Definition LOAD_MESSAGE_I (blk : progvar of type Block) (i : nat) (pf : i < BLOCK_SIZE)
-      : Repeat (statement progvar).
+      : code progvar.
       verse [code| `W i _` := blk [ i ] |].
     Defined.
     Definition LOAD_MESSAGE (blk : progvar of type Block)
@@ -426,7 +426,7 @@ Module Blake2 (C : CONFIG).
         After performing the rounds of blake, the hash gets updated as follows.
 
      *)
-    Definition UPDATE_HASH : Repeat (statement progvar).
+    Definition UPDATE_HASH : code progvar.
       verse
       [code|
         H[0] ⊕= v0 ; H[0] ⊕= v8;
@@ -442,7 +442,7 @@ Module Blake2 (C : CONFIG).
 
     (** In the iterator one needs to update the hash array as well as
         the reference variables UpperRef and LowerRef.  *)
-    Definition FINALISE : Repeat (statement progvar).
+    Definition FINALISE : code progvar.
       verse ([code| UpperRef [ 0 ] <- U ; LowerRef [ 0 ] <- L |] ++ moveBackCache hash H )%list.
     Defined.
 
@@ -460,7 +460,7 @@ Module Blake2 (C : CONFIG).
          finalise := FINALISE
       |}%list.
 
-    Definition lastBlock : Repeat (statement progvar) :=
+    Definition lastBlock : code progvar :=
       (loadCache hash H
                  ++ UPDATE_COUNTER_LAST
                  ++ INIT_STATE_LAST