def capacity_value

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:22

import Base
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

22def capacity_value(+depth: Nat,limit: {Nat.is_le(depth,31n) == True{} : Bool}) ->
23  {U32.to_nat(capacity(depth)) == Shape.extent(depth) : Nat}:
24  %Equal.sym(U32,capacity(depth),U32{Power.power(32n,depth)},Power.native_power(depth)) : {U32.to_nat(_) == Shape.extent(depth) : Nat}
25  Equal.trans(Nat,Word.to_nat(32n,Power.power(32n,depth)),WordEncoding.shift(depth,1n),Shape.extent(depth),
26    Power.power_value(32n,depth,Order.lt_succ(depth,31n,limit)),shift_extent(depth))