From 02de335e46b5caeb161bbbb25d0832c34353bda5 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 24 Nov 2025 21:55:42 -0300
Subject: [PATCH 1/9] Demonstrate a preliminary mapping from HDL to Rocq.

Starts with a very simple example, including a proof by induction.
---
 rocq-demo/rocq_playground.v | 79 +++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 rocq-demo/rocq_playground.v

diff --git a/rocq-demo/rocq_playground.v b/rocq-demo/rocq_playground.v
new file mode 100644
index 00000000..ede2f71e
--- /dev/null
+++ b/rocq-demo/rocq_playground.v
@@ -0,0 +1,79 @@
+(*  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.

From 46f3519c76fa244caacde18a733e44bfc084a78d Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 24 Nov 2025 21:55:42 -0300
Subject: [PATCH 2/9] Demonstrate a preliminary mapping from HDL to Rocq.

Starts with a very simple example, including a proof by induction.
---
 rocq-demo/rocq_hdl.v | 79 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 rocq-demo/rocq_hdl.v

diff --git a/rocq-demo/rocq_hdl.v b/rocq-demo/rocq_hdl.v
new file mode 100644
index 00000000..ede2f71e
--- /dev/null
+++ b/rocq-demo/rocq_hdl.v
@@ -0,0 +1,79 @@
+(*  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.

From c32cdee4f7ddc03138d06ed65ae8cd588c37243c Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 8 Dec 2025 21:49:05 -0300
Subject: [PATCH 3/9] Format,

---
 rocq-demo/rocq_playground.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/rocq-demo/rocq_playground.v b/rocq-demo/rocq_playground.v
index ede2f71e..93658709 100644
--- a/rocq-demo/rocq_playground.v
+++ b/rocq-demo/rocq_playground.v
@@ -1,11 +1,11 @@
 (*  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
+(** 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,
+(** Models a simple register, feeding back to itself. We prove that,
     when initialized to zero, it stays always at zero. *)
 Module simple_register.
 

From e54558d848f92006d0b3151fe84244e9a031d446 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 8 Dec 2025 21:38:47 -0300
Subject: [PATCH 4/9] Demonstrates state with multiple variables and hidden
 state.

---
 rocq-demo/rocq_hdl.v | 92 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)

diff --git a/rocq-demo/rocq_hdl.v b/rocq-demo/rocq_hdl.v
index ede2f71e..74082261 100644
--- a/rocq-demo/rocq_hdl.v
+++ b/rocq-demo/rocq_hdl.v
@@ -77,3 +77,95 @@ Module simple_register.
     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 unreacheable 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 reacheable 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.

From e4210a672f6ff60139236fb000b35b08955e9fa8 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Tue, 9 Dec 2025 07:45:35 -0300
Subject: [PATCH 5/9] Check copyright header in Rocq files.

If we ever add Verilog files, we can "or" both results, I guess.
---
 scripts/check-copyright.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/scripts/check-copyright.sh b/scripts/check-copyright.sh
index 3651931f..023cd21f 100755
--- a/scripts/check-copyright.sh
+++ b/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"
             ;;

From fbe4585578a043829bfb4d5af087fc7f4bf010b8 Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Wed, 10 Dec 2025 20:03:29 -0800
Subject: [PATCH 6/9] add FillInDefaultedGenerics<Type = Self> bound for
 SizeType

---
 crates/fayalite/src/int.rs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/crates/fayalite/src/int.rs b/crates/fayalite/src/int.rs
index 524ef271..2d1f6d2c 100644
--- a/crates/fayalite/src/int.rs
+++ b/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>;
 }

From c97b44d9d646a4aa64fcc046538fc2354bb708ee Mon Sep 17 00:00:00 2001
From: Jacob Lifshay <programmerjake@gmail.com>
Date: Sun, 14 Dec 2025 20:41:16 -0800
Subject: [PATCH 7/9] simplify SimValue Debug format, making complex structures
 much easier to read

---
 crates/fayalite/src/sim/value.rs              |  6 +--
 .../tests/sim/expected/extern_module2.txt     | 18 +++----
 .../tests/sim/expected/ripple_counter.txt     | 54 +++++++------------
 .../tests/sim/expected/sim_fork_join.txt      | 18 +++----
 .../sim/expected/sim_fork_join_scope.txt      | 18 +++----
 .../tests/sim/expected/sim_only_connects.txt  | 36 +++++--------
 .../tests/sim/expected/sim_read_past.txt      | 18 +++----
 .../expected/sim_resettable_counter_async.txt | 36 +++++--------
 ...settable_counter_async_immediate_reset.txt | 36 +++++--------
 .../expected/sim_resettable_counter_sync.txt  | 27 ++++------
 ...esettable_counter_sync_immediate_reset.txt | 27 ++++------
 11 files changed, 97 insertions(+), 197 deletions(-)

diff --git a/crates/fayalite/src/sim/value.rs b/crates/fayalite/src/sim/value.rs
index def2ae32..b6a4e4be 100644
--- a/crates/fayalite/src/sim/value.rs
+++ b/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)
     }
 }
 
diff --git a/crates/fayalite/tests/sim/expected/extern_module2.txt b/crates/fayalite/tests/sim/expected/extern_module2.txt
index fa6e767e..365830fa 100644
--- a/crates/fayalite/tests/sim/expected/extern_module2.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/ripple_counter.txt b/crates/fayalite/tests/sim/expected/ripple_counter.txt
index 9cc5f021..2be69b51 100644
--- a/crates/fayalite/tests/sim/expected/ripple_counter.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_fork_join.txt b/crates/fayalite/tests/sim/expected/sim_fork_join.txt
index 680fedb9..df9c092a 100644
--- a/crates/fayalite/tests/sim/expected/sim_fork_join.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt b/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt
index 40d16a90..917dd5d1 100644
--- a/crates/fayalite/tests/sim/expected/sim_fork_join_scope.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_only_connects.txt b/crates/fayalite/tests/sim/expected/sim_only_connects.txt
index 15456d20..af41fe27 100644
--- a/crates/fayalite/tests/sim/expected/sim_only_connects.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_read_past.txt b/crates/fayalite/tests/sim/expected/sim_read_past.txt
index 475943ec..6df4571b 100644
--- a/crates/fayalite/tests/sim/expected/sim_read_past.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt
index 7b11157c..3fea9282 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt
index 0ca767a7..2283ce5a 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_async_immediate_reset.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt
index 4af2eb62..c77046f5 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync.txt
+++ b/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 {
diff --git a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt b/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt
index 45f09d20..e1c565a1 100644
--- a/crates/fayalite/tests/sim/expected/sim_resettable_counter_sync_immediate_reset.txt
+++ b/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 {

From 4fd4371054ab89f10749de879400ada58c4dfab2 Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Wed, 10 Dec 2025 17:13:23 -0300
Subject: [PATCH 8/9] 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.

From a398f8f185549b016d13aebce585a40b78fbf05f Mon Sep 17 00:00:00 2001
From: Cesar Strauss <cestrauss@gmail.com>
Date: Mon, 22 Dec 2025 17:32:56 -0300
Subject: [PATCH 9/9] 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 95b1627a..28ceb071 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.