diff --git a/firmware/IncrementWait/CavaIncrementDevice.v b/firmware/IncrementWait/CavaIncrementDevice.v index e45667096..890b92fc4 100644 --- a/firmware/IncrementWait/CavaIncrementDevice.v +++ b/firmware/IncrementWait/CavaIncrementDevice.v @@ -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. @@ -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. @@ -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. @@ -219,8 +223,7 @@ 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 _). @@ -228,47 +231,34 @@ Section WithParameters. 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. @@ -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 _). @@ -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. @@ -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 _). @@ -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.