Format,

Starts with a very simple example, including a proof by induction.

crates/fayalite/src/int.rs

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

crates/fayalite/src/sim/value.rs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

rocq-demo/rocq_hdl.v

@@ -1,385 +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 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

@@ -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.

scripts/check-copyright.sh

@@ -32,7 +32,6 @@ 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()
 {
@@ -65,9 +64,6 @@ 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"
             ;;