machine_limits.bend
stelliferous@0.0.3.0 · 66 lines · 0 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