diff --git a/investigations/cava2/Expr.v b/investigations/cava2/Expr.v index e1d5c823f..3b26bb3ac 100644 --- a/investigations/cava2/Expr.v +++ b/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. diff --git a/investigations/cava2/Sha256Tests.v b/investigations/cava2/Sha256Tests.v new file mode 100644 index 000000000..68a8bc188 --- /dev/null +++ b/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. +*)