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

Commit

Permalink
Use ZnWords to prove the axioms, and clean the proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@fshaked
fshaked committed Aug 18, 2021
1 parent 654a072 commit c4b8e89
Showing 1 changed file with 39 additions and 59 deletions.
98 changes: 39 additions & 59 deletions firmware/IncrementWait/CavaIncrementDevice.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -147,13 +147,17 @@ Section WithParameters.
| DONE_related: forall val,
counter_related (DONE val) (mk_counter_state false 0 true (word_to_N val)).

Axiom TODO: Coq.Init.Logic.False.
(* This should be in bedrock2.ZnWords. It is use by ZnWords, which is used in
the two following Lemmas. *)
Ltac better_lia ::= Zify.zify; Z.to_euclidean_division_equations; Lia.lia.

Axiom word_to_N_inj: forall x y, word_to_N x = word_to_N y -> x = y.
Lemma incrN_word_to_bv: forall x,
((N.add (word_to_N x) 1) mod 4294967296)%N = word_to_N (word.add (word.of_Z 1) x).
Proof. intros. unfold word_to_N. ZnWords. Qed.

Axiom incrN_word_to_bv: forall v, ((N.add (word_to_N v) 1) mod 4294967296)%N = word_to_N (word.add (word.of_Z 1) v).

Axiom Z_word_N: forall (x : Z), word_to_N (word.of_Z x) = Z.to_N x.
Lemma Z_word_N: forall x,
(0 <= x < 2 ^ 32) -> word_to_N (word.of_Z x) = Z.to_N x.
Proof. intros. unfold word_to_N. ZnWords. Qed.

Set Printing Depth 100000.

