proof_shape.bend

lawful-arrays@0.1.0.0 · 201 lines · 18 definitions

1import Base
2import lawful-arrays@0.1.0.0/defs.bend as D
3import lawful-arrays@0.1.0.0/proof_base.bend as B
4import lawful-arrays@0.1.0.0/proof_tree.bend as P
5
6# Array.swap and Array.set keep a tree perfect, for any element type. Such
7# elements cannot be copied, so no mirror: the lemmas return the new array as a
8# witness beside the equations, and each subtree is used once.
9
10# Array.size(a) is (b, n) with b == a.
11def SizeW(-T: Type, -a: Array<T>) -> Type:
12  &b:Array<T> -> &n:U32 -> {Array.size(T, a) == (b, n) : Array<T> & U32} & {b == a : Array<T>}
13
14law size_node_eq:
15  for -T: Type
16  for -xs: Array<T>
17  for -ys: Array<T>
18  for -b: Array<T>
19  for -n: U32
20  for e: {Array.size(T, xs) == (b, n) : Array<T> & U32}
21  {Array.size(T, ANode{xs, ys}) == (ANode{b, ys}, U32.shl(n)) : Array<T> & U32}
22
23def size_node_eq(T, xs, ys, b, n, e):
24  %Equal.sym(Array<T> & U32, Array.size(T, xs), (b, n), e) :
25    {Array.size.node(T, ys, _) == (ANode{b, ys}, U32.shl(n)) : Array<T> & U32}
26  {==}
27
28def size_w.node(-T: Type, -xs: Array<T>, ys: Array<T>, w: SizeW(T, xs)) -> SizeW(T, ANode{xs, ys}):
29  (b, n, e, q) = w
30  (ANode{b, ys}, U32.shl(n), size_node_eq(T, xs, ys, b, n, e), P.anode_eq(T, b, ys, xs, ys, q, {==}))
31
32def size_w(-T: Type, a: Array<T>) -> SizeW(T, a):
33  match a:
34    case ALeaf{x}:
35      (ALeaf{x}, 1, {==}, {==})
36    case ANode{xs, ys}:
37      size_w.node(T, xs, ys, size_w(T, xs))
38
39# Array.swap.go(a, ...) is (na, old) with na as perfect as a at every depth.
40def SwapW(-T: Type, -a: Array<T>, -n: U32, -i: U32, -v: T, -z: Bool, -d: Nat) -> Type:
41  &na:Array<T> -> &old:T -> {Array.swap.go(T, a, n, i, v, z) == (na, old) : Array<T> & T}
42    & {D.full(T, na, d) == D.full(T, a, d) : Bool}
43
44law lo_eq:
45  for -T: Type
46  for -ys: Array<T>
47  for -r: Array<T> & T
48  for -na: Array<T>
49  for -old: T
50  for e: {r == (na, old) : Array<T> & T}
51  {Array.swap.lo(T, ys, r) == (ANode{na, ys}, old) : Array<T> & T}
52
53def lo_eq(T, ys, r, na, old, e):
54  %Equal.sym(Array<T> & T, r, (na, old), e) : {Array.swap.lo(T, ys, _) == (ANode{na, ys}, old) : Array<T> & T}
55  {==}
56
57law hi_eq:
58  for -T: Type
59  for -xs: Array<T>
60  for -r: Array<T> & T
61  for -na: Array<T>
62  for -old: T
63  for e: {r == (na, old) : Array<T> & T}
64  {Array.swap.hi(T, xs, r) == (ANode{xs, na}, old) : Array<T> & T}
65
66def hi_eq(T, xs, r, na, old, e):
67  %Equal.sym(Array<T> & T, r, (na, old), e) : {Array.swap.hi(T, xs, _) == (ANode{xs, na}, old) : Array<T> & T}
68  {==}
69
70law and_eq_l:
71  for -a: Bool
72  for -c: Bool
73  for -b: Bool
74  for e: {a == c : Bool}
75  {Bool.and(a, b) == Bool.and(c, b) : Bool}
76
77def and_eq_l(a, c, b, e):
78  %e : {Bool.and(a, b) == Bool.and(_, b) : Bool}
79  {==}
80
81law and_eq_r:
82  for -b: Bool
83  for -a: Bool
84  for -c: Bool
85  for e: {a == c : Bool}
86  {Bool.and(b, a) == Bool.and(b, c) : Bool}
87
88def and_eq_r(b, a, c, e):
89  %e : {Bool.and(b, a) == Bool.and(b, _) : Bool}
90  {==}
91
92def swap_w.lo(-T: Type, -xs: Array<T>, ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
93  w: SwapW(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n))), B.pred(d))) ->
94  SwapW(T, ANode{xs, ys}, n, i, v, True{}, d):
95  match d:
96    case 0n:
97      (na, old, e, q) = w
98      (ANode{na, ys}, old,
99        lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e), {==})
100    case 1n+p:
101      (na, old, e, q) = w
102      (ANode{na, ys}, old,
103        lo_eq(T, ys, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), na, old, e),
104        and_eq_l(D.full(T, na, p), D.full(T, xs, p), D.full(T, ys, p), q))
105
106def swap_w.hi(-T: Type, xs: Array<T>, -ys: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
107  w: SwapW(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n))), B.pred(d))) ->
108  SwapW(T, ANode{xs, ys}, n, i, v, False{}, d):
109  match d:
110    case 0n:
111      (na, old, e, q) = w
112      (ANode{xs, na}, old,
113        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
114          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e), {==})
115    case 1n+p:
116      (na, old, e, q) = w
117      (ANode{xs, na}, old,
118        hi_eq(T, xs, Array.swap.go(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v,
119          U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), na, old, e),
120        and_eq_r(D.full(T, xs, p), D.full(T, na, p), D.full(T, ys, p), q))
121
122def swap_w(-T: Type, a: Array<T>, +n: U32, +i: U32, v: T, +z: Bool, +d: Nat) -> SwapW(T, a, n, i, v, z, d):
123  match a z d:
124    case ALeaf{x} _ 0n:
125      (ALeaf{v}, x, {==}, {==})
126    case ALeaf{x} _ 1n+p:
127      (ALeaf{v}, x, {==}, {==})
128    case ANode{xs, ys} True{} _:
129      +h = U32.shr(n)
130      swap_w.lo(T, xs, ys, n, i, v, d, swap_w(T, xs, h, i, v, U32.is_lt(i, U32.shr(h)), B.pred(d)))
131    case ANode{xs, ys} False{} _:
132      +h = U32.shr(n)
133      +j = U32.sub(i, h)
134      swap_w.hi(T, xs, ys, n, i, v, d, swap_w(T, ys, h, j, v, U32.is_lt(j, U32.shr(h)), B.pred(d)))
135
136# The array a swap leaves is perfect: the steps after Array.size.
137def swap_full.fin(-T: Type, -a: Array<T>, -b: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
138  hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array<T>},
139  w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) ->
140  {D.full(T, Pair.fst(Array<T>, T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
141    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}:
142  (na, old, e, f) = w
143  %Equal.sym(Array<T> & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
144    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) :
145    {D.full(T, Pair.fst(Array<T>, T, _), d) == True{} : Bool}
146  Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f,
147    Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{},
148      Equal.cong(Array<T>, Bool, x => D.full(T, x, d), b, a, q), hf))
149
150def swap_full.go(-T: Type, -a: Array<T>, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool},
151  w: SizeW(T, a)) -> {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}:
152  (b, +n, e, q) = w
153  %Equal.sym(Array<T> & U32, Array.size(T, a), (b, n), e) :
154    {D.full(T, Pair.fst(Array<T>, T, Array.swap.at(T, i, v, _)), d) == True{} : Bool}
155  +j = U32.and(i, U32.sub(n, 1))
156  swap_full.fin(T, a, b, n, i, v, d, hf, q, swap_w(T, b, n, j, v, U32.is_lt(j, U32.shr(n)), d))
157
158law swap_full:
159  for -T: Type
160  for a: Array<T>
161  for +d: Nat
162  for +i: U32
163  for v: T
164  for hf: {D.full(T, a, d) == True{} : Bool}
165  {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}
166
167def swap_full(T, a, d, i, v, hf):
168  swap_full.go(T, a, d, i, v, hf, size_w(T, a))
169
170def set_full.fin(-T: Type, -a: Array<T>, -b: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
171  hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array<T>},
172  w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) ->
173  {D.full(T, Array.set.fin(T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
174    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}:
175  (na, old, e, f) = w
176  %Equal.sym(Array<T> & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
177    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) :
178    {D.full(T, Array.set.fin(T, _), d) == True{} : Bool}
179  Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f,
180    Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{},
181      Equal.cong(Array<T>, Bool, x => D.full(T, x, d), b, a, q), hf))
182
183def set_full.go(-T: Type, -a: Array<T>, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool},
184  w: SizeW(T, a)) -> {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}:
185  (b, +n, e, q) = w
186  %Equal.sym(Array<T> & U32, Array.size(T, a), (b, n), e) :
187    {D.full(T, Array.set.fin(T, Array.swap.at(T, i, v, _)), d) == True{} : Bool}
188  +j = U32.and(i, U32.sub(n, 1))
189  set_full.fin(T, a, b, n, i, v, d, hf, q, swap_w(T, b, n, j, v, U32.is_lt(j, U32.shr(n)), d))
190
191law set_full:
192  for -T: Type
193  for a: Array<T>
194  for +d: Nat
195  for +i: U32
196  for v: T
197  for hf: {D.full(T, a, d) == True{} : Bool}
198  {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}
199
200def set_full(T, a, d, i, v, hf):
201  set_full.go(T, a, d, i, v, hf, size_w(T, a))