programmerjake/fayalite
1
0
Fork 0
forked from libre-chip/fayalite
Code Activity
fayalite/rocq-demo/rocq_hdl.v

385 lines
12 KiB
Coq
Raw Blame History

(* 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.
View git blame Copy permalink