proofs/containers/dynamic_array/owned_swap.bend
bend-collections-laws-containers@1.0.0.0 · 52 lines · 0 definitions
1import Base
2
3# A constructive certificate carries the moved values, rather than copying a
4# Type-valued input into two recursive proof calls.
5def undo(-T: Type, +n: U32, +i: U32, r: Array<T> & T) -> Array<T> & T:
6 (a, old) = r
7 Array.swap.go(T, a, n, i, old, U32.is_lt(i, U32.shr(n)))
8
9def Cert(-T: Type, -a: Array<T>, -n: U32, -i: U32, -v: T) -> Type:
10 Sigma<&1, &1, Array<T> & T, r => ({Array.swap.go(T, a, n, i, v, U32.is_lt(i, U32.shr(n))) == r : Array<T> & T} & {undo(T, n, i, r) == (a, v) : Array<T> & T})>
11
12def lift_left(-T: Type, -xs: Array<T>, ys: Array<T>, +n: U32, +i: U32, -v: T, +e: {U32.is_lt(i, U32.shr(n)) == True{} : Bool}, r: Cert(T, xs, U32.shr(n), i, v)) -> Cert(T, ANode{xs, ys}, n, i, v):
13 match r:
14 case Tuple{Tuple{zs, old}, Tuple{+forward, +backward}}:
15 ((ANode{zs, ys}, old), (
16 %Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), True{}, e) : {Array.swap.go(T, ANode{xs, ys}, n, i, v, _) == (ANode{zs, ys}, old) : Array<T> & T}
17 %Equal.sym(Array<T> & T, Array.swap.go(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n)))), (zs, old), forward) : {Array.swap.lo(T, ys, _) == (ANode{zs, ys}, old) : Array<T> & T}
18 {==},
19 %Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), True{}, e) : {Array.swap.go(T, ANode{zs, ys}, n, i, old, _) == (ANode{xs, ys}, v) : Array<T> & T}
20 %Equal.sym(Array<T> & T, Array.swap.go(T, zs, U32.shr(n), i, old, U32.is_lt(i, U32.shr(U32.shr(n)))), (xs, v), backward) : {Array.swap.lo(T, ys, _) == (ANode{xs, ys}, v) : Array<T> & T}
21 {==}))
22
23def lift_right(-T: Type, xs: Array<T>, -ys: Array<T>, +n: U32, +i: U32, -v: T, +e: {U32.is_lt(i, U32.shr(n)) == False{} : Bool}, r: Cert(T, ys, U32.shr(n), U32.sub(i, U32.shr(n)), v)) -> Cert(T, ANode{xs, ys}, n, i, v):
24 match r:
25 case Tuple{Tuple{zs, old}, Tuple{+forward, +backward}}:
26 ((ANode{xs, zs}, old), (
27 %Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), False{}, e) : {Array.swap.go(T, ANode{xs, ys}, n, i, v, _) == (ANode{xs, zs}, old) : Array<T> & T}
28 %Equal.sym(Array<T> & T, Array.swap.go(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)))), (zs, old), forward) : {Array.swap.hi(T, xs, _) == (ANode{xs, zs}, old) : Array<T> & T}
29 {==},
30 %Equal.sym(Bool, U32.is_lt(i, U32.shr(n)), False{}, e) : {Array.swap.go(T, ANode{xs, zs}, n, i, old, _) == (ANode{xs, ys}, v) : Array<T> & T}
31 %Equal.sym(Array<T> & T, Array.swap.go(T, zs, U32.shr(n), U32.sub(i, U32.shr(n)), old, U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), (ys, v), backward) : {Array.swap.hi(T, xs, _) == (ANode{xs, ys}, v) : Array<T> & T}
32 {==}))
33
34# The branch decision is an explicit parameter, so recursion remains on a
35# proper subarray and the owning replacement is passed to exactly one child.
36def certificate(-T: Type, a: Array<T>, +n: U32, +i: U32, v: T, b: Bool, +eb: {U32.is_lt(i, U32.shr(n)) == b : Bool}) -> Cert(T, a, n, i, v):
37 match a b:
38 case ALeaf{x} _:
39 ((ALeaf{v}, x), ({==}, {==}))
40 case ANode{xs, ys} True{}:
41 lift_left(T, xs, ys, n, i, v, eb, certificate(T, xs, U32.shr(n), i, v, U32.is_lt(i, U32.shr(U32.shr(n))), {==}))
42 case ANode{xs, ys} False{}:
43 lift_right(T, xs, ys, n, i, v, eb, certificate(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))), {==}))
44
45def finish(-T: Type, -a: Array<T>, +n: U32, +i: U32, -v: T, r: Cert(T, a, n, i, v)) -> {undo(T, n, i, Array.swap.go(T, a, n, i, v, U32.is_lt(i, U32.shr(n)))) == (a, v) : Array<T> & T}:
46 match r:
47 case Tuple{out, Tuple{+forward, backward}}:
48 %Equal.sym(Array<T> & T, Array.swap.go(T, a, n, i, v, U32.is_lt(i, U32.shr(n))), out, forward) : {undo(T, n, i, _) == (a, v) : Array<T> & T}
49 backward
50
51def roundtrip(-T: Type, a: Array<T>, +n: U32, +i: U32, v: T) -> {undo(T, n, i, Array.swap.go(T, a, n, i, v, U32.is_lt(i, U32.shr(n)))) == (a, v) : Array<T> & T}:
52 finish(T, a, n, i, v, certificate(T, a, n, i, v, U32.is_lt(i, U32.shr(n)), {==}))