1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32.bend as U
5	import ../../lib/array.bend as AR
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/doubly_linked_list.bend as S
8	import ../../lib/u32div.bend as UD
9	import ./state.bend as ST
10	import ./rel.bend as RL
11	import ./vals.bend as VA
12	import ../../lib/links.bend as LK
13	import ../../lib/words32.bend as W32
14	
15	# The doubled blocks: the old block is the lower half, so every id keeps its
16	# links, value and generation.
17	
18	
19	def nth0_app(+xs: List<&2, U32>, +ys: List<&2, U32>, +i: Nat, +h: {Nat.is_lt(i, SC.length(U32, xs)) == True{} : Bool}) -> {W32.nth0(SC.append(U32, xs, ys), i) == W32.nth0(xs, i) : U32}:
20	  match xs i:
21	    case Nil{} _:
22	      Empty.absurd({W32.nth0(ys, i) == 0 : U32}, N.lt_zero_absurd(i, h))
23	    case Con{x, t} 0n:
24	      {==}
25	    case Con{x, +t} 1n+p:
26	      nth0_app(t, ys, p, h)
27	
28	def val_app(-T: Data, +vl: List<&2, Maybe<&2, T>>, +ys: List<&2, Maybe<&2, T>>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}) -> {S.val_of(T, SC.append(Maybe<&2, T>, vl, ys), i) == S.val_of(T, vl, i) : Maybe<&2, T>}:
29	  match vl i:
30	    case Nil{} _:
31	      Empty.absurd({S.val_of(T, ys, i) == None{} : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
32	    case Con{m, t} 0n:
33	      {==}
34	    case Con{m, +t} 1n+p:
35	      val_app(T, t, ys, p, h)
36	
37	
38	# the links of a live list, after the blocks are extended
39	def seg_ext(~T: Data, +pl: List<&2, U32>, +pz: List<&2, U32>, +nl: List<&2, U32>, +nz: List<&2, U32>, +sl: List<&2, Nat>, +p: U32, +q: U32, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +h: {ST.slok(~T, sl, fr, vl) == True{} : Bool}, +hp: {Nat.is_le(fr, SC.length(U32, pl)) == True{} : Bool}, +hn: {Nat.is_le(fr, SC.length(U32, nl)) == True{} : Bool}) -> {ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), sl, p, q) == ST.seg(pl, nl, sl, p, q) : Bool}:
40	  match sl:
41	    case Nil{}:
42	      {==}
43	    case Con{+x, +t}:
44	      +hx = L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h))
45	      +ht = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
46	      +e0 = nth0_app(pl, pz, x, N.lt_le_trans(x, fr, SC.length(U32, pl), hx, hp))
47	      +e1 = nth0_app(nl, nz, x, N.lt_le_trans(x, fr, SC.length(U32, nl), hx, hn))
48	      +ih = seg_ext(~T, pl, pz, nl, nz, t, LK.lnk(x), q, fr, vl, ht, hp, hn)
49	      +r1 = Equal.cong(U32, Bool, z => Bool.and(U32.is_eq(z, p), Bool.and(U32.is_eq(W32.nth0(SC.append(U32, nl, nz), x), LK.fst_or(t, q)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q))), W32.nth0(SC.append(U32, pl, pz), x), W32.nth0(pl, x), e0)
50	      +r2 = Equal.cong(U32, Bool, z => Bool.and(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(z, LK.fst_or(t, q)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q))), W32.nth0(SC.append(U32, nl, nz), x), W32.nth0(nl, x), e1)
51	      +r3 = Equal.cong(Bool, Bool, z => Bool.and(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(nl, x), LK.fst_or(t, q)), z)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q), ST.seg(pl, nl, t, LK.lnk(x), q), ih)
52	      Equal.trans(Bool, ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), Con{x, t}, p, q), Bool.and(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(SC.append(U32, nl, nz), x), LK.fst_or(t, q)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q))), ST.seg(pl, nl, Con{x, t}, p, q), r1, Equal.trans(Bool, Bool.and(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(SC.append(U32, nl, nz), x), LK.fst_or(t, q)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q))), Bool.and(U32.is_eq(W32.nth0(pl, x), p), Bool.and(U32.is_eq(W32.nth0(nl, x), LK.fst_or(t, q)), ST.seg(SC.append(U32, pl, pz), SC.append(U32, nl, nz), t, LK.lnk(x), q))), ST.seg(pl, nl, Con{x, t}, p, q), r2, r3))
53	
54	# live ids stay live when vacant slots are appended
55	def slok_ext(~T: Data, +xs: List<&2, Nat>, +fr: Nat, +vl: List<&2, Maybe<&2, T>>, +ys: List<&2, Maybe<&2, T>>, +hfr: {Nat.is_le(fr, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}, +h: {ST.slok(~T, xs, fr, vl) == True{} : Bool}) -> {ST.slok(~T, xs, fr, SC.append(Maybe<&2, T>, vl, ys)) == True{} : Bool}:
56	  match xs:
57	    case Nil{}:
58	      {==}
59	    case Con{+x, +t}:
60	      +h0 = L.and_left(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
61	      +h1 = L.and_right(Bool.and(Nat.is_lt(x, fr), ST.live(T, vl, x)), ST.slok(~T, t, fr, vl), h)
62	      +hx = L.and_left(Nat.is_lt(x, fr), ST.live(T, vl, x), h0)
63	      +e = Equal.cong(Maybe<&2, T>, Bool, m => ST.some_b(T, m), S.val_of(T, SC.append(Maybe<&2, T>, vl, ys), x), S.val_of(T, vl, x), val_app(T, vl, ys, x, N.lt_le_trans(x, fr, SC.length(Maybe<&2, T>, vl), hx, hfr)))
64	      +hl = RL.by_eq(ST.live(T, SC.append(Maybe<&2, T>, vl, ys), x), ST.live(T, vl, x), e, L.and_right(Nat.is_lt(x, fr), ST.live(T, vl, x), h0))
65	      L.and_intro(Bool.and(Nat.is_lt(x, fr), ST.live(T, SC.append(Maybe<&2, T>, vl, ys), x)), ST.slok(~T, t, fr, SC.append(Maybe<&2, T>, vl, ys)), L.and_intro(Nat.is_lt(x, fr), ST.live(T, SC.append(Maybe<&2, T>, vl, ys), x), hx, hl), slok_ext(~T, t, fr, vl, ys, hfr, h1))
66	
67	# 2^a < 2^b: a < b
68	def p2_c(+a: Nat, +b: Nat, +h: {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(a, b) == c : Bool}) -> {c == True{} : Bool}:
69	  match c:
70	    case True{}:
71	      {==}
72	    case False{}:
73	      +hba = N.pow2_mono(b, a, N.not_lt_le(a, b, hc))
74	      Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_lt(SC.pow2(a), SC.pow2(a)), False{}, Equal.sym(Bool, Nat.is_lt(SC.pow2(a), SC.pow2(a)), True{}, N.lt_le_trans(SC.pow2(a), SC.pow2(b), SC.pow2(a), h, hba)), N.lt_irrefl(SC.pow2(a)))))
75	
76	def p2_inv(+a: Nat, +b: Nat, +h: {Nat.is_lt(SC.pow2(a), SC.pow2(b)) == True{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}:
77	  p2_c(a, b, h, Nat.is_lt(a, b), {==})
78	
79	# the doubled capacity
80	def shl_cap(+cap: U32, +d: Nat, +hd: {Nat.is_lt(d, 29n) == True{} : Bool}, +hcap: {Nat.is_eq(UD.v(cap), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_eq(UD.v(U32.shl(cap)), SC.pow2(1n+d)) == True{} : Bool}:
81	  +e = N.eq_from_is_eq(UD.v(cap), SC.pow2(d), hcap)
82	  +hb = L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(2n+d)) == True{} : Bool}, SC.pow2(d), UD.v(cap), Equal.sym(Nat, UD.v(cap), SC.pow2(d), e), N.pow2_lt_succ(1n+d))
83	  +hk = N.lt_le(2n+d, 32n, N.lt_trans(2n+d, 31n, 32n, hd, {==}))
84	  +ev = U.shl_value(cap, 2n+d, hk, hb)
85	  +ev2 = Equal.trans(Nat, UD.v(U32.shl(cap)), Nat.double(UD.v(cap)), SC.pow2(1n+d), ev, Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(cap), SC.pow2(d), e))
86	  L.subst(Nat, z => {Nat.is_eq(z, SC.pow2(1n+d)) == True{} : Bool}, SC.pow2(1n+d), UD.v(U32.shl(cap)), Equal.sym(Nat, UD.v(U32.shl(cap)), SC.pow2(1n+d), ev2), N.is_eq_refl(SC.pow2(1n+d)))
87	
88	def gz_ext(+gT: AR.Tree<U32>, +d: Nat, +pg: {AR.perfect(U32, d, gT) == True{} : Bool}, +fr: Nat, +e: {SC.pow2(d) == fr : Nat}) -> {ST.gz(AR.slots(U32, AR.TNode{gT, AR.trep(U32, d, 0)}), fr) == True{} : Bool}:
89	  +es = AR.trep_slots(U32, d, 0)
90	  +h0 = L.subst(Nat, z => {ST.gz(SC.append(U32, AR.slots(U32, gT), SC.replicate(U32, SC.pow2(d), 0)), z) == True{} : Bool}, SC.length(U32, AR.slots(U32, gT)), fr, Equal.trans(Nat, SC.length(U32, AR.slots(U32, gT)), SC.pow2(d), fr, AR.slots_length(U32, d, gT, pg), e), VA.gz_grow(AR.slots(U32, gT), SC.pow2(d)))
91	  L.subst(List<&2, U32>, z => {ST.gz(SC.append(U32, AR.slots(U32, gT), z), fr) == True{} : Bool}, SC.replicate(U32, SC.pow2(d), 0), AR.slots(U32, AR.trep(U32, d, 0)), Equal.sym(List<&2, U32>, AR.slots(U32, AR.trep(U32, d, 0)), SC.replicate(U32, SC.pow2(d), 0), es), h0)
92	
93	def lvin_ext(~T: Data, +vT: AR.Tree<Maybe<&2, T>>, +d: Nat, +sl: List<&2, Nat>, +h: {ST.lvin(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl) == True{} : Bool}) -> {ST.lvin(~T, AR.slots(Maybe<&2, T>, AR.TNode{vT, AR.trep(Maybe<&2, T>, d, None{})}), 0n, sl) == True{} : Bool}:
94	  L.subst(List<&2, Maybe<&2, T>>, z => {ST.lvin(~T, SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, vT), z), 0n, sl) == True{} : Bool}, SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})), VA.lvin_grow(~T, AR.slots(Maybe<&2, T>, vT), 0n, sl, SC.pow2(d), h))