Define design safety, and prove it for 1-step and 2-step induction.

If we ever add Verilog files, we can "or" both results, I guess.

crates/fayalite/src/int.rs

@@ -14,8 +14,9 @@ use crate::{
     sim::value::{SimValue, ToSimValueWithType},
     source_location::SourceLocation,
     ty::{
-        CanonicalType, OpaqueSimValueSize, OpaqueSimValueSlice, OpaqueSimValueWriter,
-        OpaqueSimValueWritten, StaticType, Type, TypeProperties, impl_match_variant_as_self,
+        CanonicalType, FillInDefaultedGenerics, OpaqueSimValueSize, OpaqueSimValueSlice,
+        OpaqueSimValueWriter, OpaqueSimValueWritten, StaticType, Type, TypeProperties,
+        impl_match_variant_as_self,
     },
     util::{ConstBool, ConstUsize, GenericConstBool, GenericConstUsize, interned_bit, slice_range},
 };
@@ -113,7 +114,11 @@ impl_known_size_base! {
 }
 
 pub trait KnownSize:
-    GenericConstUsize + sealed::SizeTypeSealed + sealed::SizeSealed + Default
+    GenericConstUsize
+    + sealed::SizeTypeSealed
+    + sealed::SizeSealed
+    + Default
+    + FillInDefaultedGenerics<Type = Self>
 {
     const SIZE: Self;
     type ArrayMatch<Element: Type>: AsRef<[Expr<Element>]>
@@ -161,6 +166,7 @@ pub trait SizeType:
     + 'static
     + Serialize
     + DeserializeOwned
+    + FillInDefaultedGenerics<Type = Self>
 {
     type Size: Size<SizeType = Self>;
 }

crates/fayalite/src/sim/value.rs

@@ -358,11 +358,7 @@ impl<T: Type> DerefMut for SimValue<T> {
 
 impl<T: Type> fmt::Debug for SimValue<T> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        let inner = self.inner.share();
-        f.debug_struct("SimValue")
-            .field("ty", &inner.ty)
-            .field("value", &inner.value)
-            .finish()
+        T::SimValue::fmt(&**self, f)
     }
 }
 

crates/fayalite/tests/sim/expected/extern_module2.txt

@@ -354,12 +354,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x1_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x1_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -404,12 +401,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x1_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x1_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/ripple_counter.txt

