proofs/storage_allocation_refinement.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as Storage_allocation_refinement

6 imports

import Base
import ../storage_buffer.bend as Storage
import ../storage_allocation.bend as Allocation
import ./storage_tree_model.bend as Tree
import ./storage_refinement.bend as StorageLaws
import ./storage_buffer_model.bend as Buffer

Definitions

def dispatch_same source · line 10 · raw

@-Element:Data -> @-allocator:(@_:Nat -> @_:Element -> @_:Nat -> 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>) -> @depth:Nat -> @+value:Element -> @+length:Nat -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.dispatch(Element, allocator, depth, value, length) == allocator(depth, value, length) : 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.Buffer<Element>}

Dispatch changes neither the initialized array nor its live certificate. This is an unconditional equation for every element type, depth and length.

def array_same source · line 46 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.array(Element, depth, value) == Array.new(Element, depth, value) : Array<Element>}

Templates

template fresh source · line 53 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> {0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.array(Element, depth, value) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.pack(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, value)) : Array<Element>}

template contents source · line 58 · raw

@-Element:Data -> @+depth:Nat -> @+value:Element -> @+length:Nat -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_buffer_model.contents(Element, 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.allocate(Element, depth, value, length)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_buffer_model.Content{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.fresh(Element, depth, value), length} : 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_buffer_model.Content<Element>}