Run SHA-256 test vectors on circuit

investigations/cava2/Expr.v

@@ -63,6 +63,10 @@ Section Vars.
   .
 End Vars.
 
+Definition state_of {var s i o} (c : @Circuit var s i o) : type := s.
+Definition input_of {var s i o} (c : @Circuit var s i o) : type := i.
+Definition output_of {var s i o} (c : @Circuit var s i o) : type := o.
+
 Declare Scope expr_scope.
 Declare Custom Entry expr.
 Delimit Scope expr_scope with expr.
@@ -132,51 +136,52 @@ Section Var.
 
 End Var.
 
-Section RegressionTests.
+Module RegressionTests.
   Import ExprNotations.
 
-  Context {var : tvar}.
-
-  Definition fork2 {A} : Circuit [] [A] (A ** A) := {{
-    fun a => ( a, a)
-  }}.
-
-  Definition silly_id {A} : Circuit [] [A] A := {{
-    fun a => let '(x,y;z) := (a, `fork2` a) in z
-  }}.
-
-  Definition fst3 {A} : Circuit [] [A**A**A] A := {{
-    fun xyz => let '(x,y;z) := xyz in x
-  }}.
-
-  Definition ite_test {A} : Circuit [] [Bit; A] A := {{
-    fun flag a =>
-      if `silly_id` flag then (a) else a
-  }}.
-
-  Definition inital_state {sz} : denote_type (BitVec sz ** BitVec sz) := (0,1)%N.
-
-  Definition test {sz: nat}: Circuit (BitVec 10**BitVec 10) [] (BitVec 10) := {{
-    let/delay '(x;y) := (y,x) initially inital_state in y
-  }}.
-
-  Definition test2 {sz: nat}: Circuit (BitVec sz ** BitVec sz) [BitVec sz ** BitVec sz ] (BitVec sz) := {{
-    fun xy =>
-    let '(x ; y) := xy in
-    let/delay '(z;w) :=
-      let t := x in
-      (w, z)
-      initially inital_state in
-      x
-  }}.
-
-  (* Function composition for single arg functions *)
-  Definition compose {s1 s2 x y z} (f: Circuit s1 [x] y) (g: Circuit s2 [y] z)
-    : Circuit (s1++s2) [x] z := {{
-    fun x => `g` ( `f` x )
-  }}.
-  (* Notation "f >=> g" := (compose f g) (at level 61, right associativity) : expr_scope. *)
-
+  Section WithVar.
+    Context {var : tvar}.
+
+    Definition fork2 {A} : Circuit [] [A] (A ** A) := {{
+        fun a => ( a, a)
+                                                      }}.
+
+    Definition silly_id {A} : Circuit [] [A] A := {{
+        fun a => let '(x,y;z) := (a, `fork2` a) in z
+                                                  }}.
+
+    Definition fst3 {A} : Circuit [] [A**A**A] A := {{
+        fun xyz => let '(x,y;z) := xyz in x
+                                                    }}.
+
+    Definition ite_test {A} : Circuit [] [Bit; A] A := {{
+        fun flag a =>
+          if `silly_id` flag then (a) else a
+                                                       }}.
+
+    Definition inital_state {sz} : denote_type (BitVec sz ** BitVec sz) := (0,1)%N.
+
+    Definition test {sz: nat}: Circuit (BitVec 10**BitVec 10) [] (BitVec 10) := {{
+        let/delay '(x;y) := (y,x) initially inital_state in y
+                                                                              }}.
+
+    Definition test2 {sz: nat}: Circuit (BitVec sz ** BitVec sz) [BitVec sz ** BitVec sz ] (BitVec sz) := {{
+        fun xy =>
+          let '(x ; y) := xy in
+          let/delay '(z;w) :=
+             let t := x in
+             (w, z)
+               initially inital_state in
+          x
+                                                                                                        }}.
+
+    (* Function composition for single arg functions *)
+    Definition compose {s1 s2 x y z} (f: Circuit s1 [x] y) (g: Circuit s2 [y] z)
+      : Circuit (s1++s2) [x] z := {{
+        fun x => `g` ( `f` x )
+                                  }}.
+    (* Notation "f >=> g" := (compose f g) (at level 61, right associativity) : expr_scope. *)
+  End WithVar.
 End RegressionTests.
 
 Axiom value_hole : forall {t}, t.