@@ -1505,12 +1505,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -1555,12 +1552,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -1605,12 +1599,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -1655,12 +1646,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {
@@ -1704,12 +1692,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {
@@ -1753,12 +1738,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_fork_join.txt

@@ -456,12 +456,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -506,12 +503,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt

@@ -456,12 +456,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -506,12 +503,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_only_connects.txt

@@ -1583,12 +1583,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 6, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x1_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x1_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -1633,12 +1630,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 13, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x1_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x1_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -1683,12 +1677,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x1_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x1_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {
@@ -1732,12 +1723,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x1_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x1_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_read_past.txt

@@ -9655,12 +9655,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -9705,12 +9702,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt

@@ -384,12 +384,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: AsyncReset,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -434,12 +431,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -484,12 +478,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: AsyncReset,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {
@@ -533,12 +524,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt

@@ -384,12 +384,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: AsyncReset,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -434,12 +431,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -484,12 +478,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: AsyncReset,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {
@@ -533,12 +524,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt

@@ -384,12 +384,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -434,12 +431,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -484,12 +478,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt

@@ -384,12 +384,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -434,12 +431,9 @@ Simulation {
                         sim_only_slots: StatePartIndexRange<SimOnlySlots> { start: 0, len: 0 },
                     },
                     write: None,
-                }: SimValue {
-                    ty: Clock,
-                    value: OpaqueSimValue {
-                        bits: 0x0_u1,
-                        sim_only_values: [],
-                    },
+                }: OpaqueSimValue {
+                    bits: 0x0_u1,
+                    sim_only_values: [],
                 },
             },
             changed: Cell {
@@ -484,12 +478,9 @@ Simulation {
             },
             write: None,
         }: (
-            SimValue {
-                ty: Clock,
-                value: OpaqueSimValue {
-                    bits: 0x0_u1,
-                    sim_only_values: [],
-                },
+            OpaqueSimValue {
+                bits: 0x0_u1,
+                sim_only_values: [],
             },
             {
                 SensitivitySet {

rocq-demo/rocq_hdl.v

@@ -0,0 +1,385 @@
+(*  SPDX-License-Identifier: LGPL-3.0-or-later
+    See Notices.txt for copyright information *)
+
+(*  This file demonstrates converting simple HDL designs into Rocq, as well
+    as proofs by induction that parallels those of formal verification in
+    Symbiyosys with the "smtbmc" engine in the "prove" mode. *)
+
+(*  Models a simple register, feeding back to itself. We prove that,
+    when initialized to zero, it stays always at zero. *)
+Module simple_register.
+
+  (*  State record. Contains only one boolean variable, which we call "a" *)
+  Record S := { a: bool }.
+  (*  The above automatically defines an accessor function "a: S->bool", so
+      we can write "a s" to get the value of "a" in state "s". *)
+
+  (*  Defines an "initial" predicate, so "initial s" means
+      "s is an initial state". In our case, the value of "a"
+      in the initial state is zero (false) *)
+  Definition initial (s: S) :=
+    a s = false.
+  (*  As an example, we construct a state where "a" is indeed false,
+      and prove it is an initial state. The syntax for instantiating
+      such a record is "{| a := false |}". *)
+  Example test_initial: initial {| a := false |}.
+  Proof. reflexivity. Qed.
+
+  (*  Defines an "assert" predicate, so "assert s" means "assertions
+      hold in state s" or equivalently "state s is valid". In our case,
+      valid states correspond to those where "a" is false. *)
+  Definition assert (s: S) :=
+    a s = false.
+
+  (*  The following proof by induction follows the article "Temporal
+      Induction by Incremental SAT Solving",
+      https://doi.org/10.1016/S1571-0661(05)82542-3 *)
+  (*  Proves the base case, with one step: the initial state is a
+      valid state. *)
+  Theorem base1: forall s0, initial s0 -> assert s0.
+  Proof. trivial. Qed.
+
+  (*  Defines a "transition" predicate, so "t s1 s2" means:
+      "s2 can be reached in one step from s1". In our case,
+      the value of "a" in s2 is the same as in s1. *)
+  Definition t (s1 s2 : S) :=
+    a s2 = a s1.
+
+  (*  Induction principle: for all transitions from a valid state,
+      we reach a valid state. *)
+  Theorem induct1:
+    forall s0 s1, assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold t,  assert.
+    intros s0 s1 A T.
+    transitivity (a s0).
+    apply T. apply A.
+  Qed.
+  (*  Here we have proven the base case and the inductive case, so we
+      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 reachable in one step from the initial state
+      are valid. *)
+  Example one_step_valid:
+    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold initial, t, assert.
+    intros s0 s1 I T.
+    transitivity (a s0).
+    apply T. apply I.
+  Qed.
+  (*  Same as above, but we prove using only the induction theorems. *)
+  Example one_step_valid':
+    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
+  Proof.
+    apply induct1.
+  Qed.
+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 unreachable valid states that
+    leads to invalid states. A two step induction solves the problem. *)
+Module hidden_state.
+  (*  Demonstrate state with several (two) variables. *)
+  Record S :=
+  { a: bool
+  ; b: bool
+  }.
+  (*  Both registers start at zero (false). *)
+  Definition initial (s: S) :=
+    a s = false /\ b s = false.
+  (*  Just b is constrained to be zero (false) *)
+  Definition assert (s: S) :=
+    b s = false.
+  (*  "a" keeps its previous value, "b" copies "a". *)
+  Definition t (s1 s2 : S) :=
+    a s2 = a s1 /\ b s2 = a s1.
+  (*  Base case in one step. *)
+  Theorem base1:
+    forall s0,
+    initial s0 -> assert s0.
+  Proof.
+    unfold initial, assert.
+    intros s0 [_ H].
+    apply H.
+  Qed.
+  (*  Try proving the inductive case in one step. *)
+  Theorem induct1:
+    forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    unfold t, assert.
+    intros s0 s1 A T.
+    destruct T as [_ Tb].
+    transitivity (a s0). apply Tb.
+  Abort.
+  (*  Ops, we reach a dead-end. Maybe it's not provable after all?
+      Try proving its negation by finding a counter-example. *)
+  Theorem not_induct1:
+    not (forall s0 s1,
+    assert s0 -> t s0 s1 -> assert s1).
+  Proof.
+    unfold not, assert, t.
+    intros H.
+    specialize H with (s0 := {|a := true; b := false|}).
+    simpl in H.
+    specialize H with (s1 := {|a := true; b := true|}).
+    simpl in H.
+    discriminate H. reflexivity. auto.
+  Qed.
+  (*  Indeed, a valid state where "a" is one (true) leads to
+      an invalid state. Try one more step. *)
+  Theorem base2:
+    forall s0 s1,
+    initial s0 -> assert s0 -> t s0 s1 -> assert s1.
+  Proof.
+    intros s0 s1 [Ia _] _ [_ Tb].
+    unfold assert.
+    transitivity (a s0). apply Tb.
+    apply Ia.
+  Qed.
+  Theorem induct2:
+    forall s0 s1 s2,
+    assert s0 -> t s0 s1 -> assert s1 -> t s1 s2 -> assert s2.
+  Proof.
+    intros s0 s1 s2 A0 [T0a T0b] A1 [T1a T1b].
+    unfold assert in *.
+    transitivity (a s1). apply T1b.
+    transitivity (a s0). apply T0a.
+    transitivity (b s1). symmetry. apply T0b.
+    apply A1.
+  Qed.
+  (* Success! Two steps indeed work. *)
+
+  (* 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.
+  Proof.
+    intros s0 s1 s2.
+    intros Hi T01.
+    apply induct2 with (s0 := s0).
+    - apply base1. apply Hi.
+    - apply T01.
+    - apply base2 with (s0 := s0).
+      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.

rocq-demo/rocq_playground.v

@@ -1,79 +0,0 @@
-(*  SPDX-License-Identifier: LGPL-3.0-or-later
-    See Notices.txt for copyright information *)
-
-(** This file demonstrates converting simple HDL designs into Rocq, as well
-    as proofs by induction that parallels those of formal verification in
-    Symbiyosys with the "smtbmc" engine in the "prove" mode. *)
-
-(** Models a simple register, feeding back to itself. We prove that,
-    when initialized to zero, it stays always at zero. *)
-Module simple_register.
-
-  (*  State record. Contains only one boolean variable, which we call "a" *)
-  Record S := { a: bool }.
-  (*  The above automatically defines an accessor function "a: S->bool", so
-      we can write "a s" to get the value of "a" in state "s". *)
-
-  (*  Defines an "initial" predicate, so "initial s" means
-      "s is an initial state". In our case, the value of "a"
-      in the initial state is zero (false) *)
-  Definition initial (s: S) :=
-    a s = false.
-  (*  As an example, we construct a state where "a" is indeed false,
-      and prove it is an initial state. The syntax for instantiating
-      such a record is "{| a := false |}". *)
-  Example test_initial: initial {| a := false |}.
-  Proof. reflexivity. Qed.
-
-  (*  Defines an "assert" predicate, so "assert s" means "assertions
-      hold in state s" or equivalently "state s is valid". In our case,
-      valid states correspond to those where "a" is false. *)
-  Definition assert (s: S) :=
-    a s = false.
-
-  (*  The following proof by induction follows the article "Temporal
-      Induction by Incremental SAT Solving",
-      https://doi.org/10.1016/S1571-0661(05)82542-3 *)
-  (*  Proves the base case, with one step: the initial state is a
-      valid state. *)
-  Theorem base1: forall s0, initial s0 -> assert s0.
-  Proof. trivial. Qed.
-
-  (*  Defines a "transition" predicate, so "t s1 s2" means:
-      "s2 can be reached in one step from s1". In our case,
-      the value of "a" in s2 is the same as in s1. *)
-  Definition t (s1 s2 : S) :=
-    a s2 = a s1.
-
-  (*  Induction principle: for all transitions from a valid state,
-      we reach a valid state. *)
-  Theorem induct1:
-    forall s0 s1, assert s0 -> t s0 s1 -> assert s1.
-  Proof.
-    unfold t,  assert.
-    intros s0 s1 A T.
-    transitivity (a s0).
-    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). *)
-
-  (*  Example: all states reacheable in one step from the initial state
-      are valid. *)
-  Example one_step_valid:
-    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
-  Proof.
-    unfold initial, t, assert.
-    intros s0 s1 I T.
-    transitivity (a s0).
-    apply T. apply I.
-  Qed.
-  (*  Same as above, but we prove using only the induction theorems. *)
-  Example one_step_valid':
-    forall s0 s1, initial s0 -> t s0 s1 -> assert s1.
-  Proof.
-    apply induct1.
-  Qed.
-End simple_register.

scripts/check-copyright.sh

@@ -32,6 +32,7 @@ POUND_HEADER=('^"# SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"# See Notice
 SLASH_HEADER=('^"// SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"// See Notices.txt for copyright information"$')
 MD_HEADER=('^"<!--"$' '^"SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"See Notices.txt for copyright information"$')
 JSON_HEADER=('^"{"$' '^"    \"license_header\": ["$' '^"        \"SPDX-License-Identifier: LGPL-3.0-or-later\","$' '^"        \"See Notices.txt for copyright information\""')
+ROCQ_HEADER=('^"(*  SPDX-License-Identifier: LGPL-3.0-or-later"$' '^"   See Notices.txt for copyright information *)"$')
 
 function main()
 {
@@ -64,6 +65,9 @@ function main()
         *.json)
             check_file "$file" "${JSON_HEADER[@]}"
             ;;
+        *.v)
+            check_file "$file" "${ROCQ_HEADER[@]}"
+            ;;
         *)
             fail_file "$file" 0 "unimplemented file kind -- you need to add it to $0"
             ;;