File size: 4,006 Bytes
7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 a9ea017 7e1c831 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 | (* One pass of the organism, checked against the spec in every configuration a run can visit. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Abstract Indep Spec Organism.
Definition G := length organism.
Definition rec_eqb (r s : rec) : bool :=
match r, s with
| Rec a b c d e f, Rec a' b' c' d' e' f' =>
Nat.eqb a a' && Z.eqb b b' && Nat.eqb c c' && Z.eqb d d' && Z.eqb e e' && Nat.eqb f f'
end.
Lemma rec_eqb_true : forall r s, rec_eqb r s = true -> r = s.
Proof.
intros [a b c d e f] [a' b' c' d' e' f'] H. cbn in H.
repeat match goal with H : _ && _ = true |- _ => apply andb_prop in H as [? ?] end.
repeat match goal with
| H : Nat.eqb _ _ = true |- _ => apply Nat.eqb_eq in H
| H : Z.eqb _ _ = true |- _ => apply Z.eqb_eq in H
end.
subst. reflexivity.
Qed.
Lemma decode_organism : forall r, In r organism -> decodeA 6 (enc_recA 6 r) = r.
Proof.
intros r Hr.
assert (H : forallb (fun r => rec_eqb (decodeA 6 (enc_recA 6 r)) r) organism = true) by (vm_compute; reflexivity).
rewrite forallb_forall in H. apply rec_eqb_true. apply H. exact Hr.
Qed.
Lemma wbr_organism : wbr_from organism istmp [] = true.
Proof. vm_compute. reflexivity. Qed.
Lemma length_organism : G = 143.
Proof. reflexivity. Qed.
(* the summary of each head that a pass must leave *)
Definition expR (o : out) (r : bool) : ahead :=
mkH r None (if rr o then 0 else if cons o then 1 else 0) (rr o) false.
Definition expA (o : out) (x : bool) : ahead :=
mkH x (Some (if emit o then av o else x)) (if home o then 0 else if emit o then 1 else 0) (home o) (fresh o).
Definition expK (o : out) (r y : bool) : ahead :=
mkH y (Some (if cw o then r else y)) (if home o then 0 else if cw o then 1 else 0) (home o) (fresh o).
Definition oeqb (a b : option bool) : bool :=
match a, b with Some x, Some y => Bool.eqb x y | None, None => true | _, _ => false end.
Definition ahead_eqb (h1 h2 : ahead) : bool :=
Bool.eqb (acur h1) (acur h2) && oeqb (awr h1) (awr h2) && Nat.eqb (amv h1) (amv h2)
&& Bool.eqb (arw h1) (arw h2) && Bool.eqb (acl h1) (acl h2).
Lemma ahead_eqb_true : forall h1 h2, ahead_eqb h1 h2 = true -> h1 = h2.
Proof.
intros [c1 w1 m1 r1 l1] [c2 w2 m2 r2 l2] H. unfold ahead_eqb in H. cbn [acur awr amv arw acl] in H.
apply andb_prop in H as [H Hl]. apply andb_prop in H as [H Hr]. apply andb_prop in H as [H Hm].
apply andb_prop in H as [Hc Hw].
apply Bool.eqb_prop in Hc, Hr, Hl. apply Nat.eqb_eq in Hm. subst.
destruct w1 as [x|], w2 as [y|]; cbn [oeqb] in Hw; try discriminate; [|reflexivity].
apply Bool.eqb_prop in Hw. subst. reflexivity.
Qed.
Definition start_ast (w : list bool) (r x y : bool) : ast :=
mkAS w (mkH r None 0 false false) (mkH x None 0 false false) (mkH y None 0 false false) 0 false false.
(* what a pass must leave behind, judged on the abstract state t it reaches *)
Definition chk (o : out) (t : ast) (r x y : bool) : bool :=
negb (bad t)
&& forallb (fun i => Bool.eqb (wget (aw t) i) (wget (wcfg (ncf o)) i)) (filter relevant (seq 0 64))
&& ahead_eqb (aR t) (expR o r) && ahead_eqb (aA t) (expA o x) && ahead_eqb (aK t) (expK o r y)
&& Bool.eqb (aho t) (ho o).
Definition all_cfgs : list cfg :=
flat_map (fun p =>
flat_map (fun zz =>
flat_map (fun b3 => flat_map (fun b2 => flat_map (fun b1 => flat_map (fun b0 =>
map (fun mm => mkC p zz b3 b2 b1 b0 mm) [false; true])
[false; true]) [false; true]) [false; true]) [false; true])
(seq 0 (match p with PI => 32 | PC => 4 | PG => 8 | PA => 18 end)))
[PI; PC; PG; PA].
Definition bools := [false; true].
(* the abstract pass from every configuration a run can visit, with every cell under each head *)
Lemma pass_check_ok :
forallb (fun cf => forallb (fun r => forallb (fun x => forallb (fun y =>
chk (dpass cf r) (aiter G organism (start_ast (wcfg cf) r x y)) r x y)
bools) bools) bools) all_cfgs = true.
Proof. vm_compute. reflexivity. Qed.
|