programmerjake/fayalite
1
0
Fork 0
forked from libre-chip/fayalite
Code Activity

Spelling.

Browse source
This commit is contained in:
Cesar Strauss 2025-12-10 17:13:23 -03:00
parent c97b44d9d6
commit 4fd4371054
Signed by: cesar
SSH key fingerprint: SHA256:sJUl6USz0D6c6sAQyFZab8XNPJnT05pt2ES0Lv/hCg4
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
rocq-demo/rocq_hdl.v
View file

@ -57,10 +57,10 @@ Module simple_register.
Qed.
(* Here we have proven the base case and the inductive case, so we
declare success. However, we may want to formalize it from first
principles, something like "All reacheable states from an initial
principles, something like "All reachable states from an initial
state are valid", and use the above theorems to prove it (TODO). *)
(* Example: all states reacheable in one step from the initial state
(* Example: all states reachable in one step from the initial state
are valid. *)
Example one_step_valid:
forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
@ -81,7 +81,7 @@ End simple_register.
(* The same circuit as above, but with an additional output register.
The output is asserted to be always false, but no such restriction
is made on the inner register, a "hidden" state. It creates a
difficulty for induction: there are unreacheable valid states that
difficulty for induction: there are unreachable valid states that
leads to invalid states. A two step induction solves the problem. *)
Module hidden_state.
(* Demonstrate state with several (two) variables. *)
@ -155,7 +155,7 @@ Module hidden_state.
Qed.
(* Success! Two steps indeed work. *)
(* Example: all states reacheable in two steps are valid *)
(* Example: all states reachable in two steps are valid *)
Example two_steps_valid:
forall s0 s1 s2,
initial s0 -> t s0 s1 -> t s1 s2 -> assert s2.