LAWS.bend source
LAWS.bend on the hub · documented module
import Baseimport ./main.bend as Vimport ./observations.bend as O# 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 empty_contents: for -T: Data {O.contents(T,V.Vec.new(T)) == Nil{} : List<T>}law singleton_get: for -T: Data for x: T {O.result(T,V.Vec.get(T,O.one(T,x),0)) == Done{x} : Result<V.Error,T>}law growth_order: for -T: Data for a: T for b: T for c: T for d: T for e: T {O.contents(T,O.five(T,a,b,c,d,e)) == [a,b,c,d,e] : List<T>}law reserve_preserves: for -T: Data for a: T for b: T for c: T {O.unit_contents(T,V.Vec.reserve(T,O.three(T,a,b,c),17)) == ([a,b,c],Done{Unit{}}) : List<T> & Result<V.Error,Unit>}law set_preserves: for -T: Data for a: T for b: T for c: T for x: T {O.unit_contents(T,V.Vec.set(T,O.three(T,a,b,c),1,x)) == ([a,x,c],Done{Unit{}}) : List<T> & Result<V.Error,Unit>}law swap_old_and_preserves: for -T: Data for a: T for b: T for c: T for x: T {O.pop_contents(T,V.Vec.swap(T,O.three(T,a,b,c),1,x)) == ([a,x,c],Done{b}) : List<T> & Result<V.Error,T>}law push_pop_growth: for -T: Data for a: T for b: T for x: T {O.pop_contents(T,V.Vec.pop(T,O.three(T,a,b,x))) == ([a,b],Done{x}) : List<T> & Result<V.Error,T>}law slice_order: for -T: Data for a: T for b: T for c: T for d: T for e: T {O.slice_result(T,V.Vec.slice(T,O.five(T,a,b,c,d,e),1,4)) == Done{[b,c,d]} : Result<V.Error,List<T>>}law logical_bounds: for -T: Data for a: T for b: T for c: T for x: T {O.unit_contents(T,V.Vec.set(T,O.three(T,a,b,c),3,x)) == ([a,b,c],Fail{V.Bounds{}}) : List<T> & Result<V.Error,Unit>}law max_index: for -T: Data for a: T {O.result(T,V.Vec.get(T,O.one(T,a),4294967295)) == Fail{V.Bounds{}} : Result<V.Error,T>}law zero_limit: for -T: Data for x: T {O.unit_contents(T,V.Vec.push(T,V.Vec.bounded(T,0),x)) == (Nil{},Fail{V.Limit{}}) : List<T> & Result<V.Error,Unit>}law empty_pop: for -T: Data {O.pop_contents(T,V.Vec.pop(T,V.Vec.new(T))) == (Nil{},Fail{V.Empty{}}) : List<T> & Result<V.Error,T>}law empty_slice: for -T: Data {O.slice_result(T,V.Vec.slice(T,V.Vec.new(T),0,0)) == Done{Nil{}} : Result<V.Error,List<T>>}law reversed_slice: for -T: Data for x: T {O.slice_result(T,V.Vec.slice(T,O.one(T,x),1,0)) == Fail{V.InvalidRange{}} : Result<V.Error,List<T>>}law maximum_reserve: for -T: Data for x: T {O.unit_contents(T,V.Vec.reserve(T,O.one(T,x),4294967295)) == ([x],Fail{V.Limit{}}) : List<T> & Result<V.Error,Unit>}# Concrete metadata normalizations, distinct from the element-parametric laws.law initial_metadata: {O.metadata(U32,V.Vec.length(U32,V.Vec.new(U32))) == 0 : U32}law initial_capacity: {O.metadata(U32,V.Vec.capacity(U32,V.Vec.new(U32))) == 1 : U32}law rounded_capacity: {O.metadata(U32,V.Vec.capacity(U32,O.vector(U32,V.Vec.reserve(U32,V.Vec.new(U32),17)))) == 32 : U32}law effective_limit: {O.metadata(U32,V.Vec.limit(U32,V.Vec.bounded(U32,4294967295))) == 16777216 : U32}law get_preserves: for -T: Data for a: T for b: T for c: T {O.pop_contents(T,V.Vec.get(T,O.three(T,a,b,c),1)) == ([a,b,c],Done{b}) : List<T> & Result<V.Error,T>}law set_then_get: for -T: Data for a: T for b: T for c: T for x: T {O.result(T,V.Vec.get(T,O.vector(T,V.Vec.set(T,O.three(T,a,b,c),1,x)),1)) == Done{x} : Result<V.Error,T>}law push_success: for -T: Data for a: T for b: T for x: T {O.unit_contents(T,V.Vec.push(T,O.two(T,a,b),x)) == ([a,b,x],Done{Unit{}}) : List<T> & Result<V.Error,Unit>}# Necessary state observation: contents alone cannot see an empty trailing slot.law pop_length: for -T: Data for a: T for b: T for x: T {O.metadata(T,V.Vec.length(T,O.value_vector(T,V.Vec.pop(T,O.three(T,a,b,x))))) == 2 : U32}# Arithmetic-only ceiling witness: no 2^24-slot allocation is needed to check it.law maximum_plan: {V.plan_step(24n,1,0n,16777216,False{}) == (16777216,24n) : U32 & Nat}law exact_limit_reserve: {O.unit_result(U32,V.Vec.reserve(U32,V.Vec.bounded(U32,3),3)) == Done{Unit{}} : Result<V.Error,Unit>}