Expand Down Expand Up @@ -200,7 +204,7 @@ Section WithParameters.
unfold read_step in *.
destruct r.
+ (* r=VALUE *)
simp. cbn. rewrite Z_word_N. cbn.
simp. cbn. rewrite Z_word_N; try Lia.lia; []. cbn.
unfold word_to_N.
(* rewrite word.unsigned_of_Z_nowrap by (cbv; intuition discriminate). *)
simpl. do 3 eexists. ssplit; try reflexivity.
Expand All @@ -210,7 +214,7 @@ Section WithParameters.
destruct sH.
* (* sH=IDLE *)
destruct Hp1. subst. inversion H0. subst.
cbn. repeat (rewrite Z_word_N; cbn).
cbn. repeat (rewrite Z_word_N; try Lia.lia; []; cbn).
unfold status_value, STATUS_IDLE, word_to_N.
(* rewrite word.unsigned_of_Z_nowrap by (cbv; intuition discriminate). *)
do 3 eexists. ssplit; try reflexivity. 2: eapply IDLE_related.
Expand All @@ -219,56 +223,42 @@ Section WithParameters.
change (1%N) at 2 with (bool_to_dbit true).
destruct idle; reflexivity.
* (* sH=BUSY *)
simp.
destruct Hp1 as [H | H].
simp. destruct Hp1 as [H | H].
-- (* transition to DONE *)
destruct H; subst.
simpl (state_machine.reg_addr _).
unfold STATUS_ADDR, INCR_BASE_ADDR, word_to_N, status_value, STATUS_DONE.
rewrite !word.unsigned_of_Z. unfold word.wrap. simpl.
inversion H0; subst.
++ (* BUSY1_related *)
(* the transition that was used to show that sH is not stuck was a transition *)
(* from BUSY to DONE returning a done flag, but since the device is still *)
(* in BUSY state, it will still return the busy flag in this transition, *)
(* so the transition we use to simulate what happened in the device is a *)
(* BUSY-to-DONE transition returning a busy flag instead of a done flag *)
destruct max_cycles_until_done. 1: inversion H3. clear H3.
exists (word.of_Z 2). (* <- bit #1 (busy) is set, all others are 0 *)
do 2 eexists.
rewrite !word.unsigned_of_Z. unfold word.wrap. cbn.
ssplit; try reflexivity.
** simpl.
change (0%N) with (bool_to_dbit false).
** change (0%N) with (bool_to_dbit false).
eapply BUSY2_related.
shelve.
** right. eexists; ssplit; try reflexivity.
eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
Unshelve.
inversion H0; subst. Lia.lia.
instantiate ( 1 := max_cycles_until_done ).
inversion H0; subst.
Lia.lia.
** right. eexists; ssplit; try reflexivity; []. ZnWords.
++ (* BUSY2_related *)
(* the transition that was used to show that sH is not stuck was a transition *)
(* from BUSY to DONE returning a done flag, but since the device is still *)
(* in BUSY state, it will still return the busy flag in this transition, *)
(* so the transition we use to simulate what happened in the device is a *)
(* BUSY-to-DONE transition returning a busy flag instead of a done flag *)
cbn.
(* the transition that was used to show that sH is not stuck was *)
(* a transition from BUSY to DONE returning a done flag, but *)
(* since the device is still in BUSY state, it will still return *)
(* the busy flag in this transition, so the transition we use to *)
(* simulate what happened in the device is a BUSY-to-DONE *)
(* transition returning a busy flag instead of a done flag. *)
exists (word.of_Z 4). (* <- bit #2 (done) is set, all others are 0 *)
(* destruct max_cycles_until_done. 1: inversion H3. clear H3. *)
do 2 eexists.
rewrite !word.unsigned_of_Z. unfold word.wrap. cbn.
ssplit; try reflexivity.
** simpl.
change (0%N) at 1 with (bool_to_dbit false).
** change (0%N) at 1 with (bool_to_dbit false).
change (1%N) at 1 with (bool_to_dbit true).
rewrite incrN_word_to_bv.
eapply DONE_related.
** left. eexists; ssplit; try reflexivity.
eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
** left. eexists; ssplit; try reflexivity. ZnWords.
++ (* BUSY_done_related *)
exists (word.of_Z 4). (* <- bit #2 (done) is set, all others are 0 *)
do 2 eexists.
Expand All @@ -279,9 +269,7 @@ Section WithParameters.
change (1%N) at 1 with (bool_to_dbit true).
(* rewrite incrN_word_to_bv. *)
eapply DONE_related.
** left. split. 2: reflexivity. eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
** left. split. 2: reflexivity. ZnWords.
-- (* stay BUSY *)
destruct H as (n & ? & ? & ?); subst.
simpl (state_machine.reg_addr _).
Expand All @@ -294,12 +282,9 @@ Section WithParameters.
rewrite !word.unsigned_of_Z. unfold word.wrap. cbn.
ssplit; try reflexivity.
** change (0%N) with (bool_to_dbit false).
eapply BUSY2_related.
shelve.
** right. eexists; ssplit; try reflexivity. eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
Unshelve. Lia.lia.
eapply BUSY2_related. instantiate (1 := n).
Lia.lia.
** right. eexists; ssplit; try reflexivity. ZnWords.
++ (* BUSY2_related *)
exists (word.of_Z 4). (* <- bit #2 (done) is set, all others are 0 *)
do 2 eexists.
Expand All @@ -309,24 +294,21 @@ Section WithParameters.
change (1%N) at 1 with (bool_to_dbit true).
rewrite incrN_word_to_bv.
eapply DONE_related.
** left. eexists; ssplit; try reflexivity. eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
** left. eexists; ssplit; try reflexivity. 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. *)
(* 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. *)
exists (word.of_Z 4). (* <- bit #2 (done) is set, all others are 0 *)
do 2 eexists.
rewrite !word.unsigned_of_Z. unfold word.wrap. cbn.
ssplit; try reflexivity.
** simpl. eapply DONE_related.
** left. split. 2: reflexivity. eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
** left. split. 2: reflexivity. ZnWords.
* (* sH=DONE *)
destruct Hp1. subst. inversion H0. subst.
simpl (state_machine.reg_addr _).
Expand All @@ -338,9 +320,7 @@ Section WithParameters.
rewrite !word.unsigned_of_Z. unfold word.wrap. cbn.
ssplit; try reflexivity.
** simpl. eapply DONE_related.
** eapply word.unsigned_inj.
rewrite word.unsigned_slu. 2: rewrite word.unsigned_of_Z. 2: reflexivity.
rewrite !word.unsigned_of_Z. reflexivity.
** ZnWords.
- (* state_machine_write_to_device_write: *)
destruct H as (sH' & ? & ?). subst.
unfold write_step in H1.
Expand Down

0 comments on commit c4b8e89

Please sign in to comment.