From 46f3519c76fa244caacde18a733e44bfc084a78d Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 24 Nov 2025 21:55:42 -0300 Subject: [PATCH 1/7] 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 e54558d848f92006d0b3151fe84244e9a031d446 Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 8 Dec 2025 21:38:47 -0300 Subject: [PATCH 2/7] 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 Date: Tue, 9 Dec 2025 07:45:35 -0300 Subject: [PATCH 3/7] 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=('^"