~/bend-docscommunity

proofs/containers/dynamic_array/owned_swap.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_swap.bend as Owned_swap

1 import
import Base

Definitions

def undo source · line 5 · raw

@-T:Type -> @+n:U32 -> @+i:U32 -> @r:Pair(Array<T>, T) -> Pair(Array<T>, T)

A constructive certificate carries the moved values, rather than copying a Type-valued input into two recursive proof calls.

def Cert source · line 9 · raw

@-T:Type -> @-a:Array<T> -> @-n:U32 -> @-i:U32 -> @-v:T -> Type

def lift_left source · line 12 · raw

@-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)

def lift_right source · line 23 · raw

@-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)

def certificate source · line 36 · raw

@-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)

The branch decision is an explicit parameter, so recursion remains on a proper subarray and the owning replacement is passed to exactly one child.

def finish source · line 45 · raw

@-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) : Pair(Array<T>, T)}

def roundtrip source · line 51 · raw

@-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) : Pair(Array<T>, T)}