StorageRefinement.stored_sequence_element: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_refinement.bend as StorageRefinement
Lines 374-389 of stelliferous@0.0.2.0/proofs/storage_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&start_line=374&end_line=389

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

# The unchecked primitive is usable after the caller establishes its logical
# index bound. This is independent of allocation shape and unused capacity.
def stored_sequence_element(~Element: Data,+fallback: Element,+length: Nat,+values: List<&2,Element>,
  +evidence: SequenceEvidence<Element,length,values>,+index: Nat,
  inside: {Nat.is_lt(index,length) == True{} : Bool}) ->
  {Tree.read(Element,sequence_storage(Element,length,values,evidence),U32.from_nat(index)) ==
    Maybe.default(&2,Element,List.get(&2,Element,values,index),fallback) : Element}:
  SequenceEvidence{+storage,+contents,room} = evidence
  %contents :
    {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,List.get(&2,Element,_,index),fallback) : Element}
  %Equal.sym(Maybe<&2,Element>,List.get(&2,Element,Tree.read_sequence(~Element,length,0,storage),index),
    Some{Tree.read(Element,storage,(0 + U32.from_nat(index) : U32))},sequence_element(~Element,length,0,storage,index,inside)) :
    {Tree.read(Element,storage,U32.from_nat(index)) == Maybe.default(&2,Element,_,fallback) : Element}
  %Equal.sym(U32,(0 + U32.from_nat(index) : U32),U32.from_nat(index),Arithmetic.add_zero_left(U32.from_nat(index))) :
    {Tree.read(Element,storage,U32.from_nat(index)) == Tree.read(Element,storage,_) : Element}
  {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&name=add_zero_left
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=SequenceEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=sequence_element
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_refinement.bend&name=sequence_storage
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=read_sequence