~/bend-docscommunity

proofs/containers/bitlist/state.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitlist/state.bend as State

10 imports
import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitlist.bend as BLI
import ../dynamic_array/state.bend as DAS
import ../bitset/lists.bend as BL
import ../bitset/state.bend as ST
import ../../../spec/containers/bitlist.bend as S
import ./da.bend as DI

Types

type Sh source · line 22 · raw

Data

Definitions

def fl source · line 25 · raw

@w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> List<&2, Bool>

def real source · line 28 · raw

@sh:Sh -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist

def good source · line 33 · raw

@sh:Sh -> Bool

def model source · line 38 · raw

@sh:Sh -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model

def g_w source · line 44 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{good(BSh{l, n, w}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool}

def g_inv source · line 47 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+g:{good(BSh{l, n, w}) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, fl(w)) == True{} : Bool}

def g_mk source · line 50 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gw:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w) == True{} : Bool} -> @+gi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, fl(w)) == True{} : Bool} -> {good(BSh{l, n, w}) == True{} : Bool}

def same_good source · line 54 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+w2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+gw2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w2) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(w2) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(w) : List<&2, U32>} -> @+g:{good(BSh{l, n, w}) == True{} : Bool} -> {good(BSh{l, n, w2}) == True{} : Bool}

A word array with the same words: the invariant and the model carry over.

def model_of source · line 58 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+xs:List<&2, U32> -> @+c:Nat -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(w2) == xs : List<&2, U32>} -> @+ec:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.lim(w2) == c : Nat} -> {model(BSh{l, n, w2}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.M{l, c, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(xs), n)} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

The model of a shadow with given words and depth limit.

def good_of source · line 63 · raw

@+l:Maybe<&2, Nat> -> @+n:Nat -> @+w2:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+xs:List<&2, U32> -> @+gw2:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, w2) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/da.ws(w2) == xs : List<&2, U32>} -> @+gi:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(xs)) == True{} : Bool} -> {good(BSh{l, n, w2}) == True{} : Bool}