From 4fd4371054ab89f10749de879400ada58c4dfab2 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Wed, 10 Dec 2025 17:13:23 -0300 Subject: [PATCH 1/2] 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 7408226..95b1627 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. -- 2.49.1 From a398f8f185549b016d13aebce585a40b78fbf05f Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 22 Dec 2025 17:32:56 -0300 Subject: [PATCH 2/2] Define design safety, and prove it for 1-step and 2-step induction. --- rocq-demo/rocq_hdl.v | 218 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 216 insertions(+), 2 deletions(-) diff --git a/rocq-demo/rocq_hdl.v b/rocq-demo/rocq_hdl.v index 95b1627..28ceb07 100644 --- a/rocq-demo/rocq_hdl.v +++ b/rocq-demo/rocq_hdl.v @@ -56,9 +56,10 @@ Module simple_register. apply T. apply A. 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 + declare success. However, we want to formalize it from first principles, something like "All reachable states from an initial - state are valid", and use the above theorems to prove it (TODO). *) + state are valid", and use the above theorems to prove it. This will be + done later on. *) (* Example: all states reachable in one step from the initial state are valid. *) @@ -169,3 +170,216 @@ Module hidden_state. apply Hi. apply base1. apply Hi. apply T01. Qed. End hidden_state. + +(* We now formalize the notion of a safe design, where all reachable states + from an initial state are valid. This will allow us to prove that the + above designs are truly safe for all time. *) + +Section safety. + + (* define some shortcuts *) + Variable S: Type. (* state type *) + Variable I: S->Prop. (* initial state *) + Variable t: S->S->Prop. (* transition rule *) + Variable A: S->Prop. (* assertions *) + + (* Given an initial state and transition rule, recursively construct the + "reachable" concept *) + Inductive reachable: S->Prop := + (* initial states are reachable *) + | r_initial: forall s0: S, + I s0 -> reachable s0 + (* from a given reachable state, we get to another reachable state by + following a transition *) + | r_step: forall s0 s1: S, + reachable s0 -> t s0 s1 -> reachable s1. + + (* example: all states leading from an initial state are reachable *) + Example reachable_in_one_step: + forall s0 s1: S, + I s0 -> t s0 s1 -> reachable s1. + Proof. + intros s0 s1. + intros I0. + apply r_step. + apply r_initial. + exact I0. + Qed. + + (* Safety definition: all reachable states are valid (they obey + assertions) *) + Definition safe: Prop := + forall s: S, reachable s -> A s. + + (* Prove the induction principle for one-step induction: from a base case + and an inductive case, we prove full safety. This is enough to handle + cases where induction already succeeds in just one step, like the + "simple_register" example above. *) + Theorem safe1: + (* Hypothesis: *) + (* 1) base case *) + (forall s0: S, I s0 -> A s0) -> + (* 2) inductive case *) + (forall s0 s1: S, A s0 -> t s0 s1 -> A s1) -> + (* Conclusion: safe for all time *) + safe. + Proof. + intros B1 I1. + unfold safe. + (* Here we take advantage of an induction principle which is automatically + generated by Rocq when we defined the "reachable" proposition above. It + conveniently matches the base case and inductive cases from the + hypothesis *) + apply reachable_ind. + - exact B1. + - intros s0 s1 R0. + apply I1. + Qed. + + (* Now, we proceed to prove the induction principle to designs that require + two steps in induction, like the "hidden_state" design above. *) + + (* The "reachable_ind" induction principle that Rocq generated for us no + longer matches the hypothesis for the two-step case. We create another + "reachable2" property that does.*) + Inductive reachable2: S->Prop := + (* initial states are "reachable2" *) + | r2_initial1: forall s0: S, + I s0 -> reachable2 s0 + (* states one transition away from "reachable2" initial states are also + "reachable2" *) + | r2_initial2: forall s0 s1: S, + I s0 -> reachable2 s0 -> t s0 s1 -> reachable2 s1 + (* from two sequential "reachable2" states, we get another "reachable2"] + state by jumping yet another transition. *) + | r2_step: forall s0 s1 s2: S, + reachable2 s0 -> t s0 s1 -> reachable2 s1 -> t s1 s2 -> reachable2 s2. + + (* example: if, from an initial state, we jump two states, we reach a + "reachable2" state *) + Example reachable2_in_two_steps: + forall (s0 s1 s2: S), + I s0 -> t s0 s1 -> t s1 s2 -> reachable2 s2. + Proof. + intros s0 s1 s2. + intros I0 T01. + apply r2_step with (s0 := s0). + + apply r2_initial1. apply I0. + + exact T01. + + apply r2_initial2 with (s0:=s0). + exact I0. apply r2_initial1. exact I0. exact T01. + Qed. + + (* First, we prove the safety property for "reachable2". Later, we will use + this result to prove the desired theorem for "reachable" instead *) + Lemma safe2': + (* Hypothesis: *) + (* 1) base case (step 1) *) + (forall s0: S, I s0 -> A s0) -> + (* 2) base case (step 2) *) + (forall s0 s1: S, I s0 -> A s0 -> t s0 s1 -> A s1) -> + (* 3) inductive case *) + (forall s0 s1 s2: S, A s0 -> t s0 s1 -> A s1 -> t s1 s2 -> A s2) -> + (* Conclusion: "reachable2" is safe *) + forall s, reachable2 s -> A s. + Proof. + intros B1 B2 I2. + (* With our carefully crafted "reachable2", Rocq generates an induction + principle that matches our hypothesis. *) + apply reachable2_ind. + - exact B1. + - intros s0 s1 I0 R0. apply B2. exact I0. + - intros s0 s1 s2 R0 A0 T01 R1. + apply I2 with (s0 := s0). + exact A0. exact T01. + Qed. + + (* Now, we proceed to prove the same result for plain "reachable". We first + need to prove two auxiliary lemmas. *) + + Lemma reachable2_t: + forall s1 s2:S, reachable2 s1 -> t s1 s2 -> reachable2 s2. + Proof. + intros s1 s2 R1. + destruct R1 as [s1 I1| s0 s1 I0 R0 T01|sm1 s0 s1 Rm1 Tm10 R0 T01]. + - apply r2_initial2. exact I1. apply r2_initial1. exact I1. + - apply r2_step with (s0:=s0). + + exact R0. + + exact T01. + + apply r2_initial2 with (s0:=s0). exact I0. exact R0. exact T01. + - apply r2_step with (s0 := s0). + exact R0. exact T01. + apply r2_step with (s1 := s0) (s0 := sm1). + exact Rm1. exact Tm10. exact R0. exact T01. + Qed. + + Lemma reachable1_2: + forall s: S, reachable s -> reachable2 s. + Proof. + intros s R. + apply reachable_ind. + - exact r2_initial1. + - intros s0 s1 R0. + apply reachable2_t. + - exact R. + Qed. + + (* Finally, the main result: safety for 2-step induction. *) + Theorem safe2: + (* Hypothesis: *) + (* 1) base case (step 1) *) + (forall s0: S, I s0 -> A s0) -> + (* 2) base case (step 2) *) + (forall s0 s1: S, I s0 -> A s0 -> t s0 s1 -> A s1) -> + (* 3) inductive case *) + (forall s0 s1 s2: S, A s0 -> t s0 s1 -> A s1 -> t s1 s2 -> A s2) -> + (* Conclusion: safe for all time *) + safe. + Proof. + intros B1 B2 I2. + unfold safe. + intros s R. + apply safe2'. + exact B1. exact B2. exact I2. + apply reachable1_2. exact R. + Qed. + + (* A future step, maybe, would be to prove the safety of n-step induction, + for arbitrary n. *) + +End safety. + +(* We use the above results to prove that "simple_register" is indeed safe. *) +Module simple_register_safe. + Theorem simple_register_is_safe: + (* instantiate the safety property for our design *) + safe + simple_register.S + simple_register.initial + simple_register.t + simple_register.assert. + Proof. + (* apply the induction principle for 1-step induction *) + apply safe1. + - exact simple_register.base1. + - exact simple_register.induct1. + Qed. +End simple_register_safe. + +(* Likewise for "hidden_state". *) +Module hidden_state_safe. + Theorem hidden_state_is_safe: + (* instantiate the safety property for our design *) + safe + hidden_state.S + hidden_state.initial + hidden_state.t + hidden_state.assert. + Proof. + (* apply the induction principle for 2-step induction *) + apply safe2. + - exact hidden_state.base1. + - exact hidden_state.base2. + - exact hidden_state.induct2. + Qed. +End hidden_state_safe. -- 2.49.1