def stored_sequence_element

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:374

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

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