machine_limits.bend

stelliferous@0.0.2.0 · 66 lines · 13 definitions

1# Machine limits carry binary safety evidence. Nat proofs quantify over Limits
2# rather than specializing their types to a large unary bound.
3import Base
4
5def word_max() -> U32:
6  4294967295
7
8# Official v2.0.26 native Nat payloads have 48 bits. Checked metadata products
9# keep each partial value <= U32.max; doubling it and adding a U32 operand is
10# at most 3*U32.max. Binary evidence avoids expanding these bounds in unary.
11def native_nat_max() -> Word(48n):
12  Word.not(48n,Word.zero(48n))
13
14def extend_metadata_word(width: Nat,word: Word(width)) -> Word(Nat.add(width,16n)):
15  match width word:
16    case 0n WNil{}: Word.zero(16n)
17    case 1n+rest WCon{bit,tail}: WCon{bit,extend_metadata_word(rest,tail)}
18
19def extended_metadata_operand(value: U32) -> Word(48n):
20  U32{bits} = value
21  extend_metadata_word(32n,bits)
22
23def metadata_operand_max() -> Word(48n):
24  extended_metadata_operand(word_max())
25
26def metadata_product_step_max() -> Word(48n):
27  +maximum = metadata_operand_max()
28  Word.add(48n,Word.add(48n,maximum,maximum),maximum)
29
30def metadata_product_step_fits() -> {Cmp.is_le(Word.cmp(48n,metadata_product_step_max(),native_nat_max())) == True{} : Bool}:
31  {==}
32
33type Facts<-d: U32,-c: U32,-k: U32,-h: U32> is Data:
34  Facts{
35    dimension_fits: {U32.is_le(d,2147483648) == True{} : Bool},
36    capacity_fits: {U32.is_le(c,2147483648) == True{} : Bool},
37    coordinate_fits: {U32.is_le(k,2147483648) == True{} : Bool},
38    half_word_fits: {U32.is_le(h,2147483648) == True{} : Bool},
39    dimension_allocatable: {U32.is_le(d,1073741824) == True{} : Bool},
40    capacity_allocatable: {U32.is_le(c,1073741824) == True{} : Bool},
41    dimension_below_half: {U32.is_lt(d,2147483648) == True{} : Bool},
42    capacity_below_half: {U32.is_lt(c,2147483648) == True{} : Bool},
43    dimension_within_capacity: {U32.is_le(d,c) == True{} : Bool},
44    dimension_within_coordinate: {U32.is_le(d,k) == True{} : Bool},
45    doubled_dimension_within_coordinate: {U32.is_le(U32.shl(d),k) == True{} : Bool},
46    capacity_doubles_to_half: {U32.shl(c) == h : U32},
47    seven_within_capacity: {U32.is_le(7,c) == True{} : Bool},
48    sixteen_within_half: {U32.is_le(16,h) == True{} : Bool},
49    capacity_within_half: {U32.is_le(c,h) == True{} : Bool}
50  }
51
52type Limits is Data:
53  Limits{dimension: U32,capacity: U32,coordinate: U32,half_word: U32,facts: Facts<dimension,capacity,coordinate,half_word>}
54
55def dimension(limits: Limits) -> U32:
56  Limits{d,c,k,h,facts} = limits
57  d
58def capacity(limits: Limits) -> U32:
59  Limits{d,c,k,h,facts} = limits
60  c
61def coordinate(limits: Limits) -> U32:
62  Limits{d,c,k,h,facts} = limits
63  k
64def half_word(limits: Limits) -> U32:
65  Limits{d,c,k,h,facts} = limits
66  h