1	import Base
2	import ./logic.bend as L
3	import ./nat.bend as N
4	import ../../spec/lib/common.bend as SC
5	import ./lemmas/proofs/nat_algebra.bend as NA
6	
7	# Shared arithmetic and list facts for the FLAT SPLIT-POINT LAYOUT that the
8	# array-backed trees of this project use (src/fenwick_tree.bend and
9	# flat indexed structures):
10	#
11	#   * the value of index t lives at cell 2^d + t;
12	#   * the block [o, o + 2^p) of value indices (p >= 1) keeps its own cell at
13	#     the block's split point o + 2^(p-1);
14	#   * the cells a block can occupy are therefore exactly o+1 .. o+2^p-1, so
15	#     two sibling blocks never share one and a walk over one block leaves
16	#     every cell of the other untouched. That frame argument is plain
17	#     interval arithmetic, which is why this layout is used rather than the
18	#     2k/2k+1 one, where the cells of two sibling subtrees interleave.
19	#
20	# `hof(p)` is the half size a walk carries at remaining depth p (2^(p-1), and
21	# 0 at a leaf, where it is unused): one machine division steps from one level
22	# to the next, so no walk ever recomputes a power of two.
23	
24	def nthc(xs: List<&2, U32>, q: Nat) -> U32:
25	  match xs q:
26	    case Nil{} _:
27	      0
28	    case Con{x, t} 0n:
29	      x
30	    case Con{x, t} 1n+p:
31	      nthc(t, p)
32	
33	def nthc_nth(xs: List<&2, U32>, q: Nat, +h: {Nat.is_lt(q, SC.length(U32, xs)) == True{} : Bool}) -> {SC.nth(U32, xs, q) == Some{nthc(xs, q)} : Maybe<&2, U32>}:
34	  match xs q:
35	    case Nil{} _:
36	      Empty.absurd({SC.nth(U32, Nil{}, q) == Some{nthc(Nil{}, q)} : Maybe<&2, U32>}, N.lt_zero_absurd(q, h))
37	    case Con{x, t} 0n:
38	      {==}
39	    case Con{x, t} 1n+p:
40	      nthc_nth(t, p, h)
41	
42	
43	def add_one(+o: Nat) -> {Nat.add(o, 1n) == 1n+o : Nat}:
44	  %Equal.sym(Nat, Nat.add(o, 1n), 1n+Nat.add(o, 0n), N.add_succ(o, 0n)) : {_ == 1n+o : Nat}
45	  N.succ_cong(Nat.add(o, 0n), o, N.add_zero(o))
46	
47	def pow2_split(+q: Nat) -> {SC.pow2(1n+q) == Nat.add(SC.pow2(q), SC.pow2(q)) : Nat}:
48	  NA.double_self(SC.pow2(q))
49	
50	# o < o + 2^q
51	# o < o + 2^q
52	def lt_split(+o: Nat, +q: Nat) -> {Nat.is_lt(o, Nat.add(o, SC.pow2(q))) == True{} : Bool}:
53	  N.succ_le_lt(o, Nat.add(o, SC.pow2(q)),
54	    %add_one(o) : {Nat.is_le(_, Nat.add(o, SC.pow2(q))) == True{} : Bool}
55	    N.le_add_left(1n, SC.pow2(q), o, N.pow2_pos(q)))
56	
57	# o + 2^(1+q) == (o + 2^q) + 2^q
58	# o + 2^(1+q) == (o + 2^q) + 2^q
59	def split_assoc(+o: Nat, +q: Nat) -> {Nat.add(o, SC.pow2(1n+q)) == Nat.add(Nat.add(o, SC.pow2(q)), SC.pow2(q)) : Nat}:
60	  %Equal.sym(Nat, SC.pow2(1n+q), Nat.add(SC.pow2(q), SC.pow2(q)), pow2_split(q)) : {Nat.add(o, _) == Nat.add(Nat.add(o, SC.pow2(q)), SC.pow2(q)) : Nat}
61	  Equal.sym(Nat, Nat.add(Nat.add(o, SC.pow2(q)), SC.pow2(q)), Nat.add(o, Nat.add(SC.pow2(q), SC.pow2(q))), N.add_assoc(o, SC.pow2(q), SC.pow2(q)))
62	
63	# o + 2^q < o + 2^(1+q)
64	# o + 2^q < o + 2^(1+q)
65	def mid_lt(+o: Nat, +q: Nat) -> {Nat.is_lt(Nat.add(o, SC.pow2(q)), Nat.add(o, SC.pow2(1n+q))) == True{} : Bool}:
66	  %Equal.sym(Nat, Nat.add(o, SC.pow2(1n+q)), Nat.add(Nat.add(o, SC.pow2(q)), SC.pow2(q)), split_assoc(o, q)) : {Nat.is_lt(Nat.add(o, SC.pow2(q)), _) == True{} : Bool}
67	  lt_split(Nat.add(o, SC.pow2(q)), q)
68	
69	# ---- the model tree the cells realise ----
70	
71	def is_eq_sym(a: Nat, b: Nat) -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}:
72	  match a b:
73	    case 0n 0n:
74	      {==}
75	    case 0n 1n+y:
76	      {==}
77	    case 1n+x 0n:
78	      {==}
79	    case 1n+x 1n+y:
80	      is_eq_sym(x, y)
81	
82	def ne_gt(+a: Nat, +b: Nat, +h: {Nat.is_lt(b, a) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
83	  %Equal.sym(Bool, Nat.is_eq(a, b), Nat.is_eq(b, a), is_eq_sym(a, b)) : {_ == False{} : Bool}
84	  N.is_eq_lt(b, a, h)
85	
86	# 2^d <= 2^d + t
87	# 2^d <= 2^d + t
88	def base_le(+d: Nat, +t: Nat) -> {Nat.is_le(SC.pow2(d), Nat.add(SC.pow2(d), t)) == True{} : Bool}:
89	  N.le_add_right(SC.pow2(d), t)
90	
91	# ---- a write below the block ----
92	
93	def nthc_other(cl: List<&2, U32>, j: Nat, k: Nat, +v: U32, +ne: {Nat.is_eq(j, k) == False{} : Bool}) -> {nthc(SC.update(U32, cl, j, v), k) == nthc(cl, k) : U32}:
94	  match cl j k:
95	    case Nil{} _ _:
96	      {==}
97	    case Con{x, t} 0n 0n:
98	      Empty.absurd({nthc(Con{v, t}, 0n) == nthc(Con{x, t}, 0n) : U32}, L.false_true(Equal.sym(Bool, True{}, False{}, ne)))
99	    case Con{x, t} 0n 1n+b:
100	      {==}
101	    case Con{x, t} 1n+a 0n:
102	      {==}
103	    case Con{x, t} 1n+a 1n+b:
104	      nthc_other(t, a, b, v, ne)
105	
106	def nthc_same(cl: List<&2, U32>, j: Nat, +v: U32, +h: {Nat.is_lt(j, SC.length(U32, cl)) == True{} : Bool}) -> {nthc(SC.update(U32, cl, j, v), j) == v : U32}:
107	  match cl j:
108	    case Nil{} _:
109	      Empty.absurd({nthc(Nil{}, j) == v : U32}, N.lt_zero_absurd(j, h))
110	    case Con{x, t} 0n:
111	      {==}
112	    case Con{x, t} 1n+a:
113	      nthc_same(t, a, v, h)
114	
115	# 2^d < 2^(d+1)
116	def base_lt(+d: Nat) -> {Nat.is_lt(SC.pow2(d), SC.pow2(1n+d)) == True{} : Bool}:
117	  N.pow2_lt_succ(d)
118	
119	def in_cells(+cl: List<&2, U32>, +d: Nat, +k: Nat, +hk: {Nat.is_lt(k, SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(U32, cl) == SC.pow2(1n+d) : Nat}) -> {Nat.is_lt(k, SC.length(U32, cl)) == True{} : Bool}:
120	  L.subst(Nat, z => {Nat.is_lt(k, z) == True{} : Bool}, SC.pow2(1n+d), SC.length(U32, cl), Equal.sym(Nat, SC.length(U32, cl), SC.pow2(1n+d), hlen),
121	    N.lt_trans(k, SC.pow2(d), SC.pow2(1n+d), hk, base_lt(d)))
122	
123	def leaf_in_cells(+cl: List<&2, U32>, +d: Nat, +o: Nat, +ho: {Nat.is_lt(o, SC.pow2(d)) == True{} : Bool}, +hlen: {SC.length(U32, cl) == SC.pow2(1n+d) : Nat}) -> {Nat.is_lt(Nat.add(SC.pow2(d), o), SC.length(U32, cl)) == True{} : Bool}:
124	  L.subst(Nat, z => {Nat.is_lt(Nat.add(SC.pow2(d), o), z) == True{} : Bool}, SC.pow2(1n+d), SC.length(U32, cl), Equal.sym(Nat, SC.length(U32, cl), SC.pow2(1n+d), hlen),
125	    %Equal.sym(Nat, SC.pow2(1n+d), Nat.add(SC.pow2(d), SC.pow2(d)), pow2_split(d)) : {Nat.is_lt(Nat.add(SC.pow2(d), o), _) == True{} : Bool}
126	    N.lt_add_left(o, SC.pow2(d), SC.pow2(d), ho))
127	
128	# o < 2^d when the block [o, o+2^p) fits
129	# o < 2^d when the block [o, o+2^p) fits
130	def blk_lo(+o: Nat, +p: Nat, +d: Nat, +hw: {Nat.is_le(Nat.add(o, SC.pow2(p)), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(o, SC.pow2(d)) == True{} : Bool}:
131	  N.lt_le_trans(o, Nat.add(o, SC.pow2(p)), SC.pow2(d), lt_split(o, p), hw)
132	
133	# ---- the point addition walk is the model's ----
134	
135	# 2^d + o < 2^(d+1) and o + 2^q < 2^(d+1)
136	def leaf_lt(+d: Nat, +o: Nat, +ho: {Nat.is_lt(o, SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(SC.pow2(d), o), SC.pow2(1n+d)) == True{} : Bool}:
137	  %Equal.sym(Nat, SC.pow2(1n+d), Nat.add(SC.pow2(d), SC.pow2(d)), pow2_split(d)) : {Nat.is_lt(Nat.add(SC.pow2(d), o), _) == True{} : Bool}
138	  N.lt_add_left(o, SC.pow2(d), SC.pow2(d), ho)
139	
140	def node_lt(+o: Nat, +q: Nat, +d: Nat, +hw: {Nat.is_le(Nat.add(o, SC.pow2(1n+q)), SC.pow2(d)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(o, SC.pow2(q)), SC.pow2(1n+d)) == True{} : Bool}:
141	  N.lt_trans(Nat.add(o, SC.pow2(q)), SC.pow2(d), SC.pow2(1n+d),
142	    N.lt_le_trans(Nat.add(o, SC.pow2(q)), Nat.add(o, SC.pow2(1n+q)), SC.pow2(d), mid_lt(o, q), hw), base_lt(d))
143	
144	# ---- the prefix walk is the model's ----
145	
146	# The half size a walk carries at remaining depth p: 2^(p-1), and 0 at a
147	# leaf (where it is unused). One machine division steps from one level to the
148	# next, so no walk ever recomputes a power of two.
149	def hof(p: Nat) -> Nat:
150	  Nat.div(SC.pow2(p), 2n)
151	
152	def hof_succ(+q: Nat) -> {hof(1n+q) == SC.pow2(q) : Nat}:
153	  N.div2_pow2(q)
154	
155	# The comparison the source makes against the carried half size is exactly
156	# the model's branch decision.
157	def nthc_rep(m: Nat, k: Nat) -> {nthc(SC.replicate(U32, m, 0), k) == 0 : U32}:
158	  match m k:
159	    case 0n _:
160	      {==}
161	    case 1n+a 0n:
162	      {==}
163	    case 1n+a 1n+b:
164	      nthc_rep(a, b)
165