investigations/cava2/Sha256Tests.v

@@ -0,0 +1,80 @@
+(****************************************************************************)
+(* Copyright 2021 The Project Oak Authors                                   *)
+(*                                                                          *)
+(* Licensed under the Apache License, Version 2.0 (the "License")           *)
+(* you may not use this file except in compliance with the License.         *)
+(* You may obtain a copy of the License at                                  *)
+(*                                                                          *)
+(*     http://www.apache.org/licenses/LICENSE-2.0                           *)
+(*                                                                          *)
+(* Unless required by applicable law or agreed to in writing, software      *)
+(* distributed under the License is distributed on an "AS IS" BASIS,        *)
+(* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. *)
+(* See the License for the specific language governing permissions and      *)
+(* limitations under the License.                                           *)
+(****************************************************************************)
+
+Require Import Coq.Arith.PeanoNat.
+Require Import Coq.Lists.List.
+Require Import Coq.NArith.NArith.
+Require Import HmacSpec.SHA256.
+Require Import HmacSpec.Tests.SHA256TestVectors.
+Require Import Cava.Util.BitArithmetic.
+Require Import Cava.Expr.
+Require Import Cava.Semantics.
+Require Import Cava.Types.
+Require Import Cava.Sha256.
+Import ListNotations.
+
+(**** Convert to/from circuit signals ****)
+
+(* convert test vector data into circuit input signals *)
+Definition to_sha256_input (t : sha256_test_vector)
+  : list (denote_type (input_of (var:=denote_type) sha256)) :=
+  (* input must be divided into into 32-bit words *)
+  let l := N.to_nat t.(l) in
+  let nwords := l / 32 + (if l mod 32 =? 0 then 0 else 1) in
+  (* separate bytes for the final word and bytes for non-final words *)
+  let non_final_bytes := firstn ((nwords - 1) * 4) t.(msg_bytes) in
+  let final_bytes := skipn ((nwords - 1) * 4) t.(msg_bytes) in
+  (* convert bytes to words *)
+  let non_final_words := BigEndianBytes.bytes_to_Ns 4 non_final_bytes in
+  let final_bytes_padded := final_bytes ++ repeat Byte.x00 (4 - length final_bytes) in
+  let final_word := BigEndianBytes.concat_bytes final_bytes_padded in
+  let final_length := N.of_nat (length final_bytes) in
+  (* create actual input signals *)
+  let non_final_input : list (denote_type (input_of sha256)) :=
+      (* fifo_data_valid=1, fifo_data, is_final=0, final_length=0, clear=0 *)
+      List.map (fun data => (1, (data, (0, (0, (0, tt)))))%N) non_final_words in
+  let final_input : denote_type (input_of sha256) :=
+      (* fifo_data_valid=1, fifo_data, is_final=1, final_length=final_length,
+         clear=0 *)
+      (1, (final_word, (1, (final_length, (0, tt)))))%N in
+  (* create dummy input for cycles while circuit is computing final digest *)
+  let nblocks := length (SHA256.padded_msg t.(msg_bytes)) / (512 / N.to_nat w) in
+  let dummy_input : denote_type (input_of sha256) := (0, (0, (0, (0, (0, tt)))))%N in
+  (* TODO: is this number of dummy inputs always right? *)
+  non_final_input ++ [final_input] ++ repeat dummy_input (64*nblocks+13+4*nblocks).
+
+(* extract test result from circuit output signals *)
+Definition from_sha256_output
+           (out : list (denote_type (output_of (var:=denote_type) sha256)))
+  : N :=
+  let '(done, (digest, accept_input)) := last out default in
+  BigEndianBytes.concat_bytes (concat_digest digest).
+
+(**** Run test vectors ****)
+
+Goal (let t := test1 in
+      from_sha256_output (simulate sha256 (to_sha256_input t)) = t.(expected_digest)).
+Proof. vm_compute. reflexivity. Qed.
+
+Goal (let t := test2 in
+      from_sha256_output (simulate sha256 (to_sha256_input t)) = t.(expected_digest)).
+Proof. vm_compute. reflexivity. Qed.
+
+(* Currently fails to produce a valid output, even when run for >500 cycles!
+Goal (let t := test3 in
+      from_sha256_output (simulate sha256 (to_sha256_input t)) = t.(expected_digest)).
+Proof. vm_compute. reflexivity. Qed.
+*)