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