rocq/Compile.v

(* Lemma 3.4 for every unit of weights 1 and -1, whatever its fan-in: the unit fires exactly when at least t = tval of
   its literals hold, at least t literals satisfy the recursion of the lemma, and the records the compiler gives the
   unit, run on a window whose cells hold the values of its literals, leave the unit's value in the cell they write.
   They read and write the window alone, fit the code of the records, and number rcount t k, one for a constant and
   k - 1 for a chain of k >= 2 literals. *)
From Stdlib Require Import List Bool Arith ZArith Lia.
Import ListNotations.
From TH Require Import TwoHead Net Abstract Indep Run View Stored WinRun StoredStep StoredOk StoredCount.

(* at least t of l0 :: rest hold exactly when at least t of rest do, or l0 and at least t - 1 of rest do *)
Lemma atleast_rec : forall w l0 rest t,
  Z.leb t (Z.of_nat (ntrue w (l0 :: rest)))
  = Z.leb t (Z.of_nat (ntrue w rest)) || (wl w l0 && Z.leb (t - 1) (Z.of_nat (ntrue w rest))).
Proof.
  intros w l0 rest t. unfold ntrue. cbn [filter]. destruct (wl w l0); cbn [length andb orb].
  - rewrite Nat2Z.inj_succ. set (c := Z.of_nat (length (filter (wl w) rest))).
    destruct (Z.leb_spec t (Z.succ c)), (Z.leb_spec t c), (Z.leb_spec (t - 1) c); cbn [orb]; first [reflexivity | lia].
  - rewrite orb_false_r. reflexivity.
Qed.

(* a constant, a disjunction, a conjunction: one record, or k - 1 for k >= 2 literals *)
Lemma chlen_cases : forall k, chlen k = (if Nat.leb k 1 then k else k - 1).
Proof. intros [|[|k]]; reflexivity. Qed.

Section Compile.
Variables (W LV : nat) (xc : nat -> nat -> nat) (cell : nat -> nat).
Hypotheses (Hxgt : forall j k, k < 3 -> HO < xc j k) (Hxlt : forall j k, j < LV -> k < 3 -> xc j k < W)
  (Hxinj : forall j k j' k', k < 3 -> k' < 3 -> xc j k = xc j' k' -> j = j' /\ k = k').

(* the literal of an input: the cell of its signal, negated for the weight -1 *)
Definition lit_in (p : nat * Z) : nat * bool := (cell (fst p), Z.ltb 0 (snd p)).

(* the records of unit u, writing d, accumulating its chains in acc, with the levels of scratch cells from 0 *)
Definition urecs (u : tu) (d acc : nat) : list rec := ucomp xc (tval u) (map lit_in (tin u)) d acc 0.

Lemma ntrue_in : forall w (E : nat -> bool) (l : list (nat * Z)),
  (forall i z, In (i, z) l -> wcell w (cell i) = E i) -> ntrue w (map lit_in l) = length (filter (litE E) l).
Proof.
  intros w E l H. unfold ntrue. induction l as [|[i z] l IH]; [reflexivity|]. cbn [map filter].
  assert (Ep : wl w (lit_in (i, z)) = litE E (i, z)).
  { unfold wl, lit_in, litE. cbn [fst snd]. rewrite (H i z (or_introl eq_refl)). reflexivity. }
  assert (IH' : length (filter (wl w) (map lit_in l)) = length (filter (litE E) l))
    by (apply IH; intros i' z' Hin; apply (H i' z'); right; exact Hin).
  rewrite Ep. destruct (litE E (i, z)); cbn [length]; rewrite IH'; reflexivity.
Qed.

Theorem compile_unit : forall (u : tu) (E : nat -> bool) w d acc,
  (forall i z, In (i, z) (tin u) -> z = 1%Z \/ z = (-1)%Z) ->
  (forall i z, In (i, z) (tin u) -> wcell w (cell i) = E i /\ cell i <> acc /\ ~ scr LV xc 0 (cell i)) ->
  length w = W -> ok_cell W d -> ok_cell W acc -> ~ scr LV xc 0 d -> ~ scr LV xc 0 acc ->
  ((1 < tval u < Z.of_nat (length (tin u)))%Z -> length (tin u) <= LV + 2) ->
  let w' := wrun (urecs u d acc) w in
  length w' = W /\ wget w' d = fire u E /\ (forall c, c <> d -> c <> acc -> ~ scr LV xc 0 c -> wget w' c = wget w c).
Proof.
  intros u E w d acc Hw Hlit Hl Hd Ha Hsd Hsa Hlev. unfold urecs. cbv zeta.
  assert (Hls : forall l, In l (map lit_in (tin u)) -> fst l <> acc /\ ~ scr LV xc 0 (fst l)).
  { intros l Hin. apply in_map_iff in Hin as ([i z] & <- & Hin). cbn [lit_in fst].
    destruct (Hlit i z Hin) as (_ & H1 & H2). split; assumption. }
  destruct (ucomp_run W LV xc Hxgt Hxlt Hxinj (map lit_in (tin u)) (tval u) d acc 0 w Hl Hd Ha Hsd Hsa Hls
              ltac:(rewrite length_map; intros H; specialize (Hlev H); lia)) as (L1 & V1 & U1).
  split; [exact L1|]. split; [|exact U1].
  rewrite V1, (fire_count u E Hw), (ntrue_in w E (tin u)) by (intros i z Hin; exact (proj1 (Hlit i z Hin))).
  reflexivity.
Qed.

(* every record reads and writes the window alone, fits the code of a window of N cells, and they number rcount *)
Theorem compile_records : forall u d acc N,
  HO < d -> HO < acc -> (forall i z, In (i, z) (tin u) -> rd_ok (cell i) /\ cell i < N) ->
  (forall j k, j < LV -> k < 3 -> xc j k < N) -> d < N -> acc < N ->
  ((1 < tval u < Z.of_nat (length (tin u)))%Z -> length (tin u) <= LV + 2) ->
  Forall wrec (urecs u d acc) /\ Forall (rok N) (urecs u d acc)
  /\ length (urecs u d acc) = rcount (tval u) (length (tin u)).
Proof.
  intros u d acc N Hd Ha Hc Hxn HdN HaN Hlev. unfold urecs. split; [|split].
  - apply (ucomp_wrec xc Hxgt); [exact Hd | exact Ha|].
    intros l Hin. apply in_map_iff in Hin as ([i z] & <- & Hin). exact (proj1 (Hc i z Hin)).
  - apply (ucomp_rok N LV xc Hxn); [lia | exact HdN | exact HaN | |].
    + intros l Hin. apply in_map_iff in Hin as ([i z] & <- & Hin). exact (proj2 (Hc i z Hin)).
    + rewrite length_map. intros H. specialize (Hlev H). lia.
  - rewrite length_ucomp_eq, length_map. reflexivity.
Qed.

End Compile.