1	import Base
2	
3	# A constructive certificate carries the moved values, rather than copying a
4	# Type-valued input into two recursive proof calls.
5	def 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	
9	def 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	
12	def 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	
23	def 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.
36	def 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	
45	def 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	
51	def 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)), {==}))