def sequence_lookup_case

stelliferous@0.0.2.0 · proofs/storage_refinement.bend:295

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
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

295def sequence_lookup_case(~Element: Data,+present: Bool,+length: U32,+tree: Tree.Tree<Element>,+index: U32,
296  order: {U32.is_lt(index,length) == present : Bool}) ->
297  {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
298    Bool.pick(Maybe<&2,Element>,present,Some{Tree.read(Element,tree,index)},None{}) : Maybe<&2,Element>}:
299  match present:
300    case False{}:
301      sequence_missing(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),
302        %Comparison.lt(index,length) : {_ == False{} : Bool}
303        order)
304    case True{}:
305      %Arithmetic.native_roundtrip(index) :
306        {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
307          Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
308      %Arithmetic.add_zero_left(U32.from_nat(U32.to_nat(index))) :
309        {List.get(&2,Element,Tree.read_sequence(~Element,U32.to_nat(length),0,tree),U32.to_nat(index)) ==
310          Some{Tree.read(Element,tree,_)} : Maybe<&2,Element>}
311      sequence_element(~Element,U32.to_nat(length),0,tree,U32.to_nat(index),
312        %Comparison.lt(index,length) : {_ == True{} : Bool}
313        order)