Redo the increment device in Cava2. #904
Conversation
| let '(s', (is_resp, resp)) := step incr s (bool_to_dbit is_read_req, | ||
| (bool_to_dbit is_write_req, | ||
| (req_addr, (req_value, tt)))) in | ||
| (s', (dbit_to_bool is_resp, resp)). |
There was a problem hiding this comment.
Seeing all these bool_to_dbit and dbit_to_bool conversions makes me wonder whether Notation Bit := (BitVec 1) in Cava2 was really a good idea... Why not add back a separate Bit type that gets denoted to bool? (/cc @jadephilipoom and @blaxill)
There was a problem hiding this comment.
Yeah, I think it might be a good idea to add this back. My initial rationale for removing it was to avoid duplication of bitwise operations, but I think logically you really do want to sometimes reason about numbers and sometimes just reason about booleans.
There was a problem hiding this comment.
bool_to_dbit and dbit_to_bool are not really necessary, I just didn't want to change the device class while cava2 was changing. The bool/number distinction doesn't affect the proof below much (though it might for other proofs). That said, it feels weird to use N instead of bool.
|
|
||
| Axiom TODO: False. | ||
| Axiom TODO: Coq.Init.Logic.False. |
There was a problem hiding this comment.
Does False here still refer to Cava's False? That doesn't sound right, can we put it into a Notations module that gets only imported inside sections where we really want it?
| + (* DONE_related: *) | ||
| cbn. rewrite andb_false_r. cbn. assumption. | ||
| change (0%N) at 1 with (bool_to_dbit false). | ||
| change (1%N) with (bool_to_dbit true). |
There was a problem hiding this comment.
More code suggesting that we should consider again a separate Bit type that gets denoted to bool, /cc @jadephilipoom @blaxill
|
Looks great! (And I think the CI failure is due to #893) |
|
All (the pull request submitter and all commit authors) CLAs are signed, but one or more commits were authored or co-authored by someone other than the pull request submitter. We need to confirm that all authors are ok with their commits being contributed to this project. Please have them confirm that by leaving a comment that contains only Note to project maintainer: There may be cases where the author cannot leave a comment, or the comment is not properly detected as consent. In those cases, you can manually confirm consent of the commit author(s), and set the ℹ️ Googlers: Go here for more info. |
No description provided.