Skip to content
This repository has been archived by the owner on Dec 13, 2022. It is now read-only.

express device_implements_state_machine using only run1, without runUntilResp (on top of #959) #960

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

express device_implements_state_machine using only run1, without runUntilResp (on top of #959) #960

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
554d6d9
run bedrock2-generated RISC-V code for the SHA256 driver in
samuelgruetter Nov 2, 2021
7622478
disable pinmux/OpenTitan integration because it's in Cava1 and
samuelgruetter Nov 3, 2021
5b28c68
express device_implements_state_machine using only run1,
samuelgruetter Nov 3, 2021
f1e17a1
Merge branch 'main' into device_spec_run1only
samuelgruetter Nov 8, 2021
a5fec37
sketch hmac_top_invariant and some tlul state machine
samuelgruetter Nov 10, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 68 additions & 9 deletions firmware/IncrementWait/CavaIncrementDevice.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ 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.fwd.

Require Import bedrock2.ZnWords.

Expand Down Expand Up @@ -186,7 +187,11 @@ Section WithParameters.
device.run1 s i := 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 '((istate, (val, tl_d2h)), tlul_state) h2d :=
(* if the value register was requested, and we're in state Busy1, it will take one
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if this is relevant, but the SW semantics allows reading the value register only when in the DONE state.

more cycle to respond, else we will respond immediately *)
if ((a_address h2d mod 8 =? 0(*register address=VALUE*))%N && (istate =? 1 (*Busy1*))%N)%bool
then 1%nat else 0%nat;
|}.

(* conservative upper bound matching the instance given in IncrementWaitToRiscv *)
Expand Down Expand Up @@ -258,6 +263,42 @@ Section WithParameters.
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.

(* TODO move to coqutil *)
Ltac contradictory H :=
lazymatch type of H with
| ?x <> ?x => exfalso; apply (H eq_refl)
| False => case H
end.
Require Import coqutil.Tactics.autoforward.
Ltac fwd_step ::=
match goal with
| H: ?T |- _ => is_destructible_and T; destr_and H
| H: exists y, _ |- _ => let yf := fresh y in destruct H as [yf H]
| H: ?x = ?x |- _ => clear H
| H: True |- _ => clear H
| H: ?LHS = ?RHS |- _ =>
let h1 := head_of_app LHS in is_constructor h1;
let h2 := head_of_app RHS in is_constructor h2;
(* if not eq, H is a contradiction, but we don't want to change the number
of open goals in this tactic *)
constr_eq h1 h2;
(* we don't use `inversion H` or `injection H` because they unfold definitions *)
inv_rec LHS RHS;
clear H
| E: ?x = ?RHS |- context[match ?x with _ => _ end] =>
let h := head_of_app RHS in is_constructor h; rewrite E in *
| H: context[match ?x with _ => _ end], E: ?x = ?RHS |- _ =>
let h := head_of_app RHS in is_constructor h; rewrite E in *
| H: context[match ?x with _ => _ end] |- _ =>
(* note: recursive invocation of fwd_step for contradictory cases *)
destr x; try solve [repeat fwd_step; contradictory H]; []
| H: _ |- _ => autoforward with typeclass_instances in H
| |- _ => progress subst
| |- _ => progress fwd_rewrites
end.

Axiom TODO: False.

(* Set Printing All. *)
Global Instance cava_counter_satisfies_state_machine:
device_implements_state_machine counter_device increment_wait_state_machine.
Expand All @@ -283,18 +324,32 @@ Section WithParameters.
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 *.
- (* state_machine_read_to_device_read_or_later: *)
case TODO.
(*
cbn [counter_device device.state device.is_ready_state device.run1 device.addr_range_start
device.addr_range_pastend device.maxRespDelay] in *.
cbn [increment_wait_state_machine
state_machine.state
state_machine.register
state_machine.is_initial_state
state_machine.read_step
state_machine.write_step
state_machine.reg_addr
state_machine.isMMIOAddr] 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; [|].
tlsimpl.
destruct r; simp.
+ (* r=VALUE *)
destruct_tl_h2d.
cbn in *. subst.

destruct_consistent_states. subst.
repeat (rewrite Z_word_N by lia; cbn).
destruct outstanding; [|];
destruct outstanding; cbn in H1|-*; fwd.


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).
Expand Down Expand Up @@ -360,7 +415,10 @@ Section WithParameters.
ssplit; try reflexivity;
try (eapply DONE_related; unfold consistent_states; ssplit; reflexivity);
try (simpl; ZnWords).
- (* state_machine_write_to_device_write: *)
*)
- (* state_machine_write_to_device_write_or_later: *)
case TODO.
(*
destruct H as (sH' & ? & ?). subst.
unfold write_step in H1.
destruct r. 2: contradiction.
Expand All @@ -373,6 +431,7 @@ Section WithParameters.
eexists _, _, _; ssplit; try reflexivity; try assumption; apply BUSY1_related;
try lia;
try (unfold consistent_states; ssplit; reflexivity).
*)
- (* read_step_unique: *)
simpl in *. unfold read_step in *. simp.
destruct v; destruct r; try contradiction; simp; try reflexivity.
Expand Down
4 changes: 3 additions & 1 deletion firmware/IncrementWait/RunIncrementWaitSoftwareOnCava.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,14 +90,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.
12 changes: 7 additions & 5 deletions firmware/RiscvMachineWithCavaDevice/InternalMMIOMachine.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,11 +66,12 @@ 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 -> tl_h2d -> 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
Expand Down Expand Up @@ -148,8 +149,9 @@ 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
let (respo, new_device_state) :=
device.runUntilResp h2d (device.maxRespDelay mach.(getExtraState) h2d)
mach.(getExtraState) in
put (withExtraState new_device_state mach);;
resp <- fail_if_None respo;
Return (N_to_word (d_data resp)).
Expand Down
175 changes: 136 additions & 39 deletions firmware/RiscvMachineWithCavaDevice/MMIOToCava.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,43 +56,52 @@ Class device_implements_state_machine{word: word.word 32}{mem: map.map word Byte

(* 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,
it either tells us to try again later (but by decreasing device.maxRespDelay,
it promises that it won't keep telling us to try again later forever), or
we will get a response 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) *)
state_machine_read_to_device_read: forall log2_nbytes r sH sL,
state_machine_read_to_device_read_or_later: forall log2_nbytes r sH sL sL' h2d d2h,
(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';
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', d2h) ->
if d_valid d2h then
exists sH',
device_state_related sH' sL' /\
state_machine.read_step (2 ^ log2_nbytes) sH r (N_to_word (d_data d2h)) sH'
else
device_state_related sH sL' /\
(device.maxRespDelay sL' h2d < device.maxRespDelay sL h2d)%nat;
Comment on lines +67 to +79
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is incorrect in general (the original code also has the same issue).
TLDR: you never check a_ready d2h=1, and you might be sending multiple valid Get requests, instead of just one.

The process of reading from a register is broken down to two sub-tasks:

  1. Host sends a 'Get' command on channel A (h2d packet); and
  2. the device reply with an ack, that includes the value of the register, on channel D (d2h packet).

When you send an h2d packet on channel A you have to check that a_ready from the previous d2h packet is set to 1, only then you can send your h2d packet with a_valid=1, and you must send it only once (otherwise the other side might consider it as multiple messages).
After you sent the h2d packet on channel A you need to wait (i.e. send h2d packets with a_valid=0 and d_ready=1) until you get back a d2h packet with d_valid=1.


(* 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,
it either tells us to try again later (but by decreasing device.maxRespDelay,
it promises that it won't keep telling us to try again later forever), or
we will get an ack response 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_or_later: forall log2_nbytes r v sH sL sL' h2d d2h,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similar issue as with state_machine_read_to_device_read_or_later.

(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';
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', d2h) ->
if d_valid d2h 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' /\
(device.maxRespDelay sL' h2d < device.maxRespDelay sL h2d)%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.
Expand Down Expand Up @@ -123,6 +132,84 @@ 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_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 d2h sL' sH',
device.runUntilResp h2d (device.maxRespDelay sL h2d) 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'.
Proof.
intros. remember (device.maxRespDelay sL h2d) as fuel. remember (S fuel) as B.
assert (device.maxRespDelay sL h2d <= fuel < B)%nat as HB by lia. clear HeqB Heqfuel.
revert fuel sH sL H H0 HB.
induction B; intros.
- exfalso. lia.
- destr fuel; cbn [device.runUntilResp]; destruct_one_match;
pose proof (state_machine_read_to_device_read_or_later
_ _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5 E) as P;
(destruct_one_match; [destruct P as (sH' & R & V) | destruct P as (R & Decr)]).
+ (* 0 remaining fuel, valid response: *)
clear -R V. eauto 10.
+ (* 0 remaining fuel, no valid response: *)
exfalso. lia.
+ (* some remaining fuel, valid response: *)
clear -R V. eauto 10.
+ (* some remaining fuel, no valid response *)
edestruct IHB as (d2h & sL'' & sH'' & Run & Rel & St).
1: eassumption. 1: exact R. 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 ignored sL' sH',
device.runUntilResp h2d (device.maxRespDelay sL h2d) sL = (Some ignored, sL') /\
device_state_related sH' sL' /\
state_machine.write_step (2 ^ log2_nbytes) sH r v sH'.
Proof.
intros. remember (device.maxRespDelay sL h2d) as fuel. remember (S fuel) as B.
assert (device.maxRespDelay sL h2d <= fuel < B)%nat as HB by lia. clear HeqB Heqfuel.
revert fuel sH sL H H0 HB.
induction B; intros.
- exfalso. lia.
- destr fuel; cbn [device.runUntilResp]; destruct_one_match;
pose proof (state_machine_write_to_device_write_or_later
_ _ _ _ _ _ _ _ H H0 H1 H2 H3 H4 H5 H6 E) as P;
(destruct_one_match; [destruct P as (sH' & R & V) | destruct P as (R & Decr)]).
+ (* 0 remaining fuel, valid response: *)
clear -R V. eauto 10.
+ (* 0 remaining fuel, no valid response: *)
exfalso. lia.
+ (* some remaining fuel, valid response: *)
clear -R V. eauto 10.
+ (* some remaining fuel, no valid response *)
edestruct IHB as (d2h & sL'' & sH'' & Run & Rel & St).
1: eassumption. 1: exact R. 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 ->
Expand Down Expand Up @@ -314,11 +401,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 (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|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.
Expand Down Expand Up @@ -349,13 +440,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 (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
|eassumption
|rewrite ? Z_word_N in * by lia; try 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.

Expand Down
Loading