def outside_indexed

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:56

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_interval.bend as Interval

56def outside_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: Nat,+query: U32,+context: Context,+input: Tree.Tree<Element>,+depth: Nat,+capacity: U32,
57  +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
58  +capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},+room: {Nat.is_le(Nat.add(position,count),U32.to_nat(capacity)) == True{} : Bool},
59  +query_inside: {U32.is_lt(query,capacity) == True{} : Bool},+separate: Interval.Outside<position,count,U32.to_nat(query)>) ->
60  {Tree.read(Element,run_indexed(~Element,~Context,~operation,count,U32.from_nat(position),context,input),query) == Tree.read(Element,input,query) : Element}:
61  match count:
62    case 0n: {==}
63    case 1n+ +rest:
64      +value = operation(context,U32.from_nat(position),Tree.read(Element,input,U32.from_nat(position)))
65      +written = Tree.write(Element,input,U32.from_nat(position),value)
66      +position_inside = Order.room_index(position,rest,U32.to_nat(capacity),room)
67      +different = {
68        %Equal.sym(Bool,U32.is_eq(U32.from_nat(position),query),Nat.is_eq(U32.to_nat(U32.from_nat(position)),U32.to_nat(query)),Comparison.eq(U32.from_nat(position),query)) : {_ == False{} : Bool}
69        %Equal.sym(Nat,U32.to_nat(U32.from_nat(position)),position,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),position_inside))) :
70          {Nat.is_eq(_,U32.to_nat(query)) == False{} : Bool}
71        %Order.equal_symmetric(U32.to_nat(query),position) : {_ == False{} : Bool}
72        Interval.outside_head(position,rest,U32.to_nat(query),separate) : {U32.is_eq(U32.from_nat(position),query) == False{} : Bool}}
73      %Equal.sym(U32,(U32.from_nat(position) + 1 : U32),U32.from_nat(1n+position),Bounds.add_one(U32.from_nat(position))) :
74        {Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,_,context,written),query) == Tree.read(Element,input,query) : Element}
75      Equal.trans(Element,Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,U32.from_nat(1n+position),context,written),query),Tree.read(Element,written,query),Tree.read(Element,input,query),
76        outside_indexed(~Element,~Context,~operation,rest,1n+position,query,context,written,depth,capacity,
77          Equal.trans(U32,Tree.capacity(Element,written),Tree.capacity(Element,input),capacity,StorageReadback.write_capacity(~Element,input,U32.from_nat(position),value),capacity_equal),
78          Shape.write(Element,depth,input,U32.from_nat(position),value,balanced),limit,capacity_ok,Order.advance_room(position,rest,U32.to_nat(capacity),room),query_inside,
79          Interval.outside_tail(position,rest,U32.to_nat(query),separate)),
80        unchanged_full(~Element,depth,input,U32.from_nat(position),query,value,capacity,capacity_equal,balanced,limit,address_inside(position,capacity,capacity_ok,position_inside),query_inside,different))