stelliferous@0.0.2.0 checks

0x9be3b13bf249759bc81e1958bcd1a4c0

One clock assumption, 2.5 GHz (0.4 ns per cycle), prices both vector MACs

stelliferous@0.0.2.0 by Kaz9487

Published

2026-10-10

Size

972,336 bytes, 109 files

License

MIT OR Apache-2.0 (LICENSE)

Declarations

80 laws (80 proved), 1858 defs, 148 types

Import

import stelliferous@0.0.2.0/default_kernel_cost.bend as Default_kernel_cost
import 0x9be3b13bf249759bc81e1958bcd1a4c0/default_kernel_cost.bend as Default_kernel_cost
import stelliferous@0.0.2.0/default_machine_limits.bend as Default_machine_limits
import 0x9be3b13bf249759bc81e1958bcd1a4c0/default_machine_limits.bend as Default_machine_limits
import stelliferous@0.0.2.0/kernel_band_pipeline.bend as Kernel_band_pipeline
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_band_pipeline.bend as Kernel_band_pipeline
import stelliferous@0.0.2.0/kernel_band_planning.bend as Kernel_band_planning
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_band_planning.bend as Kernel_band_planning
import stelliferous@0.0.2.0/kernel_block.bend as Kernel_block
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_block.bend as Kernel_block
import stelliferous@0.0.2.0/kernel_cost.bend as Kernel_cost
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_cost.bend as Kernel_cost
import stelliferous@0.0.2.0/kernel_gather.bend as Kernel_gather
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather.bend as Kernel_gather
import stelliferous@0.0.2.0/kernel_gather_buffer.bend as Kernel_gather_buffer
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gather_buffer.bend as Kernel_gather_buffer
import stelliferous@0.0.2.0/kernel_gemm.bend as Kernel_gemm
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm.bend as Kernel_gemm
import stelliferous@0.0.2.0/kernel_gemm_buffer.bend as Kernel_gemm_buffer
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_gemm_buffer.bend as Kernel_gemm_buffer
import stelliferous@0.0.2.0/kernel_packing_buffer.bend as Kernel_packing_buffer
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_buffer.bend as Kernel_packing_buffer
import stelliferous@0.0.2.0/kernel_packing_samples.bend as Kernel_packing_samples
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_packing_samples.bend as Kernel_packing_samples
import stelliferous@0.0.2.0/kernel_pipeline.bend as Kernel_pipeline
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_pipeline.bend as Kernel_pipeline
import stelliferous@0.0.2.0/kernel_planning.bend as Kernel_planning
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_planning.bend as Kernel_planning
import stelliferous@0.0.2.0/kernel_rows.bend as Kernel_rows
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_rows.bend as Kernel_rows
import stelliferous@0.0.2.0/kernel_shape.bend as Kernel_shape
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_shape.bend as Kernel_shape
import stelliferous@0.0.2.0/kernel_spatial_packing.bend as Kernel_spatial_packing
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_spatial_packing.bend as Kernel_spatial_packing
import stelliferous@0.0.2.0/kernel_tile.bend as Kernel_tile
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_tile.bend as Kernel_tile
import stelliferous@0.0.2.0/kernel_weights.bend as Kernel_weights
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_weights.bend as Kernel_weights
import stelliferous@0.0.2.0/kernel_window.bend as Kernel_window
import 0x9be3b13bf249759bc81e1958bcd1a4c0/kernel_window.bend as Kernel_window
import stelliferous@0.0.2.0/machine_limits.bend as Machine_limits
import 0x9be3b13bf249759bc81e1958bcd1a4c0/machine_limits.bend as Machine_limits
import stelliferous@0.0.2.0/math_activation.bend as Math_activation
import 0x9be3b13bf249759bc81e1958bcd1a4c0/math_activation.bend as Math_activation
import stelliferous@0.0.2.0/math_checked_word.bend as Math_checked_word
import 0x9be3b13bf249759bc81e1958bcd1a4c0/math_checked_word.bend as Math_checked_word
import stelliferous@0.0.2.0/math_compare.bend as Math_compare
import 0x9be3b13bf249759bc81e1958bcd1a4c0/math_compare.bend as Math_compare
import stelliferous@0.0.2.0/math_fp32.bend as Math_fp32
import 0x9be3b13bf249759bc81e1958bcd1a4c0/math_fp32.bend as Math_fp32
import stelliferous@0.0.2.0/math_sequence.bend as Math_sequence
import 0x9be3b13bf249759bc81e1958bcd1a4c0/math_sequence.bend as Math_sequence
import stelliferous@0.0.2.0/proofs/binary_digit.bend as Binary_digit
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_digit.bend as Binary_digit
import stelliferous@0.0.2.0/proofs/binary_division.bend as Binary_division
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/binary_division.bend as Binary_division
import stelliferous@0.0.2.0/proofs/boolean_logic.bend as Boolean_logic
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/boolean_logic.bend as Boolean_logic
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Bounded_u32_arithmetic
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/bounded_u32_arithmetic.bend as Bounded_u32_arithmetic
import stelliferous@0.0.2.0/proofs/kernel_gather_certificate.bend as Kernel_gather_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_gather_certificate.bend as Kernel_gather_certificate
import stelliferous@0.0.2.0/proofs/kernel_gemm_certificate.bend as Kernel_gemm_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_gemm_certificate.bend as Kernel_gemm_certificate
import stelliferous@0.0.2.0/proofs/kernel_packing_certificate.bend as Kernel_packing_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_certificate.bend as Kernel_packing_certificate
import stelliferous@0.0.2.0/proofs/kernel_packing_read_witness.bend as Kernel_packing_read_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_read_witness.bend as Kernel_packing_read_witness
import stelliferous@0.0.2.0/proofs/kernel_packing_witness.bend as Kernel_packing_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_packing_witness.bend as Kernel_packing_witness
import stelliferous@0.0.2.0/proofs/kernel_read_witness.bend as Kernel_read_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_read_witness.bend as Kernel_read_witness
import stelliferous@0.0.2.0/proofs/kernel_tile_witness.bend as Kernel_tile_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_tile_witness.bend as Kernel_tile_witness
import stelliferous@0.0.2.0/proofs/kernel_weights_certificate.bend as Kernel_weights_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_weights_certificate.bend as Kernel_weights_certificate
import stelliferous@0.0.2.0/proofs/kernel_weights_witness.bend as Kernel_weights_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/kernel_weights_witness.bend as Kernel_weights_witness
import stelliferous@0.0.2.0/proofs/loop_projection.bend as Loop_projection
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/loop_projection.bend as Loop_projection
import stelliferous@0.0.2.0/proofs/nat_division.bend as Nat_division
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_division.bend as Nat_division
import stelliferous@0.0.2.0/proofs/nat_extrema.bend as Nat_extrema
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_extrema.bend as Nat_extrema
import stelliferous@0.0.2.0/proofs/nat_interval.bend as Nat_interval
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_interval.bend as Nat_interval
import stelliferous@0.0.2.0/proofs/nat_order.bend as Nat_order
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_order.bend as Nat_order
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Nat_to_u32_bounds
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/nat_to_u32_bounds.bend as Nat_to_u32_bounds
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Natural_addition
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/natural_addition.bend as Natural_addition
import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as Storage_address_bounds
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_address_bounds.bend as Storage_address_bounds
import stelliferous@0.0.2.0/proofs/storage_allocation_refinement.bend as Storage_allocation_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_allocation_refinement.bend as Storage_allocation_refinement
import stelliferous@0.0.2.0/proofs/storage_buffer_model.bend as Storage_buffer_model
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_buffer_model.bend as Storage_buffer_model
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Storage_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_certificate.bend as Storage_certificate
import stelliferous@0.0.2.0/proofs/storage_clone_certificate.bend as Storage_clone_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_clone_certificate.bend as Storage_clone_certificate
import stelliferous@0.0.2.0/proofs/storage_readback.bend as Storage_readback
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_readback.bend as Storage_readback
import stelliferous@0.0.2.0/proofs/storage_refinement.bend as Storage_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_refinement.bend as Storage_refinement
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Storage_shape
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_shape.bend as Storage_shape
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Storage_tree_model
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_tree_model.bend as Storage_tree_model
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Storage_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/storage_witness.bend as Storage_witness
import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as Tensor_access_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/tensor_access_certificate.bend as Tensor_access_certificate
import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as Tensor_cursor_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/tensor_cursor_witness.bend as Tensor_cursor_witness
import stelliferous@0.0.2.0/proofs/tensor_indexed_certificate.bend as Tensor_indexed_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/tensor_indexed_certificate.bend as Tensor_indexed_certificate
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as Traversal_array_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_array_refinement.bend as Traversal_array_refinement
import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as Traversal_batch_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_batch_refinement.bend as Traversal_batch_refinement
import stelliferous@0.0.2.0/proofs/traversal_cells_refinement.bend as Traversal_cells_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_cells_refinement.bend as Traversal_cells_refinement
import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as Traversal_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_certificate.bend as Traversal_certificate
import stelliferous@0.0.2.0/proofs/traversal_lanes_certificate.bend as Traversal_lanes_certificate
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_lanes_certificate.bend as Traversal_lanes_certificate
import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as Traversal_lanes_refinement
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_lanes_refinement.bend as Traversal_lanes_refinement
import stelliferous@0.0.2.0/proofs/traversal_lanes_witness.bend as Traversal_lanes_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_lanes_witness.bend as Traversal_lanes_witness
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as Traversal_map_readback
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_map_readback.bend as Traversal_map_readback
import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as Traversal_visit_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_visit_witness.bend as Traversal_visit_witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as Traversal_witness
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/traversal_witness.bend as Traversal_witness
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as U32_comparison
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.bend as U32_comparison
import stelliferous@0.0.2.0/proofs/u32_division.bend as U32_division
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_division.bend as U32_division
import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32_shift
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_shift.bend as U32_shift
import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32_successor
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_successor.bend as U32_successor
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as Word_arithmetic
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_arithmetic.bend as Word_arithmetic
import stelliferous@0.0.2.0/proofs/word_encoding.bend as Word_encoding
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.bend as Word_encoding
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Word_multiplication
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_multiplication.bend as Word_multiplication
import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Word_power_of_two
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_power_of_two.bend as Word_power_of_two
import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Word_subtraction
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_subtraction.bend as Word_subtraction
import stelliferous@0.0.2.0/proofs/word_width.bend as Word_width
import 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_width.bend as Word_width
import stelliferous@0.0.2.0/storage_allocation.bend as Storage_allocation
import 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_allocation.bend as Storage_allocation
import stelliferous@0.0.2.0/storage_buffer.bend as Storage_buffer
import 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_buffer.bend as Storage_buffer
import stelliferous@0.0.2.0/storage_clone.bend as Storage_clone
import 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_clone.bend as Storage_clone
import stelliferous@0.0.2.0/storage_copy.bend as Storage_copy
import 0x9be3b13bf249759bc81e1958bcd1a4c0/storage_copy.bend as Storage_copy
import stelliferous@0.0.2.0/tensor.bend as Tensor
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor.bend as Tensor
import stelliferous@0.0.2.0/tensor_access.bend as Tensor_access
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_access.bend as Tensor_access
import stelliferous@0.0.2.0/tensor_band.bend as Tensor_band
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_band.bend as Tensor_band
import stelliferous@0.0.2.0/tensor_band_concat.bend as Tensor_band_concat
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_band_concat.bend as Tensor_band_concat
import stelliferous@0.0.2.0/tensor_band_pool.bend as Tensor_band_pool
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_band_pool.bend as Tensor_band_pool
import stelliferous@0.0.2.0/tensor_band_schedule.bend as Tensor_band_schedule
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_band_schedule.bend as Tensor_band_schedule
import stelliferous@0.0.2.0/tensor_band_window.bend as Tensor_band_window
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_band_window.bend as Tensor_band_window
import stelliferous@0.0.2.0/tensor_convolution.bend as Tensor_convolution
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_convolution.bend as Tensor_convolution
import stelliferous@0.0.2.0/tensor_cursor.bend as Tensor_cursor
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_cursor.bend as Tensor_cursor
import stelliferous@0.0.2.0/tensor_f32.bend as Tensor_f32
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_f32.bend as Tensor_f32
import stelliferous@0.0.2.0/tensor_file.bend as Tensor_file
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_file.bend as Tensor_file
import stelliferous@0.0.2.0/tensor_indexed.bend as Tensor_indexed
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_indexed.bend as Tensor_indexed
import stelliferous@0.0.2.0/tensor_lanes.bend as Tensor_lanes
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_lanes.bend as Tensor_lanes
import stelliferous@0.0.2.0/tensor_layout.bend as Tensor_layout
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_layout.bend as Tensor_layout
import stelliferous@0.0.2.0/tensor_model.bend as Tensor_model
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_model.bend as Tensor_model
import stelliferous@0.0.2.0/tensor_operations.bend as Tensor_operations
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_operations.bend as Tensor_operations
import stelliferous@0.0.2.0/tensor_select.bend as Tensor_select
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_select.bend as Tensor_select
import stelliferous@0.0.2.0/tensor_shape.bend as Tensor_shape
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_shape.bend as Tensor_shape
import stelliferous@0.0.2.0/tensor_view.bend as Tensor_view
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_view.bend as Tensor_view
import stelliferous@0.0.2.0/tensor_window.bend as Tensor_window
import 0x9be3b13bf249759bc81e1958bcd1a4c0/tensor_window.bend as Tensor_window
import stelliferous@0.0.2.0/traversal_array.bend as Traversal_array
import 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_array.bend as Traversal_array
import stelliferous@0.0.2.0/traversal_cells.bend as Traversal_cells
import 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_cells.bend as Traversal_cells
import stelliferous@0.0.2.0/traversal_lanes.bend as Traversal_lanes
import 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_lanes.bend as Traversal_lanes
import stelliferous@0.0.2.0/traversal_loop.bend as Traversal_loop
import 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_loop.bend as Traversal_loop
import stelliferous@0.0.2.0/traversal_partition.bend as Traversal_partition
import 0x9be3b13bf249759bc81e1958bcd1a4c0/traversal_partition.bend as Traversal_partition

