def few_rounds

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:240

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/nat_division.bend as Division
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

240def few_rounds(~Context: Data,~map: Context -> F32 -> F32,+count: Nat,small: {Nat.is_lt(count,8n) == True{} : Bool}) -> rounds_property(~Context,~map,count):
241  match count:
242    case 0n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
243      few(~Context,~map,0n,U32.from_nat(start),slot,context,values,scratch)
244    case 1n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
245      few(~Context,~map,1n,U32.from_nat(start),slot,context,values,scratch)
246    case 2n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
247      few(~Context,~map,2n,U32.from_nat(start),slot,context,values,scratch)
248    case 3n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
249      few(~Context,~map,3n,U32.from_nat(start),slot,context,values,scratch)
250    case 4n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
251      few(~Context,~map,4n,U32.from_nat(start),slot,context,values,scratch)
252    case 5n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
253      few(~Context,~map,5n,U32.from_nat(start),slot,context,values,scratch)
254    case 6n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
255      few(~Context,~map,6n,U32.from_nat(start),slot,context,values,scratch)
256    case 7n: start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
257      few(~Context,~map,7n,U32.from_nat(start),slot,context,values,scratch)
258    case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
259      start => slot => context => values => scratch => depth => capacity => capacity_equal => balanced => limit => capacity_ok => room =>
260      Empty.absurd({Lanes.rounds(~Context,~map,8n+rest,Cells.State{Tree.pack(F32,values),Tree.pack(Tile.Tile8,scratch),U32.from_nat(start),slot,context}) ==
261    Tree.pack(F32,MapReadback.run(~F32,~Context,~map,8n+rest,U32.from_nat(start),context,values)) : Array<F32>},
262        WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(rest,0n),True{},Equal.sym(Bool,Nat.is_lt(rest,0n),False{},Division.lt_zero(rest)),small)))