rocq-demo/rocq_hdl.v

@@ -0,0 +1,171 @@
+(*  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.
+
+(*  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.

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"
             ;;