machine_limits.bend checks

raw source on the hub · import stelliferous@0.0.2.0/machine_limits.bend as Machine_limits

Machine limits carry binary safety evidence. Nat proofs quantify over Limits rather than specializing their types to a large unary bound.

1 import

import Base

Types

type Facts source · line 33 · raw

@-d:U32 -> @-c:U32 -> @-k:U32 -> @-h:U32 -> Data

Facts

@-d:U32 -> @-c:U32 -> @-k:U32 -> @-h:U32 -> @dimension_fits:{U32.is_le(d, 2147483648) == True{} : Bool} -> @capacity_fits:{U32.is_le(c, 2147483648) == True{} : Bool} -> @coordinate_fits:{U32.is_le(k, 2147483648) == True{} : Bool} -> @half_word_fits:{U32.is_le(h, 2147483648) == True{} : Bool} -> @dimension_allocatable:{U32.is_le(d, 1073741824) == True{} : Bool} -> @capacity_allocatable:{U32.is_le(c, 1073741824) == True{} : Bool} -> @dimension_below_half:{U32.is_lt(d, 2147483648) == True{} : Bool} -> @capacity_below_half:{U32.is_lt(c, 2147483648) == True{} : Bool} -> @dimension_within_capacity:{U32.is_le(d, c) == True{} : Bool} -> @dimension_within_coordinate:{U32.is_le(d, k) == True{} : Bool} -> @doubled_dimension_within_coordinate:{U32.is_le(U32.shl(d), k) == True{} : Bool} -> @capacity_doubles_to_half:{U32.shl(c) == h : U32} -> @seven_within_capacity:{U32.is_le(7, c) == True{} : Bool} -> @sixteen_within_half:{U32.is_le(16, h) == True{} : Bool} -> @capacity_within_half:{U32.is_le(c, h) == True{} : Bool} -> Facts<d, c, k, h>

type Limits source · line 52 · raw

Data

Limits

@dimension:U32 -> @capacity:U32 -> @coordinate:U32 -> @half_word:U32 -> @facts:Facts<dimension, capacity, coordinate, half_word> -> Limits

Definitions

def word_max source · line 5 · raw

U32

def native_nat_max source · line 11 · raw

Word(48n)

Official v2.0.26 native Nat payloads have 48 bits. Checked metadata products keep each partial value <= U32.max; doubling it and adding a U32 operand is at most 3*U32.max. Binary evidence avoids expanding these bounds in unary.

def extend_metadata_word source · line 14 · raw

@width:Nat -> @word:Word(width) -> Word(Nat.add(width, 16n))

def extended_metadata_operand source · line 19 · raw

@value:U32 -> Word(48n)

def metadata_operand_max source · line 23 · raw

Word(48n)

def metadata_product_step_max source · line 26 · raw

Word(48n)

def metadata_product_step_fits source · line 30 · raw

{Cmp.is_le(Word.cmp(48n, metadata_product_step_max, native_nat_max)) == True{} : Bool}

def dimension source · line 55 · raw

@limits:Limits -> U32

def capacity source · line 58 · raw

@limits:Limits -> U32

def coordinate source · line 61 · raw

@limits:Limits -> U32

def half_word source · line 64 · raw

@limits:Limits -> U32