proofs/storage_address_bounds.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as Storage_address_bounds

Machine address bounds for balanced storage, independent of element values.

10 imports

import Base
import ./storage_shape.bend as Shape
import ./natural_addition.bend as Addition
import ./word_encoding.bend as WordEncoding
import ./word_power_of_two.bend as Power
import ./nat_order.bend as Order
import ./nat_to_u32_bounds.bend as Bounds
import ./u32_comparison.bend as Comparison
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./word_subtraction.bend as Subtraction

Definitions

def capacity source · line 13 · raw

@depth:Nat -> U32

def shift_extent source · line 16 · raw

@depth:Nat -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.shift(depth, 1n) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.extent(depth) : Nat}

def capacity_value source · line 22 · raw

@+depth:Nat -> @limit:{Nat.is_le(depth, 31n) == True{} : Bool} -> {U32.to_nat(capacity(depth)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.extent(depth) : Nat}

def natural_bound source · line 28 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(depth, 31n) == True{} : Bool} -> @bound:{U32.is_lt(index, capacity(depth)) == True{} : Bool} -> {Nat.is_lt(U32.to_nat(index), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.extent(depth)) == True{} : Bool}

def child_limit_full source · line 33 · raw

@+depth:Nat -> @limit:{Nat.is_le(1n+depth, 31n) == True{} : Bool} -> {Nat.is_le(depth, 31n) == True{} : Bool}

def right_order source · line 36 · raw

@+depth:Nat -> @+index:U32 -> @choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {Nat.is_le(U32.to_nat(capacity(depth)), U32.to_nat(index)) == True{} : Bool}

def sub_value source · line 42 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(1n+depth, 31n) == True{} : Bool} -> @+bound:{U32.is_lt(index, capacity(1n+depth)) == True{} : Bool} -> @choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {U32.to_nat(U32.sub(index, capacity(depth))) == Nat.sub(U32.to_nat(index), U32.to_nat(capacity(depth))) : Nat}

def right_restores_index_full source · line 48 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(1n+depth, 31n) == True{} : Bool} -> @+bound:{U32.is_lt(index, capacity(1n+depth)) == True{} : Bool} -> @+choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {U32.to_nat(index) == Nat.add(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.extent(depth), U32.to_nat(U32.sub(index, capacity(depth)))) : Nat}

def right_stays_in_child_full source · line 58 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(1n+depth, 31n) == True{} : Bool} -> @+bound:{U32.is_lt(index, capacity(1n+depth)) == True{} : Bool} -> @+choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {U32.is_lt(U32.sub(index, capacity(depth)), capacity(depth)) == True{} : Bool}

def below_one_value source · line 69 · raw

@+index:U32 -> @bound:{U32.is_lt(index, 1) == True{} : Bool} -> {0n == U32.to_nat(index) : Nat}

def equal_values source · line 74 · raw

@+left:U32 -> @+right:U32 -> @equation:{U32.to_nat(left) == U32.to_nat(right) : Nat} -> {left == right : U32}

def equal_words source · line 79 · raw

@+left:U32 -> @+right:U32 -> @equation:{U32.is_eq(left, right) == True{} : Bool} -> {left == right : U32}

def unequal_words source · line 84 · raw

@+left:U32 -> @+right:U32 -> @different:{U32.is_eq(left, right) == False{} : Bool} -> @equal:{left == right : U32} -> Empty

def subtract_compared source · line 90 · raw

@+left:U32 -> @+right:U32 -> @+offset:U32 -> @equal:Bool -> @compared:{U32.is_eq(U32.sub(left, offset), U32.sub(right, offset)) == equal : Bool} -> @different:{U32.is_eq(left, right) == False{} : Bool} -> {equal == False{} : Bool}

def subtract_distinct source · line 102 · raw

@+left:U32 -> @+right:U32 -> @+offset:U32 -> @different:{U32.is_eq(left, right) == False{} : Bool} -> {U32.is_eq(U32.sub(left, offset), U32.sub(right, offset)) == False{} : Bool}

def child_limit source · line 107 · raw

@+depth:Nat -> @limit:{Nat.is_le(1n+depth, 30n) == True{} : Bool} -> {Nat.is_le(depth, 30n) == True{} : Bool}

Existing allocation proofs use the smaller, 30-bit allocation limit.

def right_restores_index source · line 110 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(1n+depth, 30n) == True{} : Bool} -> @+bound:{U32.is_lt(index, capacity(1n+depth)) == True{} : Bool} -> @+choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {U32.to_nat(index) == Nat.add(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.extent(depth), U32.to_nat(U32.sub(index, capacity(depth)))) : Nat}

def right_stays_in_child source · line 114 · raw

@+depth:Nat -> @+index:U32 -> @+limit:{Nat.is_le(1n+depth, 30n) == True{} : Bool} -> @+bound:{U32.is_lt(index, capacity(1n+depth)) == True{} : Bool} -> @+choice:{U32.is_lt(index, capacity(depth)) == False{} : Bool} -> {U32.is_lt(U32.sub(index, capacity(depth)), capacity(depth)) == True{} : Bool}