def rounds_property

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:231

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/traversal_cells.bend as Cells
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback
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

231# Every count: whole rounds, then the last positions one by one.
232def rounds_property(~Context: Data,~map: Context -> F32 -> F32,count: Nat) -> Type:
233  @+start: Nat -> @+slot: U32 -> @+context: Context -> @+values: Tree.Tree<F32> -> @+scratch: Tree.Tree<Tile.Tile8> ->
234  @+depth: Nat -> @+capacity: U32 -> @+capacity_equal: {Tree.capacity(F32,values) == capacity : U32} -> @+balanced: Shape.Balanced(F32,depth,values) ->
235  @+limit: {Nat.is_le(depth,30n) == True{} : Bool} -> @+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool} ->
236  @+room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool} ->
237  {Lanes.rounds(~Context,~map,count,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
238    Tree.pack(F32,MapReadback.run(~F32,~Context,~map,count,U32.from_nat(start),context,values)) : Array<F32>}