Modules

• default_kernel_cost.bend 2 declarations — One clock assumption, 2.5 GHz (0.4 ns per cycle), prices both vector MACs
• default_machine_limits.bend 2 declarations — The original execution envelope, with every binary constraint checked here.
• kernel_band_pipeline.bend 15 declarations — Independent row bands keep their output owners. Fork distributes existing
• kernel_band_planning.bend 33 declarations — Row-layout costs follow the actual halo ranges and allocation capacities.
• kernel_block.bend 7 declarations
• kernel_cost.bend 4 declarations — Prediction parameters, not machine bounds or correctness certificates. The
• kernel_gather.bend 6 declarations
• kernel_gather_buffer.bend 1 declarations
• kernel_gemm.bend 35 declarations
• kernel_gemm_buffer.bend 6 declarations
• kernel_packing_buffer.bend 2 declarations
• kernel_packing_samples.bend 11 declarations — Pixel reads of an entry whose tile crosses an output row.
• kernel_pipeline.bend 40 declarations — Each leaf owns its input, packs it, and computes before returning. The caller
• kernel_planning.bend 45 declarations — Structural cost of the 4x8 pipeline. Only guarded dimensions enter here.
• kernel_rows.bend 9 declarations
• kernel_shape.bend 8 declarations — Natural dimensions at the validation boundary, before any machine narrowing.
• kernel_spatial_packing.bend 39 declarations — One packer for every output width. A tile holds eight consecutive output
• kernel_tile.bend 21 declarations — Measured flat FP32 tile representation; logical views stay out of hot loops.
• kernel_weights.bend 17 declarations
• kernel_window.bend 10 declarations — Input rows a spatial range reads. A window stores rows [first, first + rows)
• machine_limits.bend 15 declarations — Machine limits carry binary safety evidence. Nat proofs quantify over Limits
• math_activation.bend 38 declarations — FP32 activations, imported by callers as Act: Act.silu() is a value for
• math_checked_word.bend 9 declarations — Exact overflow-checked multiplication for metadata. Each Horner step starts
• math_compare.bend 29 declarations — IEEE comparisons expressed as 32-bit masks, including unordered inputs.
• math_fp32.bend 31 declarations — Ordered FP32 arithmetic on the shared sequence model. No separate container.
• math_sequence.bend 12 declarations, 2 laws — Element- and length-indexed sequence model. Random get is O(index);
• proofs/binary_digit.bend 1 declarations — The same binary-digit interpretation serves long division and division by two.
• proofs/binary_division.bend 22 declarations, 2 laws — Natural-number binary long division, proved against the frozen Base.divmod.
• proofs/boolean_logic.bend 13 declarations, 1 laws — Fold a sequence of conditions and recover any member by one induction.
• proofs/bounded_u32_arithmetic.bend 17 declarations — Machine operations -> unbounded Nat, with explicit no-overflow obligations.
• proofs/kernel_gather_certificate.bend 6 declarations
• proofs/kernel_gemm_certificate.bend 25 declarations — Shape evidence follows the real readers and writers. Only the final flat
• proofs/kernel_packing_certificate.bend 2 declarations
• proofs/kernel_packing_read_witness.bend 13 declarations
• proofs/kernel_packing_witness.bend 36 declarations — The packer hands back its input unchanged and keeps the witness of its
• proofs/kernel_read_witness.bend 7 declarations
• proofs/kernel_tile_witness.bend 7 declarations
• proofs/kernel_weights_certificate.bend 8 declarations
• proofs/kernel_weights_witness.bend 10 declarations
• proofs/loop_projection.bend 13 declarations — One induction for every state representation, output index and step count.
• proofs/nat_division.bend 11 declarations, 3 laws — Characterize Base.Nat.divmod by quotient/remainder and remainder bounds.
• proofs/nat_extrema.bend 18 declarations — Minimum and maximum laws used by interval intersection. Proofs follow the
• proofs/nat_interval.bend 7 declarations
• proofs/nat_order.bend 48 declarations
• proofs/nat_to_u32_bounds.bend 9 declarations, 1 laws — Safe Nat -> U32 -> Nat conversion over the candidate's finite envelope.
• proofs/natural_addition.bend 5 declarations, 5 laws — Shared natural-number addition laws; induction is on a symbolic operand.
• proofs/storage_address_bounds.bend 18 declarations — Machine address bounds for balanced storage, independent of element values.
• proofs/storage_allocation_refinement.bend 4 declarations
• proofs/storage_buffer_model.bend 36 declarations — Proof-only canonical owners retain the actual certificate. They support
• proofs/storage_certificate.bend 18 declarations — A flat live certificate: depth plus one equality word. Its equation identifies
• proofs/storage_clone_certificate.bend 3 declarations
• proofs/storage_readback.bend 14 declarations — Storage readback starts with the concrete native tree operations. These
• proofs/storage_refinement.bend 41 declarations, 10 laws
• proofs/storage_shape.bend 14 declarations, 1 laws — Shape invariants depend on tree structure, never on the stored element type.
• proofs/storage_tree_model.bend 13 declarations — Proof-only Data model of native arrays, parameterized by element type.
• proofs/storage_witness.bend 31 declarations, 1 laws — Structural proof data indexed by an erased affine owner. Runtime owners carry
• proofs/tensor_access_certificate.bend 48 declarations — Discharge the reader premises for the actual tensor traversal kernels.
• proofs/tensor_cursor_witness.bend 4 declarations
• proofs/tensor_indexed_certificate.bend 13 declarations
• proofs/traversal_array_refinement.bend 24 declarations — The same ownership-parameterized state is used by implementation and model.
• proofs/traversal_batch_refinement.bend 7 declarations — A batch writes the mapped values of consecutive positions after reading all
• proofs/traversal_cells_refinement.bend 9 declarations — One round of Cells.map on packed trees, for every element and cell type:
• proofs/traversal_certificate.bend 10 declarations — Flat certificates are updated once after a complete traversal. The witness
• proofs/traversal_lanes_certificate.bend 7 declarations — The live certificate of Lanes.map_when, and its refinement: with the cover
• proofs/traversal_lanes_refinement.bend 21 declarations — Lanes.map is Traversal.map_in_place: on a balanced array that holds its
• proofs/traversal_lanes_witness.bend 14 declarations — Shape evidence for Lanes.map: every round reads the values array, writes a
• proofs/traversal_map_readback.bend 14 declarations — Pointwise semantics of the actual ordered in-place map traversal. A bounded
• proofs/traversal_visit_witness.bend 13 declarations — Shape and owner preservation for traversals with consumed cursor state.
• proofs/traversal_witness.bend 35 declarations — Proof-only preservation of affine traversal owners. Reader values are handed
• proofs/u32_comparison.bend 8 declarations, 3 laws
• proofs/u32_division.bend 20 declarations, 2 laws — Actual Base.U32 long division -> the proven Nat binary division algorithm.
• proofs/u32_shift.bend 13 declarations, 1 laws
• proofs/u32_successor.bend 11 declarations, 7 laws
• proofs/word_arithmetic.bend 10 declarations, 5 laws — Modular arithmetic identities used before applying bounded Nat conversion.
• proofs/word_encoding.bend 25 declarations, 15 laws — General-width bit-vector arithmetic used by the native-address obligation.
• proofs/word_multiplication.bend 13 declarations, 2 laws
• proofs/word_power_of_two.bend 24 declarations, 17 laws — Power-of-two capacities and masks, by bit-width induction.
• proofs/word_subtraction.bend 6 declarations, 1 laws
• proofs/word_width.bend 2 declarations, 1 laws — Width transport changes the type index, never the stored bits.
• storage_allocation.bend 5 declarations — Keep the native allocation extent constant at each call site. With a dynamic
• storage_buffer.bend 16 declarations — Shared affine storage operations. Shape descriptors do not own another buffer.
• storage_clone.bend 2 declarations
• storage_copy.bend 1 declarations — Internal contiguous ranges. Callers establish bounds; the shared copy proof
• tensor.bend 111 declarations — Public tensors own dense row-major storage or image-row bands, their extents,
• tensor_access.bend 34 declarations — Internal tensor read layouts and unchecked traversal kernels.
• tensor_band.bend 85 declarations — Internal H-axis ownership. Offsets and spans are logical image rows, not
• tensor_band_concat.bend 32 declarations — Channel concatenation writes each input range directly into its final band.
• tensor_band_pool.bend 11 declarations — Each band leaf assembles the rows its outputs read into one contiguous
• tensor_band_schedule.bend 16 declarations — Conservative memory-work estimates for elementwise and layout operations.
• tensor_band_window.bend 24 declarations — Window geometry is independent of convolution arithmetic. Each output row
• tensor_convolution.bend 56 declarations — CHW / NCHW entry. Geometry and allocation checks finish before planning.
• tensor_cursor.bend 34 declarations — Least-significant axis first. Singleton axes are omitted. The two innermost
• tensor_f32.bend 102 declarations — The everyday F32 tensor module: import this one module and call F.add,
• tensor_file.bend 87 declarations — Raw little-endian FP32 files and NumPy .npy files through the official File effects.
• tensor_indexed.bend 17 declarations — Indexed mapping with a runtime context and a closed index template. The
• tensor_lanes.bend 28 declarations — Owned FP32 input bundles use the same Cells/Lanes rounds as unary maps.
• tensor_layout.bend 85 declarations — Layout operations consume their arguments. Copy and nearest upsampling
• tensor_model.bend 34 declarations — Models: a step computes with tensors it takes by name from a store, so a
• tensor_operations.bend 38 declarations — Checked operations preserve all owners and their balanced-storage certificates.
• tensor_select.bend 16 declarations — Three-input selection: shared shape/band helpers and the common lane loop.
• tensor_shape.bend 21 declarations — Storage-independent extents. View derives this descriptor from its axes.
• tensor_view.bend 47 declarations — Rank-independent forward-strided metadata. The Array owner is passed separately.
• tensor_window.bend 16 declarations — Two-dimensional pooling over the last two axes, as two ordered sweeps. Along
• traversal_array.bend 46 declarations — One owned read/transform/write traversal. Reader and address mapping are static
• traversal_cells.bend 7 declarations — Owned inputs move through cells holding `width` consecutive output values.
• traversal_lanes.bend 17 declarations — The FP32 cells of Cells.map: eight consecutive values as one Tile8.
• traversal_loop.bend 2 declarations — One sequential traversal for affine runtime owners and reusable proof states.
• traversal_partition.bend 5 declarations — A work partition is independent of its element representation and ownership.

Other files

• LICENSE 12,609 bytes

Dependencies

No imports from other hub packages.

Dependents

No package in this build imports it.

Status on bend 2.0.36