diff --git a/cava/Cava/Util/List.v b/cava/Cava/Util/List.v index 280a29642..9731ac9db 100644 --- a/cava/Cava/Util/List.v +++ b/cava/Cava/Util/List.v @@ -1027,6 +1027,15 @@ Section Replace. | S n' => x :: replace n' a xs end end%list. + + Lemma length_replace {A} : forall n a (ls: list A), + length (replace n a ls) = length ls. + Proof. + intros. generalize dependent n. + induction ls; intros; destruct n; + try reflexivity; + cbn; auto. + Qed. End Replace. (* Proofs about fold_right and fold_left *) diff --git a/cava2/TLUL.v b/cava2/TLUL.v index 2561b35e1..9ed1dc319 100644 --- a/cava2/TLUL.v +++ b/cava2/TLUL.v @@ -17,6 +17,8 @@ Require Import Coq.Lists.List. Require Import Coq.ZArith.ZArith. +Import ListNotations. + Require Import Cava.Expr. Require Import Cava.ExprProperties. Require Import Cava.Invariant. @@ -131,7 +133,7 @@ Section Var. Definition sha_digest := Vec sha_word 8. Definition tlul_adapter_state := - (BitVec TL_AIW ** BitVec TL_SZW ** BitVec 3 ** Bit ** Bit ** Bit ** Bit)%circuit_type. + (BitVec TL_AIW ** BitVec TL_SZW ** BitVec 3 ** BitVec 32 ** Bit ** Bit ** Bit ** Bit)%circuit_type. (* Convert TLUL packets to a simple read/write register interface *) (* This is similar to OpenTitan's tlul_adapter_reg, but for simplicity we @@ -153,7 +155,9 @@ Section Var. , a_user ; d_ready) := incoming_tlp in - let/delay '(reqid, reqsz, rspop, error, outstanding, we_o; re_o) := + let/delay '(reqid, reqsz, rspop, reqaddress, error, outstanding, + (* output only signals: *) + we_o; re_o) := let a_ack := a_valid && !outstanding in let d_ack := outstanding && d_ready in @@ -166,24 +170,25 @@ Section Var. let err_internal := `Zero` in let error_i := `Zero` in - let '(reqid, reqsz, rspop, error; outstanding) := - if a_ack then - ( a_source - , a_size - , if rd_req then `K AccessAckData` else `K AccessAck` - , error_i || err_internal - , `One` - ) - else - (reqid, reqsz, rspop, error, if d_ack then `Zero` else outstanding) + let '(reqid, reqsz, rspop, reqaddress, error; outstanding) := + if a_ack then + ( a_source + , a_size + , if rd_req then `K AccessAckData` else `K AccessAck` + , a_address + , error_i || err_internal + , `One` + ) + else + (reqid, reqsz, rspop, reqaddress, error, if d_ack then `Zero` else outstanding) in let we_o := wr_req && !err_internal in let re_o := rd_req && !err_internal in - (reqid, reqsz, rspop, error, outstanding, we_o, re_o) - initially (0,(0,(0,(false,(false,(false,false)))))) - : denote_type (BitVec _ ** BitVec _ ** BitVec _ ** Bit ** Bit ** Bit ** Bit) + (reqid, reqsz, rspop, reqaddress, error, outstanding, we_o, re_o) + initially default + : denote_type (BitVec _ ** BitVec _ ** BitVec _ ** BitVec _ ** Bit ** Bit ** Bit ** Bit) in let wdata_o := a_data in @@ -195,7 +200,7 @@ Section Var. , reqsz , reqid , `K 0` - , `index` registers (`bvslice 2 30` a_address) + , `index` registers (`bvslice 2 30` reqaddress) , `K 0` , error , !outstanding @@ -208,7 +213,7 @@ End Var. Ltac destruct_tlul_adapter_reg_state reg_count := destruct_state (tlul_adapter_reg (var:=denote_type) (reg_count:=reg_count)) - ipattern:((?reqid, (?reqsz, (?rspop, (?error, (?outstanding, (?we_o, ?re_o))))))). + ipattern:((?reqid, (?reqsz, (?rspop, (?reqaddress, (?error, (?outstanding, (?we_o, ?re_o)))))))). Section StateGetters. Definition var : tvar := denote_type. @@ -220,6 +225,9 @@ Section StateGetters. : N := ltac:(destruct_tlul_adapter_reg_state reg_count; apply reqsz). Definition tlul_adapter_reg_state_rspop (s : denote_type (state_of (tlul_adapter_reg (reg_count:=reg_count)))) : N := ltac:(destruct_tlul_adapter_reg_state reg_count; apply rspop). + Definition tlul_adapter_reg_state_reqaddress (s : denote_type (state_of (tlul_adapter_reg (reg_count:=reg_count)))) + : N := ltac:(destruct_tlul_adapter_reg_state reg_count; apply reqaddress). + Definition tlul_adapter_reg_state_error (s : denote_type (state_of (tlul_adapter_reg (reg_count:=reg_count)))) : bool := ltac:(destruct_tlul_adapter_reg_state reg_count; apply error). Definition tlul_adapter_reg_state_outstanding (s : denote_type (state_of (tlul_adapter_reg (reg_count:=reg_count)))) @@ -232,9 +240,9 @@ End StateGetters. Ltac tlul_adapter_reg_state_simpl := cbn [tlul_adapter_reg_state_reqid tlul_adapter_reg_state_reqsz - tlul_adapter_reg_state_rspop tlul_adapter_reg_state_error - tlul_adapter_reg_state_outstanding tlul_adapter_reg_state_we_o - tlul_adapter_reg_state_re_o] in *. + tlul_adapter_reg_state_rspop tlul_adapter_reg_state_reqaddress + tlul_adapter_reg_state_error tlul_adapter_reg_state_outstanding + tlul_adapter_reg_state_we_o tlul_adapter_reg_state_re_o] in *. Definition tl_h2d := denote_type tl_h2d_t. Definition tl_h2d_default := default (t := tl_h2d_t). @@ -342,41 +350,45 @@ Ltac tlsimpl := set_d_sink set_d_data set_d_user set_d_error set_a_ready d_valid d_opcode d_param d_size d_source d_sink d_data d_user d_error a_ready] in *. -Section TLULSpec. +Section TLSpec. Local Open Scope N_scope. Context {reg_count : nat}. - Variant TLULState := - | OutstandingGet (reqid : N) (reqsz : N) - | OutstandingPutFullData (reqid : N). - - Definition tlul_repr := option TLULState. - - Compute denote_type (input_of tlul_adapter_reg). - Instance tlul_specification - : specification_for (tlul_adapter_reg (reg_count:=reg_count)) tlul_repr := - {| reset_repr := None; - - update_repr := - fun (input : denote_type (input_of (tlul_adapter_reg (reg_count:=reg_count)))) - (repr : tlul_repr) => - let '(h2d, (_regs, tt)) := input in - match repr with - | None => - if a_valid h2d then - if a_opcode h2d =? Get then - Some (OutstandingGet (a_source h2d) (a_size h2d)) - else if a_opcode h2d =? PutFullData then - Some (OutstandingPutFullData (a_source h2d)) - else (* unrechable *) repr - else None - | Some _ => if d_ready h2d then None else repr - end; + Variant repr_state := + | Idle + | OutstandingAccessAckData (h2d : tl_h2d) (regs : list N) + | OutstandingAccessAck (h2d : tl_h2d). + + Definition update_repr_state (input : denote_type (input_of (tlul_adapter_reg (reg_count:=reg_count)))) repr := + let '(h2d, (regs, tt)) := input in + match repr with + | Idle => + if a_valid h2d then + if a_opcode h2d =? Get then + OutstandingAccessAckData h2d regs + else if a_opcode h2d =? PutFullData then + OutstandingAccessAck h2d + else (* unreachable *) repr + else + repr + | _ => + if d_ready h2d then Idle + else match repr with + | OutstandingAccessAckData h2d _ => OutstandingAccessAckData h2d regs + | _ => repr + end + end. + + Instance tl_specification + : specification_for (tlul_adapter_reg (reg_count:=reg_count)) repr_state := + {| reset_repr := Idle; + + update_repr := update_repr_state; precondition := fun (input : denote_type (input_of tlul_adapter_reg)) - (repr : tlul_repr) => + (repr : repr_state) => let '(h2d, (regs, tt)) := input in reg_count = length regs /\ (a_valid h2d = true @@ -384,25 +396,14 @@ Section TLULSpec. postcondition := fun (input : denote_type (input_of (tlul_adapter_reg (reg_count:=reg_count)))) - (repr : tlul_repr) + (repr : repr_state) (output : denote_type (output_of (tlul_adapter_reg (reg_count:=reg_count)))) => - exists h2d regs d2h io_re io_we io_address io_data io_mask repr', + exists h2d regs repr' d2h io_re io_we io_address io_data io_mask, input = (h2d, (regs, tt)) - /\ repr' = - match repr with - | None => - if a_valid h2d then - if a_opcode h2d =? Get then - Some (OutstandingGet (a_source h2d) (a_size h2d)) - else if a_opcode h2d =? PutFullData then - Some (OutstandingPutFullData (a_source h2d)) - else (* unrechable *) repr - else None - | Some _ => if d_ready h2d then None else repr - end /\ output = (d2h, (io_re, (io_we, (io_address, (io_data, io_mask))))) + /\ repr' = update_repr_state input repr /\ match repr' with - | None => + | Idle => d_valid d2h = false /\ d_param d2h = 0 /\ d_sink d2h = 0 @@ -412,64 +413,68 @@ Section TLULSpec. /\ io_re = false /\ io_we = false - | Some (OutstandingGet reqid reqsz) => - d_valid d2h = true - /\ d_opcode d2h = AccessAckData - /\ d_param d2h = 0 - /\ d_size d2h = reqsz - /\ d_source d2h = reqid - /\ d_sink d2h = 0 - /\ d_data d2h = List.nth (N.to_nat (((a_address h2d / 4) mod (2 ^ 30)))) regs 0%N - /\ d_user d2h = 0 - /\ d_error d2h = false - /\ a_ready d2h = false - /\ match repr with - | None => if a_valid h2d then - io_re = true - /\ io_address = a_address h2d - else True - | _ => True - end - /\ io_we = false - - | Some (OutstandingPutFullData reqid) => - d_valid d2h = true - /\ d_opcode d2h = AccessAck - /\ d_param d2h = 0 - (* /\ d_size d2h = *) - /\ d_source d2h = reqid - /\ d_sink d2h = 0 - /\ d_user d2h = 0 - /\ d_error d2h = false - /\ a_ready d2h = false - /\ io_re = false - /\ match repr with - | None => if a_valid h2d then - io_we = true - /\ io_address = a_address h2d - /\ io_data = a_data h2d - /\ io_mask = a_mask h2d - else True - | _ => True - end - end + | OutstandingAccessAckData h2d regs => + d_valid d2h = true + /\ d_opcode d2h = AccessAckData + /\ d_param d2h = 0 + /\ d_size d2h = (a_size h2d) + /\ d_source d2h = (a_source h2d) + /\ d_sink d2h = 0 + /\ d_data d2h = (List.nth (N.to_nat ((((a_address h2d) / 4) mod (2 ^ 30)))) regs 0%N) + /\ d_user d2h = 0 + /\ d_error d2h = false + /\ a_ready d2h = false + /\ match repr with + | Idle => if a_valid h2d then + io_re = true + /\ io_address = a_address h2d + else io_re = false + | _ => io_re = false + end + /\ io_we = false + + | OutstandingAccessAck h2d => + d_valid d2h = true + /\ d_opcode d2h = AccessAck + /\ d_param d2h = 0 + (* /\ d_size d2h = *) + /\ d_source d2h = (a_source h2d) + /\ d_sink d2h = 0 + /\ d_user d2h = 0 + /\ d_error d2h = false + /\ a_ready d2h = false + /\ io_re = false + /\ match repr with + | Idle => if a_valid h2d then + io_we = true + /\ io_address = a_address h2d + /\ io_data = a_data h2d + /\ io_mask = a_mask h2d + else io_we = false + | _ => io_we = false + end + end; |}. - Global Instance tlul_invariant : invariant_for (tlul_adapter_reg (reg_count:=reg_count)) tlul_repr := + Global Instance tlul_invariant : invariant_for (tlul_adapter_reg (reg_count:=reg_count)) repr_state := fun (state : denote_type (state_of tlul_adapter_reg)) repr => tlul_adapter_reg_state_error state = false /\ match repr with - | None => + | Idle => tlul_adapter_reg_state_outstanding (reg_count:=reg_count) state = false - | Some (OutstandingGet reqid reqsz) => + | OutstandingAccessAckData h2d regs => tlul_adapter_reg_state_outstanding state = true - /\ tlul_adapter_reg_state_reqid state = reqid - /\ tlul_adapter_reg_state_reqsz state = reqsz + /\ tlul_adapter_reg_state_reqid state = (a_source h2d) + /\ tlul_adapter_reg_state_reqsz state = (a_size h2d) /\ tlul_adapter_reg_state_rspop state = AccessAckData - | Some (OutstandingPutFullData reqid) => + /\ tlul_adapter_reg_state_reqaddress state = (a_address h2d) + /\ reg_count = length regs + /\ a_opcode h2d = Get + | OutstandingAccessAck h2d => tlul_adapter_reg_state_outstanding state = true - /\ tlul_adapter_reg_state_reqid state = reqid + /\ tlul_adapter_reg_state_reqid state = (a_source h2d) /\ tlul_adapter_reg_state_rspop state = AccessAck + /\ a_opcode h2d = PutFullData end. Lemma tlul_adapter_reg_invariant_at_reset : invariant_at_reset tlul_adapter_reg. @@ -482,30 +487,26 @@ Section TLULSpec. Lemma tlul_adapter_reg_invariant_preserved : invariant_preserved tlul_adapter_reg. Proof. - intros (h2d, (regs, t)) state repr. destruct t. + intros (h2d & regs & t) state repr. destruct t. cbn in state. destruct_tlul_adapter_reg_state reg_count. destruct_tl_h2d. intros; subst. simplify_invariant (tlul_adapter_reg (reg_count:=reg_count)). simplify_spec (tlul_adapter_reg (reg_count:=reg_count)). - cbv [tlul_adapter_reg]. stepsimpl. logical_simplify. + cbv [tlul_adapter_reg]. stepsimpl. tlul_adapter_reg_state_simpl. tlsimpl. - match goal with - | h : reg_count = _ |- _ => clear h - end. + logical_simplify. repeat (destruct_pair_let; cbn [fst snd]). - destruct repr as [[|]|]; [| |]. - 1-2: (* repr = Some _ *) - logical_simplify; subst; - tlul_adapter_reg_state_simpl; boolsimpl; cbn [fst snd]; - destruct d_ready0; ssplit; reflexivity. - (* repr = None *) - subst. tlul_adapter_reg_state_simpl. boolsimpl. - destruct a_valid0; - try match goal with - | h: true = true -> _ |- _ => destruct h; subst - end; - cbn; ssplit; reflexivity. + tlul_adapter_reg_state_simpl. + subst. + ssplit. + - destruct (a_valid0 && negb outstanding)%bool; reflexivity. + - unfold update_repr_state. + destruct repr; [destruct a_valid0 | destruct d_ready0 ..]; + tlsimpl; boolsimpl. + 2-6: logical_simplify; subst outstanding; boolsimpl; ssplit; try reflexivity; assumption. + destruct H1; [reflexivity|..]; subst outstanding a_opcode0; cbn; [|auto]. + ssplit; try reflexivity; assumption. Qed. Lemma tlul_adapter_reg_output_correct : output_correct tlul_adapter_reg. @@ -519,42 +520,29 @@ Section TLULSpec. simplify_spec (tlul_adapter_reg (reg_count:=reg_count)). cbv [tlul_adapter_reg]. stepsimpl. logical_simplify. tlul_adapter_reg_state_simpl. tlsimpl. - rewrite List.resize_noop by assumption. - match goal with - | h : reg_count = _ |- _ => clear h - end. + (* match goal with *) + (* | h : reg_count = _ |- _ => clear h *) + (* end. *) subst. repeat (destruct_pair_let; cbn [fst snd]). - destruct repr as [repr'|]. - - (* repr = Some _ *) - destruct repr'; logical_simplify; subst; boolsimpl; - eexists _, _, _, _, _, _, _, _, _; - cbn -[N.ones]; repeat (rewrite pair_equal_spec); - tlsimpl; ssplit; try reflexivity; - destruct d_ready0; simpl; ssplit; auto; []. - rewrite N.land_ones. - replace 4 with (2 ^ 2) by reflexivity. - rewrite <- ! N.shiftr_div_pow2. - reflexivity. - - (* repr = None *) - subst. - eexists _, _, _, _, _, _, _, _, _. - cbn -[N.ones]. repeat (rewrite pair_equal_spec). - tlsimpl. ssplit; try reflexivity; []. - destruct a_valid0; simpl; ssplit; try reflexivity; []. - match goal with - | h: true = true -> _ |- _ => - destruct h; [reflexivity|..] - end; subst; simpl; ssplit; try reflexivity; []. - rewrite N.land_ones. - replace 4 with (2 ^ 2) by reflexivity. - rewrite <- ! N.shiftr_div_pow2. - reflexivity. + destruct repr; destruct a_valid0; destruct d_ready0; + tlsimpl; boolsimpl; subst. + all: try match goal with + | H: true = true -> _ |- _ => + destruct H; [auto|subst..] + end. + all: logical_simplify; subst; boolsimpl. + all: repeat eexists; cbn. + all: rewrite List.resize_noop by assumption. + all: change 1073741823 with (N.ones 30); + rewrite N.land_ones; + replace 4 with (2 ^ 2) by reflexivity; + rewrite <- ! N.shiftr_div_pow2; + try reflexivity. Qed. Existing Instances tlul_adapter_reg_invariant_at_reset tlul_adapter_reg_invariant_preserved tlul_adapter_reg_output_correct. Global Instance tlul_adapter_reg_correctness : correctness_for tlul_adapter_reg. Proof. constructor; typeclasses eauto. Defined. - -End TLULSpec. +End TLSpec. diff --git a/firmware/IncrementWait/CavaIncrementDevice.v b/firmware/IncrementWait/CavaIncrementDevice.v index cd46ee314..aa029cc17 100644 --- a/firmware/IncrementWait/CavaIncrementDevice.v +++ b/firmware/IncrementWait/CavaIncrementDevice.v @@ -1,219 +1,95 @@ -From Coq Require Import - Lists.List - ZArith.ZArith. - -Import ListNotations. - -From Cava Require Import - Expr - Primitives - Semantics - TLUL - Types - Util.BitArithmetic. - -Section Var. - Import ExprNotations. - Import PrimitiveNotations. - - Local Open Scope N. - - Context {var : tvar}. - - Definition incr_state := BitVec 2. - Definition Idle := Constant incr_state 0. - Definition Busy1 := Constant incr_state 1. - Definition Busy2 := Constant incr_state 2. - Definition Done := Constant incr_state 3. - - Definition incr - : Circuit _ [tl_h2d_t] tl_d2h_t - := {{ - fun tl_h2d => - (* Destruct and reassemble tl_h2d with a_address that matches the - tlul_adapter_reg interface. *) - let '(a_valid - , a_opcode - , a_param - , a_size - , a_source - , a_address - , a_mask - , a_data - , a_user - ; d_ready) := tl_h2d in - (* Bit #2 of the address determines which register is being accessed - (STATUS or VALUE). Zero out the other bits. *) - let a_address := a_address & (`K 1` << 2) in - let tl_h2d := (a_valid - , a_opcode - , a_param - , a_size - , a_source - , a_address - , a_mask - , a_data - , a_user - , d_ready) in - - let/delay '(istate, value; tl_d2h) := - (* Compute the value of the status register *) - let status := - if istate == `Done` then `K 4` - else if istate == `Busy1` || istate == `Busy2` then `K 2` - else (* istate == `Idle` *) `K 1` in - - (* Handle the input: - - a_opcode = Get: the adapter will do all the work; - - a_opcode = PutFullData: further handling is needed, the adapter - will output more info to req. *) - let '(tl_d2h'; req) := `tlul_adapter_reg` tl_h2d (value :> status :> []) in - let '(is_read - , is_write - , address - , write_data - ; _write_mask) := req in - - let istate' := - if istate == `Busy1` then `Busy2` - else if istate == `Busy2` then `Done` - else if istate == `Done` then - if is_read && address == `K 0` then `Idle` - else `Done` - else (* istate == `Idle` *) - if is_write then `Busy1` - else `Idle` in - - let value' := - if istate == `Busy2` then value + `K 1` - else if istate == `Idle` then write_data - else value in - - (istate', value', tl_d2h') - initially (0, - (0, - (false, (0, (0, (0, (0, (0, (0, (0, (false, false))))))))))) - : denote_type (incr_state ** BitVec 32 ** tl_d2h_t) - in - - tl_d2h - }}. -End Var. - -Example sample_trace := - Eval compute in - let nop := set_d_ready true tl_h2d_default in - let read_reg (r : N) := - set_a_valid true - (set_a_opcode Get - (set_a_size 2%N - (set_a_address r - (set_d_ready true tl_h2d_default)))) in - let write_val (v : N) := - set_a_valid true - (set_a_opcode PutFullData - (set_a_size 2%N - (set_a_address 0%N (* value-ref *) - (set_a_data v - (set_d_ready true tl_h2d_default))))) in - - simulate incr - [ (nop, tt) - ; (read_reg 4, tt) (* status *) - ; (nop, tt) - ; (write_val 42, tt) - ; (nop, tt) - ; (nop, tt) - ; (read_reg 4, tt) (* status *) - ; (nop, tt) - ; (read_reg 0, tt) (* value *) - ; (nop, tt) - ; (read_reg 4, tt) (* status *) - ]%N. -(* Print sample_trace. *) - +Require Import Coq.Lists.List. Require Import Coq.micromega.Lia. - -Require Import riscv.Utility.Utility. +Require Import Coq.ZArith.ZArith. + +Require Import Cava.Expr. +Require Import Cava.ExprProperties. +Require Import Cava.Invariant. +Require Import Cava.Primitives. +Require Import Cava.Semantics. +Require Import Cava.TLUL. +Require Import Cava.Types. +Require Import Cava.Util.BitArithmetic. +Require Import Cava.Util.List. +Require Import Cava.Util.Tactics. Require Import coqutil.Map.Interface coqutil.Map.Properties. -Require Import coqutil.Word.Interface coqutil.Word.Properties. -Require Import coqutil.Tactics.Tactics. Require Import coqutil.Tactics.Simp. +Require Import coqutil.Tactics.Tactics. +Require Import coqutil.Word.Interface coqutil.Word.Properties. + +Require Import riscv.Utility.Utility. Require Import bedrock2.ZnWords. Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.InternalMMIOMachine. Require Import Bedrock2Experiments.IncrementWait.Constants. +Require Import Bedrock2Experiments.IncrementWait.Incr. Require Import Bedrock2Experiments.IncrementWait.IncrementWaitSemantics. Require Import Bedrock2Experiments.StateMachineSemantics. Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.MMIOToCava. -Require Import Cava.Util.Tactics. +Import ListNotations. Section WithParameters. Instance var : tvar := denote_type. + Existing Instance Incr.inner_specification. + Existing Instance Incr.inner_correctness. + Existing Instance Incr.inner_invariant. + + Existing Instance TLUL.tl_specification. + Existing Instance TLUL.tlul_invariant. + Existing Instance TLUL.tlul_adapter_reg_correctness. + + Existing Instance incr_specification. + Existing Instance incr_invariant. + Existing Instance incr_correctness. + Context {word: Interface.word 32} {word_ok: word.ok word} {Mem: map.map word byte} {Registers: map.map Z word}. - Definition consistent_states - '((reqid, (reqsz, (rspop, (error, (outstanding, (_we_o, _re_o)))))) - : denote_type (state_of (tlul_adapter_reg (reg_count := 2)))) - '((d_valid, (d_opcode, (d_param, (d_size, (d_source, (d_sink, (d_data, (d_user, (d_error, a_ready))))))))) - : denote_type tl_d2h_t) - : Prop := - d_valid = outstanding /\ - d_opcode = rspop /\ - (* d_param = 0 /\ *) - d_size = reqsz /\ - d_source = reqid /\ - (* d_sink = 0 /\ *) - (* d_data = ?? *) - (* d_user = 0 /\ *) - d_error = error /\ - a_ready = negb outstanding. - - Definition mk_counter_state (istate : N) (val : N) tl_d2h tlul_state - : denote_type (state_of incr) := - ((istate, (val, tl_d2h)), tlul_state). - Global Instance counter_device: device := {| device.state := denote_type (state_of incr); - device.is_ready_state s := exists val tl_d2h tlul_state, - consistent_states tlul_state tl_d2h - /\ s = mk_counter_state 0 val tl_d2h tlul_state; - device.run1 s i := Semantics.step incr s (i, tt); + + device.is_ready_state s := exists r_regs r_tl r_inner, + incr_invariant s (ReprIdle, r_regs, r_tl, r_inner); + + device.last_d2h '((_, (_, (_, d2h))), _) := d2h; + + device.run1 s i := fst (Semantics.step incr s (i, tt)); + device.addr_range_start := INCR_BASE_ADDR; device.addr_range_pastend := INCR_END_ADDR; - device.maxRespDelay := 1; + + device.maxRespDelay '((_, (_, (_, d2h))), _) := + if a_ready d2h then 0 else 1; |}. (* conservative upper bound matching the instance given in IncrementWaitToRiscv *) Global Instance circuit_spec : circuit_behavior := {| ncycles_processing := 15%nat |}. - Inductive counter_related: IncrementWaitSemantics.state -> denote_type (state_of incr) -> Prop := - | IDLE_related: forall val tl_d2h tlul_state, - consistent_states tlul_state tl_d2h -> - counter_related IDLE (mk_counter_state 0 val tl_d2h tlul_state) - | BUSY1_related: forall val tl_d2h tlul_state ncycles, - (1 < ncycles)%nat -> - consistent_states tlul_state tl_d2h -> - counter_related (BUSY val ncycles) (mk_counter_state 1 (word_to_N val) tl_d2h tlul_state) - | BUSY2_related: forall val tl_d2h tlul_state ncycles, - (0 < ncycles)%nat -> - consistent_states tlul_state tl_d2h -> - counter_related (BUSY val ncycles) (mk_counter_state 2 (word_to_N val) tl_d2h tlul_state) + + Inductive counter_related_spec: IncrementWaitSemantics.state -> Incr.repr_state -> Prop := + | IDLE_related: counter_related_spec IDLE ReprIdle + | BUSY_related: forall val ncycles count, + (0 < count <= 2)%nat -> + (2 < ncycles + count)%nat -> + counter_related_spec (BUSY val ncycles) (ReprBusy (word_to_N val) count) (* the hardware is already done, but the software hasn't polled it yet to find out, so we have to relate a software-BUSY to a hardware-done: *) - | BUSY_done_related: forall val tl_d2h tlul_state ncycles, - consistent_states tlul_state tl_d2h -> - counter_related (BUSY val ncycles) - (mk_counter_state 3 (word_to_N (word.add (word.of_Z 1) val)) tl_d2h tlul_state) - | DONE_related: forall val tl_d2h tlul_state, - consistent_states tlul_state tl_d2h -> - counter_related (DONE val) (mk_counter_state 3 (word_to_N val) tl_d2h tlul_state). + | BUSY_done_related: forall val ncycles, + counter_related_spec (BUSY val ncycles) (ReprDone (word_to_N (word.add (word.of_Z 1) val))) + | DONE_related: forall val, + counter_related_spec (DONE val) (ReprDone (word_to_N val)). + + Definition counter_related {invariant : invariant_for incr repr} (sH : IncrementWaitSemantics.state) + (sL : denote_type (state_of incr)) (inflight_h2ds : list tl_h2d) : Prop := + exists r_state r_regs r_tl r_inner, + inflight_h2ds = [] /\ + counter_related_spec sH r_state /\ + invariant sL (r_state, r_regs, r_tl, r_inner). (* This should be in bedrock2.ZnWords. It is use by ZnWords, which is used in the two following Lemmas. *) @@ -227,160 +103,209 @@ Section WithParameters. (0 <= x < 2 ^ 32)%Z -> word_to_N (word.of_Z x) = Z.to_N x. Proof. intros. unfold word_to_N. ZnWords. Qed. - Set Printing Depth 100000. - - Ltac destruct_pair_let_hyp := - match goal with - | H: context [ match ?p with - | pair _ _ => _ - end ] |- _ => - destruct p as [?p0 ?p1] eqn:?H0 - end. + Lemma N_to_word_word_to_N: forall v, N_to_word (word_to_N v) = v. + Proof. intros. unfold N_to_word, word_to_N. ZnWords. Qed. - Ltac destruct_pair_equal_hyp := + Ltac use_spec := match goal with - | H: context [ (?l0, ?l1) = (?r0, ?r1) ] |- _ => - eapply pair_equal_spec in H; destruct H as [?H0 ?H1] + | Hrun: device.run1 ?sL ?input = ?sL', + Hinv: incr_invariant ?sL ?repr + |- _ => + assert (Hprec: precondition incr (input, tt) repr); + [ simplify_spec (incr (var:=var)); simplify_spec (tlul_adapter_reg (reg_count:=2)); simplify_spec (Incr.inner (var:=var)); + simplify_invariant (incr (var:=var)); + cbn in sL; destruct sL as ((?busy, (?done, (?regs, ?d2h))), (?s_tl, ?s_inner)); + destruct_tl_h2d; tlsimpl; logical_simplify; subst; + ssplit; intros; try discriminate; auto + + | remember (update_repr (c:=incr) (input, tt) repr) as repr' eqn:Erepr'; + (* pose proof (output_correct_pf (c:=incr) (input, tt) sL repr Hinv Hprec) as Hpostc. *) + pose proof (invariant_preserved_pf (c:=incr) (input, tt) sL repr repr' Erepr' Hinv Hprec) as Hinv'; + unfold device.run1, counter_device in Hrun; + match type of Hrun with + | fst ?step = _ => + remember step as res eqn:Hstep; + destruct res as (?sL'' & ?d2h); + cbn in Hrun; subst sL''; clear Hstep + end; + cbn [fst] in Hinv'; + destruct repr' as (((?r_state, ?r_regs), ?r_tl), ?r_inner)] end. - Ltac destruct_tlul_adapter_reg_state := + Ltac inversion_rel_spec := match goal with - | H : N * (N * (N * (bool * (bool * (bool * bool))))) |- _ => - destruct H as [?reqid [?reqsz [?rspop [?error [?outstanding [?we_o ?re_o]]]]]] + | H: counter_related_spec _ _ |- _ => inversion H; subst end. - Ltac destruct_consistent_states := + Ltac simplify_tl_repr := + unfold device.maxRespDelay, device.last_d2h, counter_device in *; + repeat match goal with + | sL: device.state |- _ => + cbn in sL; destruct sL as ((?busy, (?done, (?regs, ?d2h))), (?s_tl, ?s_inner)) + end; + destruct_tl_h2d; destruct_tl_d2h; tlsimpl; logical_simplify; subst; + simplify_invariant (incr (var:=var)); match goal with - | H : consistent_states _ _ |- _ => - destruct H as (Hvalid & Hopcode & Hsize & Hsource & Herror & Hready) - end. + | H: _ = update_repr _ (_, _, ?r_tl, _) |- _ => + destruct r_tl; logical_simplify; tlsimpl; subst; + (* logical_simplify; subst; *) + cbn in H; rewrite ? Z_word_N in H by lia; cbn in H + end; + logical_simplify; subst; + cbn; rewrite ? Z_word_N by lia; cbn; + change (Pos.to_nat 1) with 1; + repeat match goal with + | H: length ?regs = 2 |- _ => + destruct regs as [|? [|? [|]]]; cbn in H; try discriminate H; clear H; + cbn [nth] in *; subst + end; + try discriminate. - Lemma N_to_word_word_to_N: forall v, N_to_word (word_to_N v) = v. - Proof. intros. unfold N_to_word, word_to_N. ZnWords. Qed. - - (* Set Printing All. *) Global Instance cava_counter_satisfies_state_machine: device_implements_state_machine counter_device increment_wait_state_machine. Proof. - eapply Build_device_implements_state_machine with (device_state_related := counter_related); - intros. + eapply Build_device_implements_state_machine with (device_state_related := counter_related). - (* mmioAddrs_match: *) reflexivity. - (* initial_state_is_ready_state: *) - simpl in *. subst. inversion H0. subst. eexists _, _, _. eauto. + intros. + unfold device.is_ready_state, counter_device, counter_related in *; + logical_simplify. + cbn in *; subst. + inversion_rel_spec; repeat eexists; eassumption. - (* initial_states_are_related: *) - simpl in *. destruct H0 as (val & tl_d2h & tlul_state & H0 & H1). subst. - eauto using IDLE_related. + intros. + cbn in *; logical_simplify; subst. + unfold counter_related; repeat eexists; [|eassumption]. + apply IDLE_related. - (* initial_state_exists: *) - simpl in *. destruct H as (val & tl_d2h & tlul_state & H0 & H1). subst. - eauto using IDLE_related. + intros. + cbn in *; logical_simplify; subst. + unfold counter_related; repeat eexists; [|eassumption]. + apply IDLE_related. - (* nonMMIO_device_step_preserves_state_machine_state: *) - simpl in sL1, sL2. - destruct_tl_h2d. simpl in H. subst. - cbn in H1. - repeat (destruct_pair_let_hyp; - repeat (destruct_pair_equal_hyp; subst; cbn [fst snd])). - inversion H0; subst; - try (rewrite incrN_word_to_bv); - try (constructor; try lia; simpl; boolsimpl; ssplit; reflexivity). - - (* state_machine_read_to_device_read: *) - (* simpler because device.maxRespDelay=1 *) - unfold device.maxRespDelay, device.runUntilResp, device.state, device.run1, counter_device. - unfold state_machine.read_step, increment_wait_state_machine, read_step in *. - simpl in sL. destruct sL as ((istate & value & tl_d2h) & tlul_state). - destruct_tl_d2h. destruct_tlul_adapter_reg_state. - destruct H as [v [sH' [Hbytes H]]]. rewrite Hbytes. - destruct r; simp; [|]. - + (* r=VALUE *) - destruct_consistent_states. subst. - repeat (rewrite Z_word_N by lia; cbn). - destruct outstanding; [|]; - eexists _, _, _; ssplit; try reflexivity; cbn; rewrite Z_word_N by lia; - try (eapply IDLE_related; unfold consistent_states; ssplit; reflexivity); - try (apply N_to_word_word_to_N). - + (* r=STATUS *) - destruct sH; [| |]. - * (* sH=IDLE *) - inversion H0. subst. - destruct_consistent_states. subst. cbn. - repeat (rewrite Z_word_N by lia; cbn). - unfold status_value, STATUS_IDLE, N_to_word, word_to_N. - destruct outstanding; eexists _, _, _; ssplit; try reflexivity; - try (apply IDLE_related; simpl; ssplit; reflexivity); - try (simpl; unfold N_to_word; ZnWords). - * (* sH=BUSY *) - simpl. - unfold STATUS_ADDR, INCR_BASE_ADDR, N_to_word, word_to_N, status_value, STATUS_BUSY. - rewrite word.unsigned_of_Z. unfold word.wrap. - inversion H0; subst; [| |]. - -- (* BUSY1_related *) - destruct outstanding; eexists _, _, _; simpl; [|]. - ++ ssplit; try reflexivity; [|]. - ** rewrite incrN_word_to_bv. - apply BUSY_done_related; unfold consistent_states; ssplit; reflexivity. - ** right. eexists. ssplit; try reflexivity; [|]. - --- apply Nat.pred_inj; try lia. rewrite Nat.pred_succ. reflexivity. - --- simpl. ZnWords. - ++ ssplit; try reflexivity; [|]. - ** apply BUSY2_related. 1: shelve. unfold consistent_states. ssplit; reflexivity. - ** right. eexists. ssplit; try reflexivity; [|]. - --- apply Nat.pred_inj; try lia. rewrite Nat.pred_succ. reflexivity. - --- simpl. ZnWords. - Unshelve. lia. - -- (* BUSY2_related *) - destruct outstanding; eexists _, _, _; simpl; [|]. - ++ ssplit; try reflexivity; [|]. - ** rewrite incrN_word_to_bv. - apply DONE_related; unfold consistent_states; ssplit; reflexivity. - ** left. simpl. ssplit; try reflexivity. ZnWords. - ++ ssplit; try reflexivity; [|]. - ** rewrite incrN_word_to_bv. - apply BUSY_done_related; unfold consistent_states; ssplit; reflexivity. - ** right. eexists. ssplit; try reflexivity; [|]. - --- apply Nat.pred_inj; try lia. rewrite Nat.pred_succ. reflexivity. - --- simpl. ZnWords. - -- (* BUSY_done_related *) - (* the transition that was used to show that sH is not stuck was *) - (* a transition from BUSY to BUSY returning a busy flag, but *) - (* since the device already is in done state, it will return a *) - (* done flag in this transition, so the transition we use to *) - (* simulate what happened in the device is a BUSY-to-DONE *) - (* transition returning a done flag instead of a BUSY-to-BUSY *) - (* transition returning a busy flag. *) - destruct outstanding; eexists _, _, _; boolsimpl; simpl; - ssplit; try reflexivity; - try (apply DONE_related; unfold consistent_states; ssplit; reflexivity); - try (left; split; try reflexivity; simpl; ZnWords). - * (* sH=DONE *) - simpl. - unfold STATUS_ADDR, INCR_BASE_ADDR, N_to_word, word_to_N, status_value, STATUS_BUSY. - rewrite !word.unsigned_of_Z. unfold word.wrap. - inversion H0. subst. - destruct outstanding; eexists _, _, _; boolsimpl; simpl; - ssplit; try reflexivity; - try (eapply DONE_related; unfold consistent_states; ssplit; reflexivity); - try (simpl; ZnWords). - - (* state_machine_write_to_device_write: *) - destruct H as (sH' & ? & ?). subst. - unfold write_step in H1. - destruct r. 2: contradiction. - destruct sH; try contradiction. subst. - inversion H0. simpl in tl_d2h. simpl in tlul_state. - destruct_tl_d2h. destruct_tlul_adapter_reg_state. subst. cbn. - unfold word_to_N. - rewrite word.unsigned_of_Z_nowrap by (cbv; intuition discriminate). - destruct outstanding; boolsimpl; simpl; - eexists _, _, _; ssplit; try reflexivity; try assumption; apply BUSY1_related; - try lia; - try (unfold consistent_states; ssplit; reflexivity). + intros. + logical_simplify. + unfold counter_related in *; logical_simplify. + use_spec. clear Hprec. + repeat eexists; [|eassumption]. + inversion_rel_spec; simplify_tl_repr; + destruct d_ready; logical_simplify; subst; try constructor; + (destruct count as [|[|[|]]]; [exfalso; lia|..|exfalso; lia]); + rewrite ? incrN_word_to_bv; constructor; lia. + + - (* [state_machine_read_to_device_send_read_or_later] *) + intros ? ? ? ? ? ? [v [sH'' [Hpow2 Hex_read]]] **. + rewrite Hpow2. clear Hpow2. + unfold counter_related in *. cbn in Hex_read. logical_simplify. + use_spec. clear Hprec. + + destruct_one_match; [destruct_one_match|]. + { (* case 1: device ready, valid response *) + destruct r. + - (* [r:=VALUE] *) + inversion_rel_spec; destruct Hex_read; subst. + eexists; split; [|cbn; ssplit; try reflexivity]. + + repeat eexists; [|eassumption]. + simplify_tl_repr; constructor. + + simplify_tl_repr. + apply N_to_word_word_to_N. + - (* [r:=STATUS] *) + inversion_rel_spec. + + eexists; split; [repeat eexists; [|eassumption]|cbn; ssplit; try reflexivity]; + simplify_tl_repr. + * constructor. + * unfold N_to_word, status_value; ZnWords. + + + destruct ncycles as [|]; [exfalso; lia|]. + eexists; split; [repeat eexists; [|eassumption]|cbn; ssplit; try reflexivity]; + simplify_tl_repr. + * destruct count as [|[|[|]]]; [exfalso; lia|..|exfalso; lia]. + -- apply BUSY_related with (ncycles:=ncycles); lia. + -- rewrite incrN_word_to_bv; apply BUSY_done_related. + * right. eexists; ssplit; try reflexivity. + unfold N_to_word, status_value; ZnWords. + + + eexists; split; [repeat eexists; [|eassumption]|cbn; ssplit; try reflexivity]; + simplify_tl_repr. + * apply DONE_related. + * left. split; [|reflexivity]. + unfold N_to_word, status_value; ZnWords. + + + eexists; split; [repeat eexists; [|eassumption]|cbn; ssplit; try reflexivity]; + simplify_tl_repr. + * apply DONE_related. + * unfold N_to_word, status_value; ZnWords. + } + + { (* case 2: device ready, no valid response *) + exfalso; simplify_tl_repr. + } + + { (* case 3: device not ready *) + ssplit. + - repeat eexists; [|eassumption]. + inversion_rel_spec; simplify_tl_repr; + rewrite ? incrN_word_to_bv; try (constructor; lia). + all: destruct count as [|[|[|]]]; [exfalso; lia + |apply BUSY_related with (ncycles:=ncycles); lia + |apply BUSY_done_related + |exfalso; lia]. + - simplify_tl_repr; lia. + } + + - (* [state_machine_read_to_device_ack_read_or_later] *) + intros. + unfold counter_related in *; logical_simplify. + discriminate. + + - (* [state_machine_write_to_device_send_write_or_later] *) + intros ? ? ? ? ? ? ? [sH'' [Hpow2 Hex_write]] **. + rewrite Hpow2. clear Hpow2. + unfold counter_related in *. logical_simplify. + use_spec. clear Hprec. + destruct_one_match; [destruct_one_match|]. + + { (* case 1: device ready, valid response *) + destruct r. + + (* [r:=VALUE] *) + inversion_rel_spec; destruct Hex_write; subst. + eexists; split; [|cbn; ssplit; try reflexivity]. + repeat eexists; [|eassumption]. + simplify_tl_repr; constructor; lia. + + (* [r:=STATUS] *) + destruct Hex_write. + } + + { (* case 2: device ready, no valid response *) + exfalso; simplify_tl_repr. + } + + { (* case 3: device not ready *) + ssplit. + - repeat eexists; [|eassumption]. + inversion_rel_spec; simplify_tl_repr; + rewrite ? incrN_word_to_bv; try (constructor; lia). + all: destruct count as [|[|[|]]]; [exfalso; lia + |apply BUSY_related with (ncycles:=ncycles); lia + |apply BUSY_done_related + |exfalso; lia]. + - simplify_tl_repr; lia. + } + + - (* [state_machine_write_to_device_ack_write_or_later] *) + intros. + unfold counter_related in *; logical_simplify. + discriminate. + - (* read_step_unique: *) - simpl in *. unfold read_step in *. simp. + intros. simpl in *. unfold read_step in *. simp. destruct v; destruct r; try contradiction; simp; try reflexivity. destruct Hp1; destruct H0p1; simp; try reflexivity; unfold status_value in *; exfalso; ZnWords. - (* write_step_unique: *) - simpl in *. unfold write_step in *. simp. subst. reflexivity. + intros. simpl in *. unfold write_step in *. simp. subst. reflexivity. - (* initial_state_unique: *) - simpl in *. subst. reflexivity. + intros. simpl in *. subst. reflexivity. Qed. End WithParameters. diff --git a/firmware/IncrementWait/Incr.v b/firmware/IncrementWait/Incr.v new file mode 100644 index 000000000..0945d1e3e --- /dev/null +++ b/firmware/IncrementWait/Incr.v @@ -0,0 +1,528 @@ +Require Import Coq.Lists.List. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. + +Require Import Cava.Expr. +Require Import Cava.ExprProperties. +Require Import Cava.Invariant. +Require Import Cava.Primitives. +Require Import Cava.Semantics. +Require Import Cava.TLUL. +Require Import Cava.Types. +Require Import Cava.Util.BitArithmetic. +Require Import Cava.Util.List. +Require Import Cava.Util.Tactics. + +Require Import coqutil.Tactics.Simp. +Require Import coqutil.Tactics.Tactics. + +Import ListNotations. + +Section Var. + Import Expr. + Import ExprNotations. + Import PrimitiveNotations. + + Local Open Scope N. + + Context {var : tvar}. + + Definition incr_state := BitVec 2. + Definition Idle := Constant incr_state 0. + Definition Busy1 := Constant incr_state 1. + Definition Busy2 := Constant incr_state 2. + Definition Done := Constant incr_state 3. + + Definition inner + : Circuit _ [Bit; BitVec 32] (Bit ** BitVec 32) + := {{ + fun valid data => + let/delay '(istate; value) := + let istate' := + if istate == `Busy1` then `Busy2` + else if istate == `Busy2` then `Done` + else if istate == `Done` then `Idle` + else (* istate == `Idle` *) + if valid then `Busy1` + else `Idle` in + + let value' := + if istate == `Busy2` then value + `K 1` + else if istate == `Idle` then data + else value in + + (istate', value') + initially default + : denote_type (incr_state ** BitVec 32) + in + (istate == `Done`, value) + }}. + + Definition incr + : Circuit _ [tl_h2d_t] tl_d2h_t + := {{ + fun tl_h2d => + (* Destruct and reassemble tl_h2d with a_address that matches the + tlul_adapter_reg interface. *) + let '(a_valid + , a_opcode + , a_param + , a_size + , a_source + , a_address + , a_mask + , a_data + , a_user + ; d_ready) := tl_h2d in + (* Bit #2 of the address determines which register is being accessed *) + (* (STATUS or VALUE). Zero out the other bits. *) + let a_address := a_address & (`K 1` << 2) in + let tl_h2d := (a_valid + , a_opcode + , a_param + , a_size + , a_source + , a_address + , a_mask + , a_data + , a_user + , d_ready) in + + let/delay '(busy, done, registers; tl_d2h) := + let '(tl_d2h'; req) := `tlul_adapter_reg` tl_h2d registers in + let '(is_read, is_write, address, write_data; _write_mask) := req in + + let '(inner_res_valid; inner_res) := `inner` (!busy && !done && is_write) write_data in + + let busy' := + if busy then !inner_res_valid + else !done && is_write in + + let done' := + if busy then inner_res_valid + else if done then !(is_read && address == `K 0`) + else done in + + let registers' := + if inner_res_valid then `replace` registers `K (sz:=1) 0` inner_res + else registers in + + let registers' := + if busy' then `replace` registers' `K (sz:=1) 1` `K 2` + else if done' then `replace` registers' `K (sz:=1) 1` `K 4` + else `replace` registers' `K (sz:=1) 1` `K 1` in + + (busy', done', registers', tl_d2h') initially + (false, (false, ([0; 1], set_a_ready true (default (t:=tl_d2h_t))))) + : denote_type (Bit ** Bit ** Vec (BitVec 32) 2 ** tl_d2h_t) + in + + tl_d2h + }}. +End Var. + +Definition sim {s i o} (c : Circuit s i o) (input : list (denote_type i)) + : list (denote_type s * denote_type i * denote_type o) := + fst (List.fold_left (fun '(acc, s) i => + let '(s', o) := step c s i in + (acc ++ [(s, i, o)], s')) + input + ([], reset_state c)). + +Example sample_trace := + Eval compute in + let nop := set_d_ready true tl_h2d_default in + let read_reg (r : N) := + set_a_valid true + (set_a_opcode Get + (set_a_size 2%N + (set_a_address r + (set_d_ready true tl_h2d_default)))) in + let write_val (v : N) := + set_a_valid true + (set_a_opcode PutFullData + (set_a_size 2%N + (set_a_address 0%N (* value-ref *) + (set_a_data v + (set_d_ready true tl_h2d_default))))) in + + sim incr + [ (nop, tt) + ; (read_reg 4, tt) (* status *) + ; (nop, tt) + ; (write_val 42, tt) + ; (nop, tt) + ; (nop, tt) + ; (read_reg 4, tt) (* status *) + ; (nop, tt) + ; (read_reg 0, tt) (* value *) + ; (nop, tt) + ; (read_reg 4, tt) (* status *) + ]%N. +(* Print sample_trace. *) + +Section Spec. + Local Open Scope N. + + Variant repr_state := + | ReprIdle + | ReprBusy (data : N) (count : nat) + | ReprDone (res : N). + + Notation inner_repr := repr_state. + + Global Instance inner_invariant : invariant_for inner inner_repr := + fun (state : denote_type (state_of inner)) repr => + let '(istate, value) := state in + match repr with + | ReprIdle => istate = 0 + | ReprBusy data c => (0 < c <= 2)%nat /\ istate = N.of_nat c /\ value = data + | ReprDone res => istate = 3 /\ value = res + end. + + Definition inner_spec_step (input : denote_type (input_of inner)) repr := + let '(valid, (data, tt)) := input in + match repr with + | ReprIdle => if valid then ReprBusy data 1 else ReprIdle + | ReprBusy data 2 => ReprDone ((data + 1) mod 2^32) + | ReprBusy data c => ReprBusy data (c + 1) + | ReprDone _ => ReprIdle + end. + + Instance inner_specification + : specification_for inner inner_repr := + {| reset_repr := ReprIdle; + + update_repr := + fun (input : denote_type (input_of inner)) repr => + inner_spec_step input repr; + + precondition := + fun (input : denote_type (input_of inner)) repr => True; + + postcondition := + fun (input : denote_type (input_of inner)) repr + (output : denote_type (output_of inner)) => + let repr' := inner_spec_step input repr in + match repr' with + | ReprDone res => output = (true, res) + | _ => exists res, output = (false, res) + end; + |}. + + Lemma inner_invariant_at_reset : invariant_at_reset inner. + Proof. + simplify_invariant inner. reflexivity. + Qed. + + Lemma inner_invariant_preserved : invariant_preserved inner. + Proof. + intros (valid, (data, t)) state repr. destruct t. + cbn in * |-. destruct state as (istate, value). + intros repr' ? Hinvar Hprec; subst. + simplify_invariant inner. + simplify_spec inner. + cbv [inner inner_spec_step]. stepsimpl. + repeat (destruct_pair_let; cbn [fst snd]). + destruct repr as [|? iiscount|?]; logical_simplify; subst. + - destruct valid; cbn; ssplit; lia. + - destruct iiscount as [|[|[|iiscount]]]; cbn; ssplit; lia. + - reflexivity. + Qed. + + Lemma inner_output_correct : output_correct inner. + Proof. + intros (valid, (data, t)) state repr. destruct t. + cbn in * |-. destruct state as (istate, value). + remember (update_repr (c:=inner) (valid, (data, tt)) repr) as repr'. + intros Hinvar Hprec. + simplify_invariant inner. + simplify_spec inner. + cbv [inner inner_spec_step]. stepsimpl. + repeat (destruct_pair_let; cbn [fst snd]). + destruct repr as [|? iiscount|?]; logical_simplify; subst. + - destruct valid; eexists; cbn; ssplit; reflexivity. + - destruct iiscount as [|[|[|iiscount]]]; try lia; eexists; reflexivity. + - eexists. reflexivity. + Qed. + + Existing Instances inner_invariant_at_reset inner_invariant_preserved + inner_output_correct. + Global Instance inner_correctness : correctness_for inner. + Proof. constructor; typeclasses eauto. Defined. + + Definition repr := (repr_state * list N * TLUL.repr_state * inner_repr)%type. + + Global Instance incr_invariant : invariant_for incr repr := + fun (state : denote_type (state_of incr)) repr => + let '((s_busy, (s_done, (s_regs, s_d2h))), (s_tlul, s_inner)) := state in + let '(r_state, r_regs, r_tl, r_inner) := repr in + tlul_invariant (reg_count:=2) s_tlul r_tl + /\ match r_tl with + | TLUL.Idle => + d_valid s_d2h = false + /\ d_error s_d2h = false + /\ a_ready s_d2h = true + | TLUL.OutstandingAccessAckData h2d regs => + d_valid s_d2h = true + /\ d_opcode s_d2h = AccessAckData + /\ d_param s_d2h = 0 + /\ d_size s_d2h = (a_size h2d) + /\ d_source s_d2h = (a_source h2d) + /\ d_sink s_d2h = 0 + /\ d_data s_d2h = (List.nth (N.to_nat ((((a_address h2d) / 4) mod (2 ^ 30)))) regs 0%N) + /\ d_user s_d2h = 0 + /\ d_error s_d2h = false + /\ a_ready s_d2h = false + | TLUL.OutstandingAccessAck h2d => + d_valid s_d2h = true + /\ d_opcode s_d2h = AccessAck + /\ d_param s_d2h = 0 + (* /\ d_size s_d2h = *) + /\ d_source s_d2h = (a_source h2d) + /\ d_sink s_d2h = 0 + /\ d_user s_d2h = 0 + /\ d_error s_d2h = false + /\ a_ready s_d2h = false + end + /\ inner_invariant s_inner r_inner + /\ match r_state with + | ReprIdle => s_busy = false /\ s_done = false + /\ r_inner = ReprIdle + /\ nth 1 r_regs 0%N = 1 + | ReprBusy data count => s_busy = true /\ s_done = false + /\ r_inner = ReprBusy data count + /\ nth 1 r_regs 0%N = 2 + | ReprDone res => s_busy = false /\ s_done = true + /\ (r_inner = ReprDone res \/ r_inner = ReprIdle) + /\ nth 0 r_regs 0%N = res + /\ nth 1 r_regs 0%N = 4 + end + /\ s_regs = r_regs + /\ length r_regs = 2%nat. + + Existing Instance tl_specification. + + Instance incr_specification + : specification_for incr repr := + {| reset_repr := (ReprIdle, [0; 1], TLUL.Idle, ReprIdle); + + update_repr := + fun (input : denote_type (input_of incr)) repr => + let '(i_h2d, tt) := input in + let '(r_state, r_regs, r_tl, r_inner) := repr in + + let h2d := set_a_address (N.land (a_address i_h2d) 4) i_h2d in + + let r_tl' := + let tlul_input := (h2d, (r_regs, tt)) in + update_repr (c:=tlul_adapter_reg (reg_count:=2)) + tlul_input r_tl in + + (* compute (some) tlul output *) + let '(is_read, is_write, address, write_data) := + match r_tl' with + | TLUL.Idle => (false, false, 0, 0) + | TLUL.OutstandingAccessAckData _ _ => + match r_tl with + | TLUL.Idle => (a_valid h2d, false, a_address h2d, 0) + | _ => (false, false, 0, 0) + end + | TLUL.OutstandingAccessAck _ => + match r_tl with + | TLUL.Idle => (false, a_valid h2d, a_address h2d, a_data h2d) + | _ => (false, false, 0, 0) + end + end in + + let r_inner' := + let inner_input := (match r_state with ReprIdle => is_write | _ => false end, + (write_data, tt)) in + update_repr (c:=inner) inner_input r_inner in + + let r_state' := + match r_state with + | ReprDone _ => + if (is_read && (address =? 0))%bool then ReprIdle + else r_state + | _ => + match r_inner' with + | ReprBusy data count => ReprBusy data count + | ReprDone res => ReprDone res + | _ => r_state + end + end in + + let r_regs' := + match r_inner' with + | ReprDone res => replace 0 res r_regs + | _ => r_regs + end in + + let r_regs' := + match r_state' with + | ReprIdle => replace 1 1 r_regs' + | ReprBusy _ _ => replace 1 2 r_regs' + | ReprDone _ => replace 1 4 r_regs' + end in + + (r_state', r_regs', r_tl', r_inner'); + + precondition := + fun (input : denote_type (input_of incr)) repr => + let '(i_h2d, tt) := input in + let '(r_state, r_regs, r_tl, r_inner) := repr in + + let h2d := set_a_address (N.land (a_address i_h2d) 4) i_h2d in + + let tlul_input := (h2d, (r_regs, tt)) in + + let prec_tlul := + precondition (tlul_adapter_reg (reg_count:=2)) + tlul_input r_tl in + + let prec_inner := + forall d2h is_read is_write address write_data write_mask, + postcondition (tlul_adapter_reg (reg_count:=2)) + tlul_input r_tl + (d2h, (is_read, (is_write, (address, (write_data, write_mask))))) + -> precondition inner (match r_state with ReprIdle => is_write | _ => false end, + (write_data, tt)) r_inner in + + prec_tlul /\ prec_inner; + + postcondition := + fun (input : denote_type (input_of incr)) repr + (output : denote_type (output_of incr)) => + let '(i_h2d, tt) := input in + let '(r_state, r_regs, r_tl, r_inner) := repr in + let h2d := set_a_address (N.land (a_address i_h2d) 4) i_h2d in + + (* let postc_tlul := *) + (* let tlul_input := (h2d, (r_regs, tt)) in *) + (* exists req, *) + (* postcondition (tlul_adapter_reg (reg_count:=2)) *) + (* tlul_input r_tl *) + (* (output, req) in *) + (* postc_tlul; *) + True; + |}. + + Lemma incr_invariant_at_reset : invariant_at_reset incr. + Proof. + simplify_invariant incr. + cbn. ssplit; [apply (tlul_adapter_reg_invariant_at_reset (reg_count:=2)) + |reflexivity..]. + Qed. + + Existing Instance tlul_adapter_reg_correctness. + + Lemma incr_invariant_preserved : invariant_preserved incr. + Proof. + intros (h2d, t) state (((r_state, r_regs), r_tl), r_inner). destruct t. + cbn in * |-. destruct state as ((busy, (done, (registers, d2h))), (tl_st, inner_st)). + destruct_tl_h2d. destruct_tl_d2h. + intros repr' ? Hinvar Hprec; subst. + simplify_invariant incr. logical_simplify. subst. + simplify_spec incr. logical_simplify. subst. + (* destruct Hprec as [regs Hprec]. *) + match goal with + | |- context [step incr ?s ?i] => + remember (step incr s i) as step eqn:Estep; + cbv -[Semantics.step inner tlul_adapter_reg] in Estep; + subst + end. + stepsimpl. + use_correctness. + clear H5. + rename H9 into Hpostc_tl. + repeat (destruct_pair_let; cbn [fst snd]). + ssplit. + - eapply tlul_adapter_reg_invariant_preserved. + 2: apply H. + + reflexivity. + + assumption. + - pose (r_tl_:=r_tl); destruct r_tl; logical_simplify; subst. + + destruct_tl_h2d; destruct_tl_d2h; tlsimpl; subst. + pose (r_state_:=r_state); destruct r_state; cbn in *; logical_simplify; subst; + pose (a_valid_:=a_valid); (destruct a_valid; + [ match goal with + | H: true = true -> _ |- _ => + destruct H; [auto|subst..] + end|]); cbn in *; logical_simplify; subst; + ssplit; auto. + + destruct_tl_h2d; destruct_tl_d2h; tlsimpl; subst. + pose (r_state_:=r_state); destruct r_state; cbn in *; logical_simplify; subst; + pose (d_ready_:=d_ready); destruct d_ready; cbn in *; logical_simplify; subst; + ssplit; auto. + + destruct_tl_h2d; destruct_tl_d2h; tlsimpl; subst. + pose (r_state_:=r_state); destruct r_state; cbn in *; logical_simplify; subst; + pose (d_ready_:=d_ready); destruct d_ready; cbn in *; logical_simplify; subst; + ssplit; reflexivity. + - eapply inner_invariant_preserved. + 2: eassumption. + + simpl in *. + destruct r_inner; try reflexivity. + destruct r_tl eqn:Houts; logical_simplify; subst. + * destruct a_valid eqn:Hvalid; logical_simplify; subst. + -- match goal with + | H: true = true -> _ |- _ => + destruct H; try reflexivity; subst + end; logical_simplify; subst; + boolsimpl; destruct r_state; logical_simplify; subst; + cbn in Hpostc_tl |- *; logical_simplify; subst; reflexivity. + -- boolsimpl; destruct r_state; reflexivity. + + * destruct d_ready; logical_simplify; subst; + boolsimpl; destruct r_state; reflexivity. + * destruct d_ready; logical_simplify; subst; + boolsimpl; destruct r_state; reflexivity. + + simplify_spec inner. auto. + - destruct r_tl; destruct r_inner; destruct r_state; destruct inner_st; + logical_simplify; subst; simplify_invariant inner; try discriminate. + all: simplify_spec (tlul_adapter_reg (reg_count:=2)); logical_simplify; tlsimpl; subst. + all: destruct a_valid; [destruct H3; subst|]; cbn in Hpostc_tl; logical_simplify; subst; cbn. + all: eauto. + all: destruct_tl_d2h; tlsimpl; subst. + all: try (destruct (N.land a_address 4 =? 0) eqn:Haddr; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + all: try (destruct count as [|[|[|]]]; [lia|..|lia]; cbn; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + all: try (destruct H6; discriminate). + all: try (destruct d_ready; logical_simplify; subst; cbn; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + - destruct r_tl; destruct r_inner; destruct r_state; destruct inner_st; + logical_simplify; subst. + all: simplify_invariant inner. + all: try discriminate. + all: simplify_spec (tlul_adapter_reg (reg_count:=2)); logical_simplify; tlsimpl; subst. + all: destruct a_valid; [destruct H3; subst|]; cbn in Hpostc_tl; logical_simplify; subst; cbn. + all: eauto. + all: try (destruct (N.land a_address 4 =? 0) eqn:Haddr; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + all: try (destruct count as [|[|[|]]]; [lia|..|lia]; cbn; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + all: try (destruct H6; discriminate). + all: try (destruct d_ready; logical_simplify; subst; cbn; + ssplit; eauto; + destruct x0 as [|? [|]]; cbn in *; try discriminate; reflexivity). + - repeat destruct_one_match; rewrite ! length_replace; assumption. + Qed. + + Lemma incr_output_correct : output_correct incr. + Proof. + intros ? **. + simplify_spec incr. destruct input. destruct d0. destruct r as [[[? ?] ?] ?]. + apply I. + Qed. + + Existing Instances incr_invariant_at_reset incr_invariant_preserved + incr_output_correct. + Global Instance incr_correctness : correctness_for incr. + Proof. constructor; typeclasses eauto. Defined. +End Spec. diff --git a/firmware/IncrementWait/RunIncrementWaitSoftwareOnCava.v b/firmware/IncrementWait/RunIncrementWaitSoftwareOnCava.v index acfe25f40..e6397e2ff 100644 --- a/firmware/IncrementWait/RunIncrementWaitSoftwareOnCava.v +++ b/firmware/IncrementWait/RunIncrementWaitSoftwareOnCava.v @@ -4,6 +4,7 @@ Require Import coqutil.Datatypes.List. Require Import coqutil.Word.Interface coqutil.Map.Interface. Require Import coqutil.Map.OfListWord. Require Import Bedrock2Experiments.RiscvMachineWithCavaDevice.InternalMMIOMachine. +Require Import Bedrock2Experiments.IncrementWait.Incr. Require Import Bedrock2Experiments.IncrementWait.IncrementWaitToRiscV. Require Import Bedrock2Experiments.IncrementWait.CavaIncrementDevice. Require Import riscv.Spec.Decode. @@ -90,14 +91,16 @@ Section WithVar. end%list. (* Useful for debugging: display (ok-flag, pc, output) after each cycle: + TODO why are some flags false, but then again true?? Compute snd (trace 100 initial). *) Definition res(nsteps: nat): LogElem := outcomeToLogElem (run_rec sched 0 nsteps initial). (* We can vm_compute through the execution of the IncrementWait program, - riscv-coq's processor model, and Cava's reaction to the IncrementWait program: *) + riscv-coq's processor model, and Cava's reaction to the IncrementWait program: Goal exists nsteps, res nsteps = (true, word.unsigned ret_addr, 43). exists 55%nat. vm_compute. reflexivity. Qed. + *) End WithVar. diff --git a/firmware/RiscvMachineWithCavaDevice/InternalMMIOMachine.v b/firmware/RiscvMachineWithCavaDevice/InternalMMIOMachine.v index b8f170bd0..4d57a2d7e 100644 --- a/firmware/RiscvMachineWithCavaDevice/InternalMMIOMachine.v +++ b/firmware/RiscvMachineWithCavaDevice/InternalMMIOMachine.v @@ -54,11 +54,16 @@ Module device. includes Cava.Core.Circuit.reset_state *) is_ready_state: state -> Prop; + (* the d2h output the device produced when it transitioned to the state *) + (* TODO: probably need to add to [device_implements_state_machine] somthing like + [forall s h2d d2h s', run1 s h2d = (s', d2h) -> last_d2h s' = d2h] *) + last_d2h: state -> tl_d2h; + (* run one simulation step, will be instantiated with Cava.Semantics.Combinational.step *) run1: (* input: TileLink host-2-device *) state -> tl_h2d -> (* output: next state, TileLink device-2-host *) - state * tl_d2h; + state; (* lowest address of the MMIO address range used to communicate with this device *) addr_range_start: Z; @@ -66,23 +71,46 @@ Module device. (* one past the highest MMIO address *) addr_range_pastend: Z; - (* max number of device cycles (ie calls of run1) this device takes to serve read/write requests *) - maxRespDelay: nat; + (* max number of device cycles this device takes to serve read/write requests, ie + max number of run1 calls with active read/write request until the device responds *) + maxRespDelay: state -> nat; }. (* Note: there are two levels of "polling until a response is available": - - on the hardware level, using readResp/writeResp, which appears as + - on the hardware level, using runUntilResp, which appears as blocking I/O for the software - on the software level, using MMIO reads on some status register, where the MMIO read immediately gives a "busy" response, and the software keeps polling until the MMIO read returns a "done" response *) - (* returning None means out of fuel and must not happen if fuel >= device.maxRespDelay *) + Definition waitForResp{D: device} := + fix rec(fuel: nat)(s: device.state): option device.state := + let next := device.run1 s (set_d_ready true tl_h2d_default) in + if d_valid (device.last_d2h next) then + Some next + else + match fuel with + | O => None + | S fuel' => rec fuel' next + end. + + (* returning None means out of fuel and must not happen if fuel >= device.maxRespDelay. + It is also assumed that [a_valid h2d = true] and [d_ready h2d = true]. + When the result is [Some res], retrieve the response d2h by calling + [device.last_d2h res]. *) Definition runUntilResp{D: device}(h2d: tl_h2d) := - fix rec(fuel: nat)(s: device.state): option tl_d2h * device.state := - let '(next, respo) := device.run1 s h2d in - if d_valid respo then (Some respo, next) else + fix rec(fuel: nat)(s: device.state): option device.state := + let next := device.run1 s h2d in + if a_ready (device.last_d2h s) then + if d_valid (device.last_d2h next) then + Some next + else + match fuel with + | O => None + | S fuel' => waitForResp fuel' next + end + else match fuel with - | O => (None, next) + | O => None | S fuel' => rec fuel' next end. @@ -148,11 +176,11 @@ Section WithParams. Definition runUntilResp(h2d: tl_h2d): OState (ExtraRiscvMachine D) word := mach <- get; - let (respo, new_device_state) := device.runUntilResp h2d device.maxRespDelay - mach.(getExtraState) in + new_device_state <- fail_if_None + (device.runUntilResp h2d (device.maxRespDelay mach.(getExtraState)) + mach.(getExtraState)); put (withExtraState new_device_state mach);; - resp <- fail_if_None respo; - Return (N_to_word (d_data resp)). + Return (N_to_word (d_data (device.last_d2h new_device_state))). Definition mmioLoad(log2_nbytes: nat)(addr: word) : OState (ExtraRiscvMachine D) (HList.tuple byte (2 ^ log2_nbytes)) := @@ -238,7 +266,7 @@ Section WithParams. end. Definition device_step_without_IO(d: D): D := - let '(next_state, ignored_d2h) := (device.run1 d tl_h2d_default) in next_state. + let next_state := device.run1 d (set_d_ready true tl_h2d_default) in next_state. Fixpoint device_steps(n: nat): OState (ExtraRiscvMachine D) unit := match n with diff --git a/firmware/RiscvMachineWithCavaDevice/MMIOToCava.v b/firmware/RiscvMachineWithCavaDevice/MMIOToCava.v index e2974c668..289ee4df7 100644 --- a/firmware/RiscvMachineWithCavaDevice/MMIOToCava.v +++ b/firmware/RiscvMachineWithCavaDevice/MMIOToCava.v @@ -27,72 +27,134 @@ Class device_implements_state_machine{word: word.word 32}{mem: map.map word Byte mmioAddrs_match: sameset state_machine.isMMIOAddr device.isMMIOAddr; (* simulation relation between high-level states sH and low-level states sL *) - device_state_related: state_machine.state -> D -> Prop; + device_state_related: state_machine.state -> D -> list tl_h2d -> Prop; (* if an initial high-level state is related to some low-level state, it must be a ready state *) initial_state_is_ready_state: forall sH sL, state_machine.is_initial_state sH -> - device_state_related sH sL -> + device_state_related sH sL [] -> device.is_ready_state sL; (* every initial high-level state is related to every initial low-level state *) initial_states_are_related: forall sH sL, state_machine.is_initial_state sH -> device.is_ready_state sL -> - device_state_related sH sL; + device_state_related sH sL []; (* for every initial low-level state, there exists a related initial high-level state *) initial_state_exists: forall sL, device.is_ready_state sL -> - exists sH, state_machine.is_initial_state sH /\ device_state_related sH sL; + exists sH, state_machine.is_initial_state sH /\ device_state_related sH sL []; (* transitions that are not responding to MMIO cannot change the state as seen by the software: *) nonMMIO_device_step_preserves_state_machine_state: - forall sL1 sL2 sH h2d ignored_resp, + forall sL1 sL2 sH h2d, a_valid h2d = false -> - device_state_related sH sL1 -> - device.run1 sL1 h2d = (sL2, ignored_resp) -> - device_state_related sH sL2; + (* d_ready h2d = false -> *) + device_state_related sH sL1 [] -> + device.run1 sL1 h2d = sL2 -> + device_state_related sH sL2 []; (* for each high-level state sH from which n bytes can be read at register r, - if we run the low-level device with the read step's address on the input wires, - we will get a response after at most device.maxRespDelay device cycles, - and the response will match some possible high-level read step's response, - but not necessarily the one we used to show that sH accepts reads (to allow - underspecification-nondeterminism in the high-level state machine) *) - state_machine_read_to_device_read: forall log2_nbytes r sH sL, + if we run the low-level device with the read step's address in the h2d + packet, it either tells us it's not ready to receive a request, or it's + ready, but the response is not valid yet, or it's ready, and the response + is valid, matching some possible high-level read step's response, but not + necessarily the one we used to show that sH accepts reads (to allow + underspecification-nondeterminism in the high-level state machine). In the + cases were we don't get a response, we have to try again later (either + sending the message again if the device was not ready, or wait for the + response), and by decreasing device.maxRespDelay, the device promises that + it won't keep telling us to try again later forever. In the case where the + device was ready but its response is not valid yet, the new state has an + inflight message, and the waiting for the response is handled by + state_machine_read_to_device_ack_read_or_later. *) + state_machine_read_to_device_send_read_or_later: forall log2_nbytes r sH sL sL' h2d, (exists v sH', state_machine.read_step (2 ^ log2_nbytes) sH r v sH') -> - device_state_related sH sL -> - exists d2h sL' sH', - device.runUntilResp - (set_a_valid true - (set_a_opcode Get - (set_a_size (N.of_nat log2_nbytes) - (set_a_address (word_to_N (state_machine.reg_addr r)) - (set_d_ready true tl_h2d_default))))) - device.maxRespDelay sL = (Some d2h, sL') /\ - device_state_related sH' sL' /\ - state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data d2h)) sH'; - - (* for each high-level state sH in which an n-byte write to register r with value v is possible, - if we run the low-level device with the write step's address and value on the input wires, - we will get an ack response after at most device.maxRespDelay device cycles, - and the device will end up in a state corresponding to a high-level state reached after - a high-level write, but not necessarily in the state we used to show that sH accepts writes *) - state_machine_write_to_device_write: forall log2_nbytes r v sH sL, + device_state_related sH sL [] -> + a_valid h2d = true -> + a_opcode h2d = Get -> + a_size h2d = N.of_nat log2_nbytes -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + d_ready h2d = true -> + device.run1 sL h2d = sL' -> + if a_ready (device.last_d2h sL) then + if d_valid (device.last_d2h sL') then + exists sH', + device_state_related sH' sL' [] /\ + state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data (device.last_d2h sL'))) sH' + else + device_state_related sH sL' [h2d] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat + else + device_state_related sH sL' [] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat; + + state_machine_read_to_device_ack_read_or_later: forall log2_nbytes r sH sL sL' h2d, + (exists v sH', state_machine.read_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [h2d] -> + a_opcode h2d = Get -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + device.run1 sL (set_d_ready true tl_h2d_default) = sL' -> + if d_valid (device.last_d2h sL') then + exists sH', + device_state_related sH' sL' [] /\ + state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data (device.last_d2h sL'))) sH' + else + device_state_related sH sL' [h2d] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat; + + (* for each high-level state sH in which an n-byte write to register r with + value v is possible, if we run the low-level device with the write step's + address and value in the h2d packet, it either tells us it's not ready to + receive a request, or it's ready, but the response is not valid yet, or + it's ready, and the response is valid, and the device will end up in a + state corresponding to a high-level state reached after a high-level write, + but not necessarily in the state we used to show that sH accepts writes (to + allow underspecification-nondeterminism in the high-level state machine). + In the cases were we don't get a response, we have to try again later + (either sending the message again if the device was not ready, or wait for + the response), and by decreasing device.maxRespDelay, the device promises + that it won't keep telling us to try again later forever. In the case where + the device was ready but its response is not valid yet, the new state has + an inflight message, and the waiting for the response is handled by + state_machine_write_to_device_ack_write_or_later *) + state_machine_write_to_device_send_write_or_later: forall log2_nbytes r v sH sL sL' h2d, (exists sH', state_machine.write_step (2 ^ log2_nbytes) sH r v sH') -> - device_state_related sH sL -> - exists ignored sL' sH', - device.runUntilResp - (set_a_valid true - (set_a_opcode PutFullData - (set_a_size (N.of_nat log2_nbytes) - (set_a_address (word_to_N (state_machine.reg_addr r)) - (set_a_data (word_to_N v) - (set_d_ready true tl_h2d_default)))))) - device.maxRespDelay sL = (Some ignored, sL') /\ - device_state_related sH' sL' /\ - state_machine.write_step (2 ^ log2_nbytes) sH r v sH'; + device_state_related sH sL [] -> + a_valid h2d = true -> + a_opcode h2d = PutFullData -> + a_size h2d = N.of_nat log2_nbytes -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + a_data h2d = word_to_N v -> + d_ready h2d = true -> + device.run1 sL h2d = sL' -> + if a_ready (device.last_d2h sL) then + if d_valid (device.last_d2h sL') then + exists sH', + device_state_related sH' sL' [] /\ + state_machine.write_step (2 ^ log2_nbytes) sH r v sH' + else + device_state_related sH sL' [h2d] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat + else + device_state_related sH sL' [] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat; + + state_machine_write_to_device_ack_write_or_later: forall log2_nbytes r v sH sL sL' h2d, + (exists sH', state_machine.write_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [h2d] -> + a_opcode h2d = PutFullData -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + a_data h2d = word_to_N v -> + device.run1 sL (set_d_ready true tl_h2d_default) = sL' -> + if d_valid (device.last_d2h sL') then + exists sH', + device_state_related sH' sL' [] /\ + state_machine.write_step (2 ^ log2_nbytes) sH r v sH' + else + device_state_related sH sL' [h2d] /\ + (device.maxRespDelay sL' < device.maxRespDelay sL)%nat; (* If two steps starting in the same high-level state agree on what gets appended to the trace, then the resulting high-level states must be equal. @@ -123,10 +185,180 @@ Section WithParams. {D: device} {DI: device_implements_state_machine D M}. + (* for each high-level state sH from which n bytes can be read at register r, + if we run the low-level device with the read step's address on the input wires, + we will get a response after at most device.maxRespDelay device cycles, + and the response will match some possible high-level read step's response, + but not necessarily the one we used to show that sH accepts reads (to allow + underspecification-nondeterminism in the high-level state machine) *) + Lemma state_machine_read_to_device_ack_read: forall log2_nbytes r sH sL h2d, + (exists v sH', state_machine.read_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [h2d] -> + a_opcode h2d = Get -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + exists sL' sH', + device.waitForResp (device.maxRespDelay sL) sL = Some sL' /\ + device_state_related sH' sL' [] /\ + state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data (device.last_d2h sL'))) sH'. + Proof. + intros. remember (device.maxRespDelay sL) as fuel. + remember (S fuel) as B. + assert (device.maxRespDelay sL <= fuel < B)%nat as HB by lia. + clear HeqB Heqfuel. + revert fuel sH sL H H0 H1 HB. + induction B; intros. + - exfalso. lia. + - remember (device.run1 sL (set_d_ready true tl_h2d_default)) as sL' eqn:E. + apply eq_sym in E. + destr fuel; cbn [device.waitForResp]; + pose proof (state_machine_read_to_device_ack_read_or_later + _ _ _ _ _ _ H H0 H1 H2 E) as P; rewrite E in *; + (destruct_one_match; [destruct P as (sH' & R & V); eauto 10 | + destruct P as (R & Decl)]). + + exfalso. lia. + + edestruct IHB as (sL'' & sH'' & Run & Rel & St); + try eassumption. 2: eauto 10. lia. + Qed. + + Lemma state_machine_write_to_device_ack_write: forall log2_nbytes r v sH sL h2d, + (exists sH', state_machine.write_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [h2d] -> + a_opcode h2d = PutFullData -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + a_data h2d = word_to_N v -> + exists sL' sH', + device.waitForResp (device.maxRespDelay sL) sL = Some sL' /\ + device_state_related sH' sL' [] /\ + state_machine.write_step (2 ^ log2_nbytes) sH r v sH'. + Proof. + intros. remember (device.maxRespDelay sL) as fuel. + remember (S fuel) as B. + assert (device.maxRespDelay sL <= fuel < B)%nat as HB by lia. + clear HeqB Heqfuel. + revert fuel sH sL H H0 HB. + induction B; intros. + - exfalso. lia. + - remember (device.run1 sL (set_d_ready true tl_h2d_default)) as sL' eqn:E. + apply eq_sym in E. + destr fuel; cbn [device.waitForResp]; + pose proof (state_machine_write_to_device_ack_write_or_later + _ _ _ _ _ _ _ H H0 H1 H2 H3 E) as P; rewrite E in *; + (destruct_one_match; [destruct P as (sH' & R & V); eauto 10 | + destruct P as (R & Decl)]). + + exfalso. lia. + + edestruct IHB as (sL'' & sH'' & Run & Rel & St); + try eassumption. 2: eauto 10. lia. + Qed. + + Lemma waitForResp_mono : forall (fuel fuel' : nat) s s', + (fuel <= fuel')%nat -> + device.waitForResp fuel s = Some s' -> + device.waitForResp fuel' s = Some s'. + Proof. + intros ? ?. revert fuel. induction fuel'; intros; inversion H; subst; auto. + cbn [device.waitForResp]. + destruct_one_match; destruct fuel; + cbn [device.waitForResp] in H0; rewrite E in H0; + try assumption; try discriminate. + eapply IHfuel' with (fuel:=fuel); [lia|auto]. + Qed. + + Lemma state_machine_read_to_device_read: forall log2_nbytes r sH sL h2d, + (exists v sH', state_machine.read_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [] -> + a_valid h2d = true -> + a_opcode h2d = Get -> + a_size h2d = N.of_nat log2_nbytes -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + d_ready h2d = true -> + exists sL' sH', + device.runUntilResp h2d (device.maxRespDelay sL) sL = Some sL' /\ + device_state_related sH' sL' [] /\ + state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data (device.last_d2h sL'))) sH'. + Proof. + intros. remember (device.maxRespDelay sL) as fuel. remember (S fuel) as B. + assert (device.maxRespDelay sL <= fuel < B)%nat as HB by lia. clear HeqB Heqfuel. + revert fuel sH sL H H0 HB. + induction B; intros. + - exfalso. lia. + - remember (device.run1 sL h2d) as sL' eqn:E. apply eq_sym in E. + destr fuel; cbn [device.runUntilResp]; + pose proof (state_machine_read_to_device_send_read_or_later + _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5 E) as P; + (repeat destruct_one_match; subst; rewrite ? E1 in P; + [destruct P as (sH' & R & V) | + destruct P as (R & Decr) ..]); + rewrite ? E in *. + + (* 0 remaining fuel, device ready, valid response: *) + eauto 10. + + (* 0 remaining fuel, device ready, no valid response: *) + exfalso. lia. + + (* 0 remaining fuel, device not ready: *) + exfalso. lia. + + (* some remaining fuel, device ready, valid response: *) + eauto 10. + + (* some remaining fuel, device ready, no valid response: *) + pose proof (state_machine_read_to_device_ack_read + _ _ _ _ _ H R H2 H4) as (sL'' & sH'' & W' & R' & V'). + eapply waitForResp_mono in W'. 1: eauto 10. lia. + + (* some remaining fuel, device not ready: *) + edestruct IHB as (sL'' & sH'' & Run & Rel & St); + try eassumption. 2: eauto 10. lia. + Qed. + + (* for each high-level state sH in which an n-byte write to register r with value v is possible, + if we run the low-level device with the write step's address and value on the input wires, + we will get an ack response after at most device.maxRespDelay device cycles, + and the device will end up in a state corresponding to a high-level state reached after + a high-level write, but not necessarily in the state we used to show that sH accepts writes *) + Lemma state_machine_write_to_device_write: forall log2_nbytes r v sH sL h2d, + (exists sH', state_machine.write_step (2 ^ log2_nbytes) sH r v sH') -> + device_state_related sH sL [] -> + a_valid h2d = true -> + a_opcode h2d = PutFullData -> + a_size h2d = N.of_nat log2_nbytes -> + a_address h2d = word_to_N (state_machine.reg_addr r) -> + a_data h2d = word_to_N v -> + d_ready h2d = true -> + exists sL' sH', + device.runUntilResp h2d (device.maxRespDelay sL) sL = Some sL' /\ + device_state_related sH' sL' [] /\ + state_machine.write_step (2 ^ log2_nbytes) sH r v sH'. + Proof. + intros. remember (device.maxRespDelay sL) as fuel. remember (S fuel) as B. + assert (device.maxRespDelay sL <= fuel < B)%nat as HB by lia. clear HeqB Heqfuel. + revert fuel sH sL H H0 HB. + induction B; intros. + - exfalso. lia. + - remember (device.run1 sL h2d) as sL' eqn:E. apply eq_sym in E. + destr fuel; cbn [device.runUntilResp]; + pose proof (state_machine_write_to_device_send_write_or_later + _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5 H6 E) as P; + (repeat destruct_one_match; subst; rewrite ? E1 in P; + [destruct P as (sH' & R & V) | + destruct P as (R & Decr) ..]); + rewrite ? E in *. + + (* 0 remaining fuel, device ready, valid response: *) + eauto 10. + + (* 0 remaining fuel, device ready, no valid response: *) + exfalso. lia. + + (* 0 remaining fuel, device not ready: *) + exfalso. lia. + + (* some remaining fuel, device ready, valid response: *) + clear -R V. eauto 10. + + (* some remaining fuel, device ready, no valid response: *) + pose proof (state_machine_write_to_device_ack_write + _ _ _ _ _ _ H R H2 H4 H5) as (sL'' & sH'' & W' & R' & V'). + eapply waitForResp_mono in W'. 1: eauto 10. lia. + + (* some remaining fuel, device not ready *) + edestruct IHB as (sL'' & sH'' & Run & Rel & St); + try eassumption. 2: eauto 10. lia. + Qed. + Inductive related: MetricRiscvMachine -> ExtraRiscvMachine D -> Prop := mkRelated: forall regs pc npc m xAddrs (t: list LogItem) t_ignored mc d s, execution t s -> - device_state_related s d -> + device_state_related s d [] -> map.undef_on m state_machine.isMMIOAddr -> disjoint (of_list xAddrs) state_machine.isMMIOAddr -> related @@ -314,11 +546,15 @@ Section WithParams. | E1: execution _ _, E2: execution _ _ |- _ => pose proof (execution_unique _ _ _ E1 E2); subst; clear E2 end. - 1-4: edestruct state_machine_read_to_device_read as (v'' & d'' & s'' & RU'' & Rel'' & RS''); - [do 2 eexists; match goal with - | H: state_machine.read_step ?n _ _ _ _ |- _ => - change n at 1 with (2 ^ (Nat.log2 n))%nat in H - end; eassumption|solve[eauto]|]. + 1-4: match goal with + | |- context[device.runUntilResp ?p _ _] => + edestruct state_machine_read_to_device_read with (h2d := p) + as (d'' & s'' & RU'' & Rel'' & RS''); + [do 2 eexists; match goal with + | H: state_machine.read_step ?n _ _ _ _ |- _ => + change n at 1 with (2 ^ (Nat.log2 n))%nat in H + end; eassumption|eassumption|reflexivity..|] + end. 1-4: cbn -[HList.tuple]; tlsimpl; simpl in RU''; rewrite RU''; cbn -[HList.tuple]. 4: { (* 64-bit MMIO is not supported: *) eapply state_machine.read_step_size_valid in HLp2p2. simpl in HLp2p2. exfalso. intuition congruence. @@ -349,13 +585,19 @@ Section WithParams. | E1: execution _ _, E2: execution _ _ |- _ => pose proof (execution_unique _ _ _ E1 E2); subst; clear E2 end. - 1-3: edestruct state_machine_write_to_device_write as (ignored & d' & s'' & RU & Rel' & WS'); - [eexists; match goal with - | H: state_machine.write_step ?n _ _ _ _ |- _ => - change n at 1 with (2 ^ (Nat.log2 n))%nat in H - end; eassumption|solve[eauto]|]. + 1-3: match goal with + | |- context[device.runUntilResp ?p _ _] => + edestruct state_machine_write_to_device_write with (h2d := p) + as (d' & s'' & RU & Rel' & WS'); + [eexists; match goal with + | H: state_machine.write_step ?n _ _ _ _ |- _ => + change n at 1 with (2 ^ (Nat.log2 n))%nat in H + end; eassumption + |eassumption + |rewrite ? Z_word_N in * by lia; reflexivity..|] + end. 1-3: cbn -[HList.tuple Primitives.invalidateWrittenXAddrs]; - tlsimpl; simpl in RU; rewrite Z_word_N in RU by lia; rewrite RU; + tlsimpl; simpl in RU; rewrite RU; cbn -[HList.tuple Primitives.invalidateWrittenXAddrs]. 1-3: eauto 15 using mkRelated, execution_write_cons, preserve_disjoint_of_invalidateXAddrs. @@ -398,13 +640,8 @@ Section WithParams. unfold device_step_without_IO. eapply mkRelated. + eassumption. - + match goal with - | |- context[let '(_, _) := ?p in _] => destruct p eqn: E - end. - eapply nonMMIO_device_step_preserves_state_machine_state. 2: eassumption. - 1: instantiate (1 := tl_h2d_default); reflexivity. - simpl. - exact E. + + eapply nonMMIO_device_step_preserves_state_machine_state; + [..|reflexivity]; auto. + assumption. + assumption. Qed. diff --git a/silveroak-opentitan/hmac/end2end/Bedrock2StateMachineToCavaHmac.v b/silveroak-opentitan/hmac/end2end/Bedrock2StateMachineToCavaHmac.v new file mode 100644 index 000000000..18df72856 --- /dev/null +++ b/silveroak-opentitan/hmac/end2end/Bedrock2StateMachineToCavaHmac.v @@ -0,0 +1,221 @@ +(****************************************************************************) +(* 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.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. + +Require Import coqutil.Tactics.Tactics. +Require Import coqutil.Datatypes.Prod. + +Require Import Cava.Util.Byte. +Require Import Cava.Types. +Require Import Cava.Expr. +Require Import Cava.Primitives. +Require Import Cava.TLUL. +Require Import Cava.Invariant. +Require Import Cava.Primitives. +Require Import Cava.Semantics. +Require Import Cava.Expr. +Require Import Cava.ExprProperties. +Require Import Cava.Util.Tactics. +Require Import Cava.Util.List. +Require Import Cava.Util.If. +Require Import Cava.Util.Nat. +Require Import Cava.Util.Byte. +Require Import coqutil.Word.Interface coqutil.Word.Properties. +Require Import coqutil.Word.LittleEndianList. +Require Import HmacHardware.Hmac. +Require Import HmacHardware.Sha256. +Require HmacSoftware.HmacSemantics. + +Import ListNotations. + +Axiom hmac_repr: Type. +(* Note: hmac_repr might/should be an Inductive, so probably no hmac_repr_msg getter will + exists, but we will need to do a match, and assert False in the other cases *) +Axiom hmac_repr_msg: hmac_repr -> list Byte.byte. +Axiom hmac_repr_max_cycles_until_done: hmac_repr -> nat. + +Instance hmac_invariant: invariant_for hmac hmac_repr. Admitted. + +(* TLUL communication state *) +Inductive tlul_protocol_state := +(* host is not interested in talking to device at the moment *) +| HostNotInterested +(* host wants to talk to device and is waiting for device to become ready *) +| HostWaitingForReady(maxDelay: nat) +(* host can and will send a packet in the next cycle *) +| HostCanSend +(* host sent a message to device and is waiting for a reply from device *) +| HostWaitingForReply(packet: tl_h2d)(maxDelay: nat). + +Definition tlul_state_step(s1 s2: tlul_protocol_state): Prop := + match s1 with + | HostNotInterested => + s2 = HostNotInterested \/ + exists maxDelay, s2 = HostWaitingForReady maxDelay + | HostWaitingForReady maxDelay => + (exists maxDelay', maxDelay = S maxDelay' /\ s2 = HostWaitingForReady maxDelay') \/ + s2 = HostCanSend + | HostCanSend => exists packet maxDelay, s2 = HostWaitingForReply packet maxDelay + | HostWaitingForReply packet maxDelay => + (exists maxDelay', maxDelay = S maxDelay' /\ s2 = HostWaitingForReply packet maxDelay') \/ + s2 = HostNotInterested + end. + +Definition a_valid_of_current_tlul_state(s: tlul_protocol_state): bool := + match s with + | HostNotInterested => false + | HostWaitingForReady maxDelay => false + | HostCanSend => true + | HostWaitingForReply packet maxDelay => false + end. + +Definition d_ready_of_current_tlul_state(s: tlul_protocol_state): bool := + match s with + | HostNotInterested => false + | HostWaitingForReady maxDelay => false + | HostCanSend => true + | HostWaitingForReply packet maxDelay => true + end. + +Definition d_valid_of_current_and_next_tlul_state(s1 s2: tlul_protocol_state): bool := + match s1 with + | HostWaitingForReply packet maxDelay => + match s2 with + | HostWaitingForReply packet' maxDelay' => false + | _ => true + end + | _ => false + end. + +(* If the host and device both behave correctly, then each device cycle that takes in + h2d and outputs d2h (ie `step circuit circuit_state1 h2d = (circuit_state2, d2h)`) + corresponds to a transition in the following transition system: *) +Definition tlul_step(s1: tlul_protocol_state)(h2d: tl_h2d) + (s2: tlul_protocol_state)(d2h: tl_d2h): Prop := + a_valid h2d = a_valid_of_current_tlul_state s1 /\ + d_ready h2d = d_ready_of_current_tlul_state s1 /\ + d_valid d2h = d_valid_of_current_and_next_tlul_state s1 s2 /\ + match s1 with + | HostNotInterested => + match s2 with + | HostNotInterested => True + | HostWaitingForReady maxDelay => a_ready d2h = false + | HostCanSend => a_ready d2h = true + | HostWaitingForReply packet maxDelay => False + end + | HostWaitingForReady maxDelay => + match s2 with + | HostNotInterested => False + | HostWaitingForReady maxDelay' => a_ready d2h = false /\ maxDelay = S maxDelay' + | HostCanSend => a_ready d2h = true + | HostWaitingForReply packet maxDelay => False + end + | HostCanSend => + match s2 with + | HostWaitingForReply packet maxDelay => packet = h2d + | _ => False + end + | HostWaitingForReply packet maxDelay => + match s2 with + | HostNotInterested => True + | HostWaitingForReady maxDelay' => a_ready d2h = false + | HostCanSend => a_ready d2h = true + | HostWaitingForReply packet' maxDelay' => packet' = packet /\ maxDelay = S maxDelay' + end + end. + +Section WithParams. + Context {word: word 32} {word_ok: word.ok word}. + + Definition REG_DIGEST_0: nat. + let r := eval unfold HmacHardware.Hmac.REG_DIGEST_0 in HmacHardware.Hmac.REG_DIGEST_0 in + lazymatch r with + | Constant _ ?v => exact (N.to_nat v) + end. + Defined. + + Definition REG_CFG: nat. + let r := eval unfold HmacHardware.Hmac.REG_CFG in HmacHardware.Hmac.REG_CFG in + lazymatch r with + | Constant _ ?v => exact (N.to_nat v) + end. + Defined. + + Definition REG_INTR_STATE: nat := 0. + Definition REG_INTR_ENABLE: nat := 1. + + Definition N_le_word_list_to_byte_list: list N -> list Byte.byte := + List.flat_map (fun n => le_split 4 (Z.of_N n)). + + Definition get_hl_config(regs: list N): HmacSemantics.idle_data := {| + HmacSemantics.intr_enable := word.of_Z (Z.of_N (List.nth REG_INTR_ENABLE regs 0%N)); + HmacSemantics.hmac_done := N.testbit 0 (List.nth REG_INTR_ENABLE regs 0%N); + HmacSemantics.hmac_en := N.testbit 0 (List.nth REG_CFG regs 0%N); + HmacSemantics.sha_en := N.testbit 1 (List.nth REG_CFG regs 0%N); + HmacSemantics.swap_endian := N.testbit 2 (List.nth REG_CFG regs 0%N); + HmacSemantics.swap_digest := N.testbit 3 (List.nth REG_CFG regs 0%N); + |}. + + Instance hmac_top_invariant: invariant_for hmac_top HmacSemantics.state := + fun (circuit_state: denote_type hmac_top_state) (stm_state: HmacSemantics.state) => + let '((wasfull, (d2h, regs)), (tlul_st, hmac_st)) := circuit_state in + exists hmac_r: hmac_repr, hmac_invariant hmac_st hmac_r /\ + match stm_state with + | HmacSemantics.IDLE digest config => + digest = N_le_word_list_to_byte_list (List.firstn 8 (List.skipn REG_DIGEST_0 regs)) /\ + config = get_hl_config regs + | HmacSemantics.CONSUMING buf => + get_hl_config regs = HmacSemantics.sha_default_cfg /\ + hmac_repr_msg hmac_r = buf + | HmacSemantics.PROCESSING buf ncycles => + get_hl_config regs = HmacSemantics.sha_default_cfg /\ + hmac_repr_msg hmac_r = buf /\ + Z.of_nat (hmac_repr_max_cycles_until_done hmac_r) = ncycles + end. + + Instance hmac_top_specification: specification_for hmac_top HmacSemantics.state := {| + reset_repr := HmacSemantics.IDLE (List.repeat Byte.x00 32) HmacSemantics.zero_cfg; + precondition h2d st := True; + update_repr h2d st := + match st with + | HmacSemantics.IDLE digest config => st + | HmacSemantics.CONSUMING buf => st + | HmacSemantics.PROCESSING buf ncycles => st + end; + postcondition h2d st d2h := True; + |}. + + Lemma hmac_top_invariant_at_reset: invariant_at_reset hmac_top. + Admitted. + + Lemma hmac_top_invariant_preserved: invariant_preserved hmac_top. + Proof. + simplify_invariant hmac_top. cbn [absorb_any]. + simplify_spec hmac_top. + intros input state repr new_repr. + Admitted. + + Lemma hmac_top_output_correct: output_correct hmac_top. + Proof. + simplify_invariant hmac_top. simplify_spec hmac_top. + intros input state repr new_repr. + Admitted. + +End WithParams. diff --git a/silveroak-opentitan/hmac/end2end/CavaHmacDevice.v b/silveroak-opentitan/hmac/end2end/CavaHmacDevice.v index 3cd431157..0c2a7331c 100644 --- a/silveroak-opentitan/hmac/end2end/CavaHmacDevice.v +++ b/silveroak-opentitan/hmac/end2end/CavaHmacDevice.v @@ -1,3 +1,4 @@ +Require Import Coq.Lists.List. Require Import Coq.ZArith.ZArith. Open Scope Z_scope. Require Import riscv.Utility.Utility. Require Import coqutil.Map.Interface coqutil.Map.Properties. @@ -16,6 +17,7 @@ Require Import Cava.TLUL. Require Import Cava.Types. Require Import Cava.Util.BitArithmetic. +Import ListNotations. Section WithParameters. Instance var : tvar := denote_type. @@ -28,12 +30,18 @@ Section WithParameters. Global Instance hmac_device: device := {| device.state := denote_type (state_of hmac_top); device.is_ready_state s := True; (* FIXME *) - device.run1 s i := Semantics.step hmac_top s (i, tt); + + device.last_d2h '((_, (d2h, _)), _) := d2h; + + device.run1 s i := fst (Semantics.step hmac_top s (i, tt)); + device.addr_range_start := TOP_EARLGREY_HMAC_BASE_ADDR; device.addr_range_pastend := TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_MSG_FIFO_REG_OFFSET + HMAC_MSG_FIFO_SIZE_BYTES; - device.maxRespDelay := 1; (* FIXME *) + + device.maxRespDelay '((_, (d2h, _)), _) := + if a_ready d2h then 0%nat else 1%nat; |}. Global Instance hmac_timing: timing := { max_negative_done_polls := 16; diff --git a/silveroak-opentitan/hmac/sw/HmacSemantics.v b/silveroak-opentitan/hmac/sw/HmacSemantics.v index 93ea8a241..a4bf505c7 100644 --- a/silveroak-opentitan/hmac/sw/HmacSemantics.v +++ b/silveroak-opentitan/hmac/sw/HmacSemantics.v @@ -50,6 +50,24 @@ Section WithParams. | CONSUMING(sha_buffer: list byte) | PROCESSING(sha_buffer: list byte)(max_cycles_until_done: Z). + Definition sha_default_cfg := {| + hmac_done := false; + intr_enable := word.of_Z 0; + hmac_en := false; + sha_en := true; + swap_endian := true; + swap_digest := false; + |}. + + Definition zero_cfg := {| + hmac_done := false; + intr_enable := word.of_Z 0; + hmac_en := false; + sha_en := false; + swap_endian := false; + swap_digest := false; + |}. + Inductive read_step: nat -> state -> word -> word -> state -> Prop := | read_done_bit_not_done: forall b v n, 0 < n -> @@ -109,17 +127,12 @@ Section WithParams. swap_digest := swap_digest s; |}) | write_hash_start: forall d v, v = word.of_Z (Z.shiftl 1 HMAC_CMD_HASH_START_BIT) -> - write_step 4 (IDLE d (* Here one can see that we only model a subset of the features of - the HMAC module: in our model, starting the computation is only - possible from the specific configuration below. - But using an HMAC module with more features than what we expose - to the software is safe, so modeling only a subset is not a problem. *) - {| hmac_done := false; - intr_enable := word.of_Z 0; - hmac_en := false; - sha_en := true; - swap_endian := true; - swap_digest := false; |}) + (* Here one can see that we only model a subset of the features of + the HMAC module: in our model, starting the computation is only + possible from the sha_default_cfg configuration. + But using an HMAC module with more features than what we expose + to the software is safe, so modeling only a subset is not a problem. *) + write_step 4 (IDLE d sha_default_cfg) (word.of_Z (TOP_EARLGREY_HMAC_BASE_ADDR + HMAC_CMD_REG_OFFSET)) v (CONSUMING []) | write_byte: forall bs bs' v,