Hugging Face's logo

phanerozoic
/
threshold-computers

threshold-logic
neuromorphic
computer-architecture
recurrent-neural-network
in-memory-computing
self-replication
loihi
truenorth
akida
Model card Files
xet
 Community
threshold-computers / rocq /HostCount.v
phanerozoic's picture
phanerozoic
Put the organism first and move serialization, sizes and the Rocq map to appendices
5ee1fb5
Raw History Blame Contribute Delete
24.5 kB
(* Proposition 5.9 and Appendix B: the units, edges and biases of H_A for every A >= 3, and the identity units and nonzero entries of
Lev(H_A). *)
From Stdlib Require Import List Bool Arith ZArith Lia NArith Morphisms Setoid.
Import ListNotations.
From TH Require Import TwoHead Net Gates Host HostWF Lev BlockLev HostLev.
#[local] Instance nsum_proper : Proper (eq ==> pointwise_relation nat eq ==> eq) nsum.
Proof. intros k k' -> f g H. apply nsum_ext. intros i _. apply H. Qed.
(* ---- counting bits ---------------------------------------------------------------------------------------- *)
(* half of the values below 2^k have bit b set *)
Lemma count_bit : forall k b, b < k -> 2 * nsum (2 ^ k) (fun v => Nat.b2n (Nat.testbit v b)) = 2 ^ k.
Proof.
induction k as [|k IH]; intros b Hb; [lia|].
rewrite Nat.pow_succ_r', (Nat.mul_comm 2 (2 ^ k)), nsum_mul.
destruct b as [|b].
- rewrite (nsum_ext (2 ^ k) _ (fun _ => 1)); [rewrite nsum_const; lia|].
intros q _. cbn [nsum]. rewrite Nat.add_0_r, Nat.testbit_even_0, Nat.testbit_odd_0. reflexivity.
- rewrite (nsum_ext (2 ^ k) _ (fun q => Nat.b2n (Nat.testbit q b) + Nat.b2n (Nat.testbit q b))).
+ rewrite nsum_add. specialize (IH b ltac:(lia)). lia.
+ intros q _. cbn [nsum]. rewrite Nat.add_0_r, Nat.testbit_even_succ', Nat.testbit_odd_succ'. lia.
Qed.
(* a cyclic shift of the indices leaves a sum unchanged *)
Lemma nsum_shift : forall M c f, c <= M -> nsum M (fun j => f ((j + c) mod M)) = nsum M f.
Proof.
intros M c f Hc. destruct (Nat.eq_dec M 0) as [->|HM]; [reflexivity|].
replace M with ((M - c) + c) at 1 by lia. rewrite nsum_split.
rewrite (nsum_ext (M - c) _ (fun j => f (c + j))) by (intros j Hj; rewrite Nat.mod_small by lia; f_equal; lia).
rewrite (nsum_ext c _ f).
- transitivity (nsum (c + (M - c)) f); [rewrite nsum_split; lia | f_equal; lia].
- intros i Hi. f_equal. replace (M - c + i + c) with (i + 1 * M) by lia.
rewrite Nat.Div0.mod_add. apply Nat.mod_small. lia.
Qed.
Section HC.
Variable A : nat.
Hypothesis HA : 3 <= A.
Lemma SW_half : SW A = 2 * 2 ^ (A - 1).
Proof. unfold SW. replace A with (S (A - 1)) at 1 by lia. rewrite Nat.pow_succ_r'. reflexivity. Qed.
(* the decode lines of p + 3: half of the lines feed each bit *)
Lemma Q_count : forall i, i < A ->
length (filter (fun j => bitof A ((j + 3) mod SW A) i) (seq 0 (SW A))) = 2 ^ (A - 1).
Proof.
intros i Hi. pose proof (SW_ge A HA). rewrite length_filter_seq.
transitivity (nsum (SW A) (fun v => Nat.b2n (Nat.testbit v (A - 1 - i)))).
- rewrite <- (nsum_shift (SW A) 3 (fun v => Nat.b2n (Nat.testbit v (A - 1 - i)))) by lia.
apply nsum_ext. intros j _. reflexivity.
- pose proof (count_bit A (A - 1 - i) ltac:(lia)) as Hc. pose proof SW_half as E. unfold SW in *. lia.
Qed.
Lemma nsum_SS : nsum (A - 1) (fun i => S (S i)) = tri A + (A - 1).
Proof.
unfold tri. generalize (A - 1) as k. induction k as [|k IH]; cbn [nsum]; lia.
Qed.
(* ---- the units ------------------------------------------------------------------------------------------- *)
(* (8A + 4) 2^A + (A^2 + 39A + 4)/2 units *)
Theorem host_units_count : 2 * length (host_units A) = (16 * A + 8) * SW A + A * A + 39 * A + 4.
Proof.
change (host_units A) with (fus (hblocks A) (nH A)).
rewrite (units_bsum (hblocks A) (nH A) (hout A) (host_wf' A HA) (hout_valid A HA)), (bsum_host A HA).
rewrite (nsum_ext (A - 1) _ (fun i => S (S i))) by (intros i _; rewrite nsum_const; lia).
rewrite nsum_SS. pose proof (tri_eq A HA).
cbn [nsum nth hpre hpost bcount bsize blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB blk_AC blk_W blk_RX blk_RY blk_KP
blk_X blk_Y blk_PR blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0 blk_H blk_R blk_LEQ blk_TA blk_TB blk_NP blk_HAB
blk_WR blk_NM].
rewrite !nsum_const. nia.
Qed.
(* the datapath and the memory: the blocks whose number of units grows with 2^A, with the operand fetch and the read
multiplexer, hold (8A + 4) 2^A + 5A of them *)
Definition memblocks : list nat := [0; 2; 3; 4; 6; 7; 8; 10; 11; 12; 13; 14; 15; tb A + 13; tb A + 14].
Theorem host_memory_count :
fold_right Nat.add 0 (map (fun b => bcount (nth b (hblocks A) blk0) * bsize (nth b (hblocks A) blk0)) memblocks)
= (8 * A + 4) * SW A + 5 * A.
Proof.
unfold memblocks. cbn [map fold_right]. rewrite !nth_hb_pre by lia. rewrite !nth_hb_post by lia.
cbn [nth hpre hpost bcount bsize blk_P blk_FA blk_F blk_PA blk_PB blk_W blk_RX blk_RY blk_KP blk_X blk_Y blk_WR blk_NM].
nia.
Qed.
(* ---- the edges --------------------------------------------------------------------------------------------- *)
Definition pe (b : nat) : nat :=
nsum (bcount (nth b (hpre A) blk0)) (fun j => nsum (bsize (nth b (hpre A) blk0))
(fun r => length (sin (nth r (bshape (nth b (hpre A) blk0) j) su0)))).
Definition qe (i : nat) : nat :=
nsum (bcount (nth i (hpost A) blk0)) (fun j => nsum (bsize (nth i (hpost A) blk0))
(fun r => length (sin (nth r (bshape (nth i (hpost A) blk0) j) su0)))).
Definition te (i : nat) : nat := nsum (S (S i)) (fun r => length (sin (nth r (bshape (blk_T A (S i)) 0) su0))).
Ltac ecnt := unfold pe, qe;
cbn [nth hpre hpost bcount bsize bshape blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB blk_AC blk_W blk_RX blk_RY blk_KP
blk_X blk_Y blk_PR blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0 blk_H blk_R blk_LEQ blk_TA blk_TB blk_NP blk_HAB
blk_WR blk_NM nsum sin sAND sOR lits map length app];
repeat setoid_rewrite length_map; repeat setoid_rewrite length_seq; rewrite ?nsum_const; try lia.
Lemma pe_vals : pe 0 = SW A * A /\ pe 1 = A * 2 /\ pe 2 = A * SW A * 2 /\ pe 3 = A * SW A * 2 /\ pe 4 = A * SW A * 2
/\ pe 6 = 3 * A * SW A /\ pe 7 = SW A * A /\ pe 8 = SW A * A /\ pe 9 = A /\ pe 10 = SW A * 2 /\ pe 11 = A * SW A * 2
/\ pe 12 = A * SW A * 2 /\ pe 13 = SW A * A * 2 /\ pe 14 = A * SW A /\ pe 15 = A * SW A /\ pe 16 = (A - 1) * 2.
Proof. repeat split; ecnt. Qed.
Lemma pe5 : pe 5 = A * 2 ^ (A - 1).
Proof.
unfold pe. cbn [nth hpre bcount bsize bshape blk_Q nsum sin sOR].
rewrite (nsum_ext A _ (fun _ => 2 ^ (A - 1))); [rewrite nsum_const; lia|].
intros i Hi. cbn [nth Nat.add]. rewrite !length_map. apply Q_count. lia.
Qed.
Lemma qe_vals : qe 1 = A * 2 /\ qe 2 = A * 2 /\ qe 3 = A * 2 /\ qe 4 = A /\ qe 5 = 6 /\ qe 6 = (A - 1) * 9
/\ qe 7 = (A - 1) * 3 /\ qe 8 = 4 /\ qe 9 = A * 3 /\ qe 10 = A * 3 /\ qe 11 = A * 3 /\ qe 12 = 9
/\ qe 13 = SW A * A * 2 /\ qe 14 = SW A * A * 2.
Proof. repeat split; ecnt. Qed.
Lemma qe0 : qe 0 = tri A + (A - 1).
Proof.
unfold qe. cbn [nth hpost bcount bsize bshape blk_C nsum sin sOR]. rewrite <- nsum_SS.
apply nsum_ext. intros m _. cbn [nth map length]. rewrite !length_map, length_seq. lia.
Qed.
Lemma sum_rev : forall k, 2 * nsum k (fun j => k + 1 - j) = k * k + 3 * k.
Proof.
intro k. assert (H1 : nsum k (fun j => k + 1 - j) + nsum k (fun j => j) = k * (k + 1)).
{ rewrite <- nsum_add, <- nsum_const. apply nsum_ext. intros j Hj. lia. }
assert (H2 : 2 * nsum k (fun j => j) = k * (k - 1)) by (clear; induction k as [|k IH]; cbn [nsum]; nia).
nia.
Qed.
Lemma te_val : forall i, 2 * te i = S i * S i + 5 * S i.
Proof.
intro i. unfold te. replace (S (S i)) with (1 + S i) by lia. rewrite nsum_split.
assert (H0 : nsum 1 (fun r => length (sin (nth r (bshape (blk_T A (S i)) 0) su0))) = S i)
by (cbn [nsum nth bshape blk_T sin sAND]; rewrite !length_map, length_seq; reflexivity).
rewrite H0. rewrite (nsum_ext (S i) _ (fun j => S i + 1 - j)).
- pose proof (sum_rev (S i)). lia.
- intros j Hj. cbn [Nat.add nth bshape blk_T]. rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia).
rewrite seq_nth by lia. cbn [sin sAND]. rewrite length_map, length_app, length_map, length_seq. cbn [length]. lia.
Qed.
Lemma sum_te : forall K, 6 * nsum K (fun i => S i * S i + 5 * S i) = K * (K + 1) * (2 * K + 1) + 15 * (K * (K + 1)).
Proof. induction K as [|K IH]; cbn [nsum]; nia. Qed.
(* (49A + 4) 2^(A-1) + (A^3 + 3A^2 + 2A)/6 + A^2 + 32A + 4 edges *)
Theorem host_edges : 6 * nsum (length (host_units A)) (fun k => length (tin (nth k (host_units A) tu0)))
= 3 * (49 * A + 4) * SW A + A * A * A + 9 * (A * A) + 194 * A + 24.
Proof.
change (host_units A) with (fus (hblocks A) (nH A)).
rewrite (edges_bsum (hblocks A) (nH A) (hout A) (host_wf' A HA) (hout_valid A HA)), (bsum_host A HA).
rewrite (nsum_ext 17 _ pe)
by (intros b Hb; unfold pe; apply nsum_ext; intros j _; apply nsum_ext; intros r _; cbn [usu]; unfold sunit;
rewrite nth_hb_pre by exact Hb; reflexivity).
rewrite (nsum_ext (A - 1) _ te)
by (intros i Hi; unfold te; apply nsum_ext; intros r _; cbn [usu]; unfold sunit;
replace (17 + i) with (16 + S i) by lia; rewrite nth_hb_T by lia; reflexivity).
rewrite (nsum_ext 15 _ qe)
by (intros i Hi; unfold qe; apply nsum_ext; intros j _; apply nsum_ext; intros r _; cbn [usu]; unfold sunit;
rewrite nth_hb_post by lia; reflexivity).
cbn [nsum]. rewrite pe5, qe0.
destruct pe_vals as (P0 & P1 & P2 & P3 & P4 & P6 & P7 & P8 & P9 & P10 & P11 & P12 & P13 & P14 & P15 & P16).
destruct qe_vals as (Q1 & Q2 & Q3 & Q4 & Q5 & Q6 & Q7 & Q8 & Q9 & Q10 & Q11 & Q12 & Q13 & Q14).
rewrite P0, P1, P2, P3, P4, P6, P7, P8, P9, P10, P11, P12, P13, P14, P15, P16.
rewrite Q1, Q2, Q3, Q4, Q5, Q6, Q7, Q8, Q9, Q10, Q11, Q12, Q13, Q14.
assert (HT : 2 * nsum (A - 1) te = nsum (A - 1) (fun i => S i * S i + 5 * S i)).
{ generalize (A - 1) as K. induction K as [|K IH]; cbn [nsum]; [reflexivity|]. rewrite <- IH, <- te_val. lia. }
pose proof (sum_te (A - 1)) as HS6. pose proof (tri_eq A HA) as Htri. pose proof SW_half as Hh.
assert (Ea : exists a, A = S (S (S a))) by (exists (A - 3); lia). destruct Ea as [a Ea].
rewrite Ea in *. cbn [Nat.sub] in *. rewrite ?Nat.sub_0_r in *. nia.
Qed.
(* ---- the biases ---------------------------------------------------------------------------------------- *)
Lemma sb_and : forall ls, (- Z.of_nat (length ls) <= sb (sAND ls) <= 0)%Z.
Proof.
intro ls. cbn [sb sAND]. pose proof (npos_nneg ls). unfold npos in *. pose proof (filter_length_le _ snd ls). lia.
Qed.
Lemma sb_or : forall ls, sb (sOR ls) = (Z.of_nat (nneg ls) - 1)%Z.
Proof. reflexivity. Qed.
Lemma nneg_pos : forall (X : Type) (f : X -> sref) (l : list X), nneg (map (fun x => (f x, true)) l) = 0.
Proof. intros X f l. unfold nneg. induction l as [|x t IH]; [reflexivity|]. cbn [map filter snd negb]. exact IH. Qed.
Lemma lw_pm : forall (ls : list lit) p z, In (p, z) (map lw ls) -> z = 1%Z \/ z = (-1)%Z.
Proof.
intros ls p z H. apply in_map_iff in H as ([x pol] & E & _). unfold lw in E. cbn [fst snd] in E.
injection E as _ <-. destruct pol; [left | right]; reflexivity.
Qed.
(* every unit is a threshold unit with weights -1 or 1 and a bias in [-A, 1] *)
Definition gate_ok (u : su) : Prop :=
(forall p z, In (p, z) (sin u) -> z = 1%Z \/ z = (-1)%Z) /\ (- Z.of_nat A <= sb u <= 1)%Z.
Lemma and_ok : forall ls, length ls <= A -> gate_ok (sAND ls).
Proof.
intros ls H. split; [intros p z Hin; exact (lw_pm ls p z Hin)|]. pose proof (sb_and ls). lia.
Qed.
Lemma or_ok : forall ls, nneg ls <= 2 -> gate_ok (sOR ls).
Proof. intros ls H. split; [intros p z Hin; exact (lw_pm ls p z Hin)|]. rewrite sb_or. lia. Qed.
Theorem host_gate_ok : forall b j r, valid (hblocks A) (nH A) (SRef b j r) -> gate_ok (sunit (hblocks A) b j r).
Proof.
intros b j r (Hb & Hj & Hr). rewrite length_hblocks in Hb by lia. unfold sunit.
destruct (Nat.lt_ge_cases b 17) as [Hp|Hp].
{ rewrite nth_hb_pre in Hj, Hr |- * by exact Hp.
assert (Hc : b = 0 \/ b = 1 \/ b = 2 \/ b = 3 \/ b = 4 \/ b = 5 \/ b = 6 \/ b = 7 \/ b = 8 \/ b = 9
\/ b = 10 \/ b = 11 \/ b = 12 \/ b = 13 \/ b = 14 \/ b = 15 \/ b = 16) by lia.
destruct Hc as [->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->| ->]]]]]]]]]]]]]]]];
cbn [nth hpre bcount bsize bshape blk_P blk_HP blk_FA blk_Q blk_F blk_PA blk_PB blk_AC blk_W
blk_RX blk_RY blk_KP blk_X blk_Y blk_PR] in Hj, Hr |- *;
(destruct r as [|r]; [|lia]); cbn [nth];
first [ apply and_ok; unfold lits; rewrite ?length_map, ?length_seq; cbn [length]; lia
| apply or_ok; rewrite ?nneg_pos; unfold nneg; cbn [filter snd negb length]; lia ]. }
destruct (Nat.lt_ge_cases b (tb A)) as [HT|HT].
{ unfold tb in HT. replace b with (16 + (b - 16)) in Hj, Hr |- * by lia.
rewrite nth_hb_T in Hj, Hr |- * by lia. cbn [bcount bsize bshape blk_T] in Hj, Hr |- *.
destruct r as [|r]; cbn [nth].
- apply and_ok. rewrite length_map, length_seq. lia.
- rewrite nth_map_d with (d' := 0) by (rewrite length_seq; lia). rewrite seq_nth by lia.
apply and_ok. rewrite length_app, length_map, length_seq. cbn [length]. lia. }
replace b with (tb A + (b - tb A)) in Hj, Hr |- * by lia.
rewrite nth_hb_post in Hj, Hr |- * by lia.
assert (Hi : b - tb A < 15) by (unfold tb in *; lia).
remember (b - tb A) as i eqn:Ei. clear Ei Hb Hp HT.
assert (Hc : i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4 \/ i = 5 \/ i = 6 \/ i = 7 \/ i = 8 \/ i = 9
\/ i = 10 \/ i = 11 \/ i = 12 \/ i = 13 \/ i = 14) by lia.
destruct Hc as [->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->|[->| ->]]]]]]]]]]]]]];
cbn [nth hpost bcount bsize bshape blk_C blk_AX blk_NX blk_XN blk_EQ blk_R0 blk_H blk_R blk_LEQ
blk_TA blk_TB blk_NP blk_HAB blk_WR blk_NM] in Hj, Hr |- *.
- destruct r as [|r]; [|lia]. cbn [nth]. apply or_ok.
assert (E : forall x (l : list lit), nneg ((x, true) :: l) = nneg l) by reflexivity.
rewrite E, nneg_pos. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. cbn [length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. cbn [length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply or_ok. unfold nneg. cbn [filter snd negb length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. rewrite length_map, length_seq. lia.
- assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia. destruct Hr3 as [->|[->| ->]]; cbn [nth];
first [apply and_ok; cbn [length]; lia | apply or_ok; unfold nneg; cbn [filter snd negb length]; lia].
- assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia.
destruct Hr3 as [->|[->| ->]]; cbn [nth map]; split; cbn [sin sb];
try (intros p z Hin; repeat (destruct Hin as [Hin|Hin]; [injection Hin as _ <-; auto|]); destruct Hin); lia.
- destruct r as [|r]; [|lia]. cbn [nth]. split; cbn [sin sb]; [|lia].
intros p z Hin. repeat (destruct Hin as [Hin|Hin]; [injection Hin as _ <-; auto|]). destruct Hin.
- destruct r as [|r]; [|lia]. cbn [nth]. split; cbn [sin sb]; [|lia].
intros p z Hin. repeat (destruct Hin as [Hin|Hin]; [injection Hin as _ <-; auto|]). destruct Hin.
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. cbn [length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. cbn [length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply or_ok. unfold nneg. cbn [filter snd negb length]. lia.
- assert (Hr3 : r = 0 \/ r = 1 \/ r = 2) by lia. destruct Hr3 as [->|[->| ->]]; cbn [nth];
first [apply and_ok; cbn [length]; lia | apply or_ok; unfold nneg; cbn [filter snd negb length]; lia].
- destruct r as [|r]; [|lia]. cbn [nth]. apply and_ok. cbn [length]. lia.
- destruct r as [|r]; [|lia]. cbn [nth]. apply or_ok. unfold nneg. cbn [filter snd negb length]. lia.
Qed.
(* the units of the flat netlist, with their weights and biases *)
Theorem host_weights_biases : forall k, k < length (host_units A) ->
(forall i z, In (i, z) (tin (nth k (host_units A) tu0)) -> z = 1%Z \/ z = (-1)%Z)
/\ (- Z.of_nat A <= Net.tb (nth k (host_units A) tu0) <= 1)%Z.
Proof.
intros k Hk. change (host_units A) with (fus (hblocks A) (nH A)) in *.
rewrite (fus_len (hblocks A) (nH A) (host_wf' A HA)) in Hk.
destruct (loc (hblocks A) (nH A) (host_wf' A HA) k Hk) as (b & j & r & Hv & ->).
rewrite (fus_nth (hblocks A) (nH A) (host_wf' A HA) b j r Hv). unfold flat_unit. cbn [tin Net.tb].
destruct (host_gate_ok b j r Hv) as [Hw Hs]. split; [|exact Hs].
intros i z Hin. apply in_map_iff in Hin as ([p z'] & E & Hin). cbn [fst snd] in E. injection E as _ <-.
exact (Hw p z' Hin).
Qed.
(* ---- each unit occurs once in Lev(H_A) ---------------------------------------------------------------------- *)
Lemma hout_inj : forall i i', i < nH A -> i' < nH A -> hout A i = hout A i' -> i = i'.
Proof.
intros i i' Hi Hi' E. destruct (Nat.eq_dec i i') as [|Hne]; [assumption|]. exfalso. unfold hout in E.
destruct (Nat.ltb_spec i A), (Nat.ltb_spec i' A); try destruct (Nat.eqb_spec i A); try destruct (Nat.eqb_spec i' A);
try lia; injection E; intros; lia.
Qed.
Lemma depth13_out : forall x, valid (hblocks A) (nH A) x -> cdh A x = 13 -> exists i, i < nH A /\ hout A i = x.
Proof.
intros x Hx H13. destruct (out_dec A HA x) as [Ho|Hno]; [exact Ho|]. exfalso.
destruct (host_reader A HA x Hx Hno) as (b & j & r & z & Hv & Hin & _).
destruct (host_unit_ok A HA b j r Hv) as [Hall _]. pose proof (proj1 (Hall x z Hin)).
pose proof (cdh_le13 A HA (SRef b j r)). lia.
Qed.
Definition hsrc : list src := concat (map snd (lsrc (nH A) (host_units A) (host_next A))).
Lemma hsrc_range : forall s, In (Un s) hsrc -> nH A <= s < nH A + length (host_units A).
Proof.
intros s Hs. unfold hsrc, lsrc in Hs. rewrite map_app, concat_app in Hs. apply in_app_or in Hs as [Hs|Hs].
- rewrite map_map in Hs. apply in_concat in Hs as (cs & Hcs & Hin). apply in_map_iff in Hcs as (l & <- & _).
cbn [snd] in Hin. destruct (srcs_spec _ _ _ l (Un s) Hin) as [HU _]. destruct (HU s eq_refl) as (k & Hk & -> & _).
lia.
- cbn [map concat snd] in Hs. rewrite app_nil_r in Hs.
destruct (srcd_spec (nH A) (host_units A) (host_next A)) with (c := Un s) as [HU _]; try exact Hs.
+ apply Forall_forall. intros a Ha. unfold host_next in Ha. apply in_map_iff in Ha as (i & <- & Hi).
apply in_seq in Hi. unfold NS. pose proof (idx_lt_total _ _ _ (hout_valid A HA i ltac:(lia))) as H.
change (host_units A) with (fus (hblocks A) (nH A)). rewrite (fus_len _ _ (host_wf' A HA)). exact H.
+ exact (host_next_len A).
+ rewrite (host_dmax A HA). lia.
+ destruct (HU s eq_refl) as (k & Hk & -> & _). lia.
Qed.
Lemma host_once : forall k, k < length (host_units A) -> length (filter (isun (nH A + k)) hsrc) = 1.
Proof.
intros k Hk. unfold hsrc.
assert (Hwfn : wfn (nH A) (host_units A)) by exact (fwfn (hblocks A) (nH A) (host_wf' A HA)).
rewrite (lev_units (nH A) (host_units A) (host_next A) Hwfn (host_next_len A)) by (unfold NS; lia).
change (host_units A) with (fus (hblocks A) (nH A)) in Hk. rewrite (fus_len _ _ (host_wf' A HA)) in Hk.
destruct (loc (hblocks A) (nH A) (host_wf' A HA) k Hk) as (b & j & r & Hv & Ek).
replace (nH A + k) with (idx (nH A) (hblocks A) (SRef b j r)) by (rewrite idx_ref, Ek; reflexivity).
rewrite (host_need A HA b j r Hv), (host_dep A HA _ Hv), (host_dmax A HA).
destruct (Nat.ltb_spec (cdh A (SRef b j r)) 13) as [Hl|Hg]; [reflexivity|].
pose proof (cdh_le13 A HA (SRef b j r)).
destruct (depth13_out (SRef b j r) Hv ltac:(lia)) as (i0 & Hi0 & E0).
unfold host_next. rewrite length_filter_map, <- E0.
rewrite (filter_ext_in _ (fun i => true && Nat.eqb i i0)).
- rewrite filter_eqb_seq by exact Hi0. reflexivity.
- intros i Hi. apply in_seq in Hi. cbn [andb]. destruct (Nat.eqb_spec i i0) as [->|E]; [apply Nat.eqb_refl|].
apply Nat.eqb_neq. intro Ex. apply E. apply hout_inj; [lia | exact Hi0|].
exact (idx_inj (hblocks A) (nH A) _ _ (hout_valid A HA i ltac:(lia)) (hout_valid A HA i0 Hi0) Ex).
Qed.
(* the rows of Lev(H_A) that are not units of H_A are identity units, and the entries are the edges of H_A and one for
each identity unit *)
Theorem host_lev_rows_split :
length (concat (lev (nH A) (host_units A) (host_next A)))
= length (host_units A) + length (filter (fun c => negb (isUn c)) hsrc)
/\ fold_right Nat.add 0 (map (fun row => length (tin row)) (concat (lev (nH A) (host_units A) (host_next A))))
= nsum (length (host_units A)) (fun k => length (tin (nth k (host_units A) tu0)))
+ length (filter (fun c => negb (isUn c)) hsrc).
Proof.
split.
- rewrite lev_rowcount. fold hsrc.
assert (Hs : forall L : list src, length L = length (filter isUn L) + length (filter (fun c => negb (isUn c)) L))
by (induction L as [|c t IH]; [reflexivity|]; cbn [filter length]; destruct (isUn c); cbn [negb length]; lia).
rewrite Hs, (count_Un hsrc (nH A) (length (host_units A)) hsrc_range).
rewrite (nsum_ext _ _ (fun _ => 1)) by (intros k Hk; apply host_once; exact Hk). rewrite nsum_const. lia.
- rewrite lev_rowlens. fold hsrc. rewrite (sum_rowlen hsrc (host_units A) (nH A) (length (host_units A)) hsrc_range).
rewrite (nsum_ext _ (fun k => length (filter (isun (nH A + k)) hsrc) * length (tin (nth k (host_units A) tu0)))
(fun k => length (tin (nth k (host_units A) tu0))))
by (intros k Hk; rewrite host_once by exact Hk; lia).
lia.
Qed.
(* Lev(H_A) adds (11A + 6) 2^A + 35A + 25 identity units to the units of H_A *)
Theorem host_lev_identity : length (filter (fun c => negb (isUn c)) hsrc) = (11 * A + 6) * SW A + 35 * A + 25.
Proof.
destruct host_lev_rows_split as [H _]. rewrite length_concat in H. unfold list_sum in H.
pose proof (host_lev_rows A HA) as R. pose proof host_units_count as U. lia.
Qed.
End HC.
(* the least and the greatest bias are attained, by the conjunction [c = 2^A - 1] and by the disjunction of the
negated low bits of the operands *)
Lemma host_bias_attained : forall A, 3 <= A ->
(exists k, k < length (host_units A) /\ Net.tb (nth k (host_units A) tu0) = (- Z.of_nat A)%Z)
/\ (exists k, k < length (host_units A) /\ Net.tb (nth k (host_units A) tu0) = 1%Z).
Proof.
intros A HA. pose proof (SW_ge A HA). change (host_units A) with (fus (hblocks A) (nH A)).
assert (Hv1 : valid (hblocks A) (nH A) (SRef 9 0 0)).
{ split; [rewrite length_hblocks by lia; unfold tb; lia|]. rewrite nth_hb_pre by lia. cbn. lia. }
assert (Hv2 : valid (hblocks A) (nH A) (SRef (tb A + 5) 0 1)).
{ split; [rewrite length_hblocks by lia; lia|]. rewrite nth_hb_post by lia. cbn. lia. }
split.
- exists (boff (hblocks A) 9 + sz (hblocks A) 9 * 0 + 0). split.
+ rewrite (fus_len _ _ (host_wf' A HA)). exact (unit_lt _ _ 9 0 0 Hv1).
+ rewrite (fus_nth _ _ (host_wf' A HA) 9 0 0 Hv1). unfold flat_unit, sunit. cbn [Net.tb].
rewrite nth_hb_pre by lia. cbn [nth hpre bshape blk_AC sb sAND]. unfold npos.
assert (G : forall l : list nat, length (filter snd (map (fun t => (opb A 2 t, true)) l)) = length l)
by (induction l as [|a t IH]; [reflexivity|]; cbn [map filter snd length]; rewrite IH; reflexivity).
rewrite G, length_seq. reflexivity.
- exists (boff (hblocks A) (tb A + 5) + sz (hblocks A) (tb A + 5) * 0 + 1). split.
+ rewrite (fus_len _ _ (host_wf' A HA)). exact (unit_lt _ _ _ 0 1 Hv2).
+ rewrite (fus_nth _ _ (host_wf' A HA) _ 0 1 Hv2). unfold flat_unit, sunit. cbn [Net.tb].
rewrite nth_hb_post by lia. reflexivity.
Qed.
(* ---- the host with eight-bit words, in binary numbers ------------------------------------------------------ *)
Lemma host_units_8 : N.of_nat (length (host_units 8)) = 17598%N.
Proof. pose proof (host_units_count 8 ltac:(lia)) as H. assert (SW 8 = 256) by reflexivity. lia. Qed.
Lemma host_edges_8 : N.of_nat (nsum (length (host_units 8)) (fun k => length (tin (nth k (host_units 8) tu0)))) = 51132%N.
Proof. pose proof (host_edges 8 ltac:(lia)) as H. assert (SW 8 = 256) by reflexivity. lia. Qed.
Lemma host_memory_8 : N.of_nat (fold_right Nat.add 0 (map (fun b => bcount (nth b (hblocks 8) blk0)
* bsize (nth b (hblocks 8) blk0)) (memblocks 8)))
= 17448%N.
Proof. pose proof (host_memory_count 8 ltac:(lia)) as H. assert (SW 8 = 256) by reflexivity. lia. Qed.
(* Lev(H_8): 24,369 identity units and 75,501 nonzero entries *)
Lemma host_lev_identity_8 : N.of_nat (length (filter (fun c => negb (isUn c)) (hsrc 8))) = 24369%N.
Proof. pose proof (host_lev_identity 8 ltac:(lia)) as H. assert (SW 8 = 256) by reflexivity. lia. Qed.
Lemma host_lev_nonzero_8 :
N.of_nat (fold_right Nat.add 0 (map (fun row => length (tin row)) (concat (lev (nH 8) (host_units 8) (host_next 8)))))
= 75501%N.
Proof.
destruct (host_lev_rows_split 8 ltac:(lia)) as [_ H]. rewrite H.
pose proof host_edges_8. pose proof host_lev_identity_8. lia.
Qed.