From 4fd4371054ab89f10749de879400ada58c4dfab2 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Wed, 10 Dec 2025 17:13:23 -0300 Subject: [PATCH] Spelling. --- rocq-demo/rocq_hdl.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/rocq-demo/rocq_hdl.v b/rocq-demo/rocq_hdl.v index 74082261..95b1627a 100644 --- a/rocq-demo/rocq_hdl.v +++ b/rocq-demo/rocq_hdl.v @@ -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.