rocq-demo/rocq_hdl.v

@@ -56,11 +56,12 @@ 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
-      principles, something like "All reacheable states from an initial
-      state are valid", and use the above theorems to prove it (TODO). *)
+      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. This will be
+      done later on. *)
 
-  (*  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 +82,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 +156,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.
@@ -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.