~/bend-docscommunity

proofs/containers/dynamic_array/layout.bend checks

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

5 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC

Definitions

def somes source · line 9 · raw

@-T:Data -> @xs:List<&2, Maybe<&2, T>> -> List<&2, T>

def nones source · line 18 · raw

@-T:Data -> @xs:List<&2, Maybe<&2, T>> -> Bool

def lay source · line 27 · raw

@-T:Data -> @xs:List<&2, Maybe<&2, T>> -> @n:Nat -> Bool

def nones_somes source · line 42 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+h:{nones(T, xs) == True{} : Bool} -> {somes(T, xs) == [] : List<&2, T>}

def lay_len source · line 51 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+h:{lay(T, xs, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, somes(T, xs)) == n : Nat}

def lay_le source · line 67 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+h:{lay(T, xs, n) == True{} : Bool} -> {Nat.is_le(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool}

def lay_nil_pos source · line 82 · raw

@-T:Data -> @+n:Nat -> @+i:Nat -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {lay(T, [], n) == False{} : Bool}

def lay_nth source · line 90 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+i:Nat -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, xs, i) == Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, somes(T, xs), i)} : Maybe<&2, Maybe<&2, T>>}

Slot i (< n) holds exactly the i-th item.

def nones_nth source · line 105 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+i:Nat -> @+h:{nones(T, xs) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, xs, i) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}

def nones_rep source · line 116 · raw

@-T:Data -> @+k:Nat -> {nones(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, k, None{})) == True{} : Bool}

def somes_rep source · line 123 · raw

@-T:Data -> @+k:Nat -> {somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, k, None{})) == [] : List<&2, T>}

def lay_rep source · line 130 · raw

@-T:Data -> @+k:Nat -> {lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, k, None{}), 0n) == True{} : Bool}

def nones_lay0 source · line 137 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+h:{nones(T, xs) == True{} : Bool} -> {lay(T, xs, 0n) == True{} : Bool}

def lay0_nones source · line 146 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+h:{lay(T, xs, 0n) == True{} : Bool} -> {nones(T, xs) == True{} : Bool}

def nones_append source · line 155 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+ys:List<&2, Maybe<&2, T>> -> @+hx:{nones(T, xs) == True{} : Bool} -> @+hy:{nones(T, ys) == True{} : Bool} -> {nones(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, xs, ys)) == True{} : Bool}

def lay_set source · line 166 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+i:Nat -> @+v:T -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, i, Some{v}), n) == True{} : Bool}

def somes_set source · line 181 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+i:Nat -> @+v:T -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, i, Some{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(T, somes(T, xs), i, v) : List<&2, T>}

def push_free source · line 198 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Maybe<&2, T>, xs, n) == Some{None{}} : Maybe<&2, Maybe<&2, T>>}

def lay_push source · line 211 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:T -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool} -> {lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, n, Some{v}), 1n+n) == True{} : Bool}

def somes_push source · line 224 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+v:T -> @+h:{lay(T, xs, n) == True{} : Bool} -> @+hn:{Nat.is_lt(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs)) == True{} : Bool} -> {somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, n, Some{v})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(T, somes(T, xs), v) : List<&2, T>}

def lay_pop source · line 240 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+m:Nat -> @+h:{lay(T, xs, 1n+m) == True{} : Bool} -> {lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, m, None{}), m) == True{} : Bool}

def init_cons source · line 251 · raw

@-T:Data -> @+x:T -> @+ys:List<&2, T> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, ys) == 1n+k : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, x <> ys) == x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, ys) : List<&2, T>}

def somes_pop source · line 258 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+m:Nat -> @+h:{lay(T, xs, 1n+m) == True{} : Bool} -> {somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Maybe<&2, T>, xs, m, None{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.init(T, somes(T, xs)) : List<&2, T>}

def nth_last source · line 273 · raw

@-T:Data -> @+ys:List<&2, T> -> @+m:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(T, ys) == 1n+m : Nat} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, ys, m) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.last(T, ys) : Maybe<&2, T>}

nth at the last position is last.

def lay_grow source · line 288 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+n:Nat -> @+k:Nat -> @+h:{lay(T, xs, n) == True{} : Bool} -> {lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, k, None{})), n) == True{} : Bool}

def somes_grow source · line 303 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+k:Nat -> {somes(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Maybe<&2, T>, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, k, None{}))) == somes(T, xs) : List<&2, T>}