proofs/lib/flat.bend
bend-collections-laws-containers@1.0.0.0 · 165 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/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
24def 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
33def 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
43def 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
47def 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
52def 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
59def 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)
65def 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
71def 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
82def 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
88def 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
93def 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
106def 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)
116def base_lt(+d: Nat) -> {Nat.is_lt(SC.pow2(d), SC.pow2(1n+d)) == True{} : Bool}:
117 N.pow2_lt_succ(d)
118
119def 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
123def 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
130def 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)
136def 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
140def 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.
149def hof(p: Nat) -> Nat:
150 Nat.div(SC.pow2(p), 2n)
151
152def 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.
157def 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