(*  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.