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/2] 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 0000000..ede2f71
--- /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 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 2/2] 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 ede2f71..9365870 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.