def refines

stelliferous@0.0.2.0 · proofs/traversal_lanes_certificate.bend:27

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
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/traversal_lanes_refinement.bend as LanesLaws
import stelliferous@0.0.2.0/proofs/boolean_logic.bend as Boolean
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

27# The cover test of a balanced tree gives the bounds of the refinement.
28def refines(~Context: Data,~operation: Context -> F32 -> F32,+covered: Bool,+count: Nat,+position: U32,+context: Context,+values: Tree.Tree<F32>,+depth: Nat,
29  +balanced: Shape.Balanced(F32,depth,values),+guard: {Lanes.covered(depth,position,count) == covered : Bool}) ->
30  {Lanes.map_when(~Context,~operation,covered,count,position,context,Tree.pack(F32,values)) ==
31    Traversal.map_in_place(~F32,~Context,~operation,count,position,context,Tree.pack(F32,values)) : Array<F32>}:
32  match covered:
33    case False{}: {==}
34    case True{}:
35      +room = Nat.is_le(Nat.add(U32.to_nat(position),count),U32.to_nat(U32.shln(1,depth)))
36      %Arithmetic.native_roundtrip(position) :
37        {Lanes.map(~Context,~operation,count,_,context,Tree.pack(F32,values)) ==
38          Traversal.map_in_place(~F32,~Context,~operation,count,_,context,Tree.pack(F32,values)) : Array<F32>}
39      LanesLaws.map(~Context,~operation,count,U32.to_nat(position),context,values,depth,balanced,Boolean.left(Nat.is_le(depth,30n),room,guard),
40        Boolean.right(Nat.is_le(depth,30n),room,guard))