1	# Machine limits carry binary safety evidence. Nat proofs quantify over Limits
2	# rather than specializing their types to a large unary bound.
3	import Base
4	
5	def 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.
11	def native_nat_max() -> Word(48n):
12	  Word.not(48n,Word.zero(48n))
13	
14	def 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	
19	def extended_metadata_operand(value: U32) -> Word(48n):
20	  U32{bits} = value
21	  extend_metadata_word(32n,bits)
22	
23	def metadata_operand_max() -> Word(48n):
24	  extended_metadata_operand(word_max())
25	
26	def metadata_product_step_max() -> Word(48n):
27	  +maximum = metadata_operand_max()
28	  Word.add(48n,Word.add(48n,maximum,maximum),maximum)
29	
30	def metadata_product_step_fits() -> {Cmp.is_le(Word.cmp(48n,metadata_product_step_max(),native_nat_max())) == True{} : Bool}:
31	  {==}
32	
33	type 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	
52	type Limits is Data:
53	  Limits{dimension: U32,capacity: U32,coordinate: U32,half_word: U32,facts: Facts<dimension,capacity,coordinate,half_word>}
54	
55	def dimension(limits: Limits) -> U32:
56	  Limits{d,c,k,h,facts} = limits
57	  d
58	def capacity(limits: Limits) -> U32:
59	  Limits{d,c,k,h,facts} = limits
60	  c
61	def coordinate(limits: Limits) -> U32:
62	  Limits{d,c,k,h,facts} = limits
63	  k
64	def half_word(limits: Limits) -> U32:
65	  Limits{d,c,k,h,facts} = limits
66	  h