proofs/containers/dynamic_array/clear.bend checks

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

11 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as AR
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/dynamic_array.bend as DA
import ./layout.bend as LY
import ./state.bend as ST
import ./steps.bend as SP
import ../../lib/array_ext.bend as AX

Definitions

def nones_rep_eq source · line 21 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.nones(T, xs) == True{} : Bool} -> {xs == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Maybe<&2, T>, xs), None{}) : List<&2, Maybe<&2, T>>}

A list of Nones is the replication of None to its length.

def lay0_nones source · line 31 · raw

@-T:Data -> @+xs:List<&2, Maybe<&2, T>> -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, xs, 0n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.nones(T, xs) == True{} : Bool}

A layout of length 0 holds only Nones.

def empty_slots_eq source · line 41 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(Maybe<&2, T>, d, t) == True{} : Bool} -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/layout.lay(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t), 0n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(Maybe<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(Maybe<&2, T>, d, None{})) : List<&2, Maybe<&2, T>>}

The slots of a good empty shadow are those of the all-None tree.

Templates

template clear_go_eq source · line 48 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+k:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, k, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_go_at(T, k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(Maybe<&2, T>, t)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_slots(T, d) : Array<Maybe<&2, T>>}

Resetting the k occupied slots of a good shadow gives the all-None block.

template clear_eq source · line 69 · raw

@-T:Data -> @+l:Nat -> @+d:Nat -> @+n:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<Maybe<&2, T>> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_at(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Sh{l, d, n, t})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>}