~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0xd684886d10b431b9dce6c3b2d1ef1980/LAWS.bend as LAWS

3 imports
import Base
import ./main.bend as V
import ./observations.bend as O

Laws

law empty_contents provedin PROOF.bendsource · line 8 · raw

@-T:Data -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(T)) == [] : List<&1, T>}

Universal over arbitrary Data elements; vector shapes/indices are fixed. These are substantive finite-shape refinement theorems, not a proof for all reachable lengths, capacities, or arbitrary operation traces.

law singleton_get provedin PROOF.bendsource · line 12 · raw

@-T:Data -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.get(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.one(T, x), 0)) == Done{x} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>}

law growth_order provedin PROOF.bendsource · line 17 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @d:T -> @e:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.five(T, a, b, c, d, e)) == [a, b, c, d, e] : List<&1, T>}

law reserve_preserves provedin PROOF.bendsource · line 26 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.reserve(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 17)) == ([a, b, c], Done{Unit{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law set_preserves provedin PROOF.bendsource · line 33 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.set(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 1, x)) == ([a, x, c], Done{Unit{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law swap_old_and_preserves provedin PROOF.bendsource · line 41 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.pop_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.swap(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 1, x)) == ([a, x, c], Done{b}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>)}

law push_pop_growth provedin PROOF.bendsource · line 49 · raw

@-T:Data -> @a:T -> @b:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.pop_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.pop(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, x))) == ([a, b], Done{x}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>)}

law slice_order provedin PROOF.bendsource · line 56 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @d:T -> @e:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.slice_result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.slice(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.five(T, a, b, c, d, e), 1, 4)) == Done{[b, c, d]} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, List<&1, T>>}

law logical_bounds provedin PROOF.bendsource · line 65 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.set(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 3, x)) == ([a, b, c], Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.Bounds{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law max_index provedin PROOF.bendsource · line 73 · raw

@-T:Data -> @a:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.get(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.one(T, a), 4294967295)) == Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.Bounds{}} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>}

law zero_limit provedin PROOF.bendsource · line 78 · raw

@-T:Data -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.push(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.bounded(T, 0), x)) == ([], Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.Limit{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law empty_pop provedin PROOF.bendsource · line 83 · raw

@-T:Data -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.pop_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.pop(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(T))) == ([], Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.Empty{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>)}

law empty_slice provedin PROOF.bendsource · line 87 · raw

@-T:Data -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.slice_result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.slice(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(T), 0, 0)) == Done{[]} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, List<&1, T>>}

law reversed_slice provedin PROOF.bendsource · line 91 · raw

@-T:Data -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.slice_result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.slice(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.one(T, x), 1, 0)) == Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.InvalidRange{}} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, List<&1, T>>}

law maximum_reserve provedin PROOF.bendsource · line 96 · raw

@-T:Data -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.reserve(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.one(T, x), 4294967295)) == ([x], Fail{0xd684886d10b431b9dce6c3b2d1ef1980/main.Limit{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law initial_metadata provedin PROOF.bendsource · line 102 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/observations.metadata(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.length(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(U32))) == 0 : U32}

Concrete metadata normalizations, distinct from the element-parametric laws.

law initial_capacity provedin PROOF.bendsource · line 104 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/observations.metadata(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.capacity(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(U32))) == 1 : U32}

law rounded_capacity provedin PROOF.bendsource · line 106 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/observations.metadata(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.capacity(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.vector(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.reserve(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.new(U32), 17)))) == 32 : U32}

law effective_limit provedin PROOF.bendsource · line 108 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/observations.metadata(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.limit(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.bounded(U32, 4294967295))) == 16777216 : U32}

law get_preserves provedin PROOF.bendsource · line 111 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.pop_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.get(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 1)) == ([a, b, c], Done{b}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>)}

law set_then_get provedin PROOF.bendsource · line 118 · raw

@-T:Data -> @a:T -> @b:T -> @c:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.result(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.get(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.vector(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.set(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, c), 1, x)), 1)) == Done{x} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, T>}

law push_success provedin PROOF.bendsource · line 126 · raw

@-T:Data -> @a:T -> @b:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_contents(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.push(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.two(T, a, b), x)) == ([a, b, x], Done{Unit{}}) : Pair(List<&1, T>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>)}

law pop_length provedin PROOF.bendsource · line 134 · raw

@-T:Data -> @a:T -> @b:T -> @x:T -> {0xd684886d10b431b9dce6c3b2d1ef1980/observations.metadata(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.length(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.value_vector(T, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.pop(T, 0xd684886d10b431b9dce6c3b2d1ef1980/observations.three(T, a, b, x))))) == 2 : U32}

Necessary state observation: contents alone cannot see an empty trailing slot.

law maximum_plan provedin PROOF.bendsource · line 142 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/main.plan_step(24n, 1, 0n, 16777216, False{}) == (16777216, 24n) : Pair(U32, Nat)}

Arithmetic-only ceiling witness: no 2^24-slot allocation is needed to check it.

law exact_limit_reserve provedin PROOF.bendsource · line 144 · raw

{0xd684886d10b431b9dce6c3b2d1ef1980/observations.unit_result(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.reserve(U32, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec.bounded(U32, 3), 3)) == Done{Unit{}} : Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>}