1	# Machine address bounds for balanced storage, independent of element values.
2	import Base
3	import ./storage_shape.bend as Shape
4	import ./natural_addition.bend as Addition
5	import ./word_encoding.bend as WordEncoding
6	import ./word_power_of_two.bend as Power
7	import ./nat_order.bend as Order
8	import ./nat_to_u32_bounds.bend as Bounds
9	import ./u32_comparison.bend as Comparison
10	import ./bounded_u32_arithmetic.bend as Arithmetic
11	import ./word_subtraction.bend as Subtraction
12	
13	def capacity(depth: Nat) -> U32:
14	  U32.shln(1,depth)
15	
16	def shift_extent(depth: Nat) -> {WordEncoding.shift(depth,1n) == Shape.extent(depth) : Nat}:
17	  match depth:
18	    case 0n: {==}
19	    case 1n+rest:
20	      Equal.cong(Nat,Nat,Nat.double,WordEncoding.shift(rest,1n),Shape.extent(rest),shift_extent(rest))
21	
22	def capacity_value(+depth: Nat,limit: {Nat.is_le(depth,31n) == True{} : Bool}) ->
23	  {U32.to_nat(capacity(depth)) == Shape.extent(depth) : Nat}:
24	  %Equal.sym(U32,capacity(depth),U32{Power.power(32n,depth)},Power.native_power(depth)) : {U32.to_nat(_) == Shape.extent(depth) : Nat}
25	  Equal.trans(Nat,Word.to_nat(32n,Power.power(32n,depth)),WordEncoding.shift(depth,1n),Shape.extent(depth),
26	    Power.power_value(32n,depth,Order.lt_succ(depth,31n,limit)),shift_extent(depth))
27	
28	def natural_bound(+depth: Nat,+index: U32,+limit: {Nat.is_le(depth,31n) == True{} : Bool},bound: {U32.is_lt(index,capacity(depth)) == True{} : Bool}) ->
29	  {Nat.is_lt(U32.to_nat(index),Shape.extent(depth)) == True{} : Bool}:
30	  %capacity_value(depth,limit) : {Nat.is_lt(U32.to_nat(index),_) == True{} : Bool}
31	  Bounds.as_nat_lt(index,capacity(depth),bound)
32	
33	def child_limit_full(+depth: Nat,limit: {Nat.is_le(1n+depth,31n) == True{} : Bool}) -> {Nat.is_le(depth,31n) == True{} : Bool}:
34	  Bounds.strict_le(depth,31n,Bounds.predecessor_strict(depth,31n,limit))
35	
36	def right_order(+depth: Nat,+index: U32,choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) ->
37	  {Nat.is_le(U32.to_nat(capacity(depth)),U32.to_nat(index)) == True{} : Bool}:
38	  Order.ge_true(U32.to_nat(index),U32.to_nat(capacity(depth)),Order.comparison_not_less(Nat.cmp(U32.to_nat(index),U32.to_nat(capacity(depth))),
39	    %Comparison.lt(index,capacity(depth)) : {_ == False{} : Bool}
40	    choice))
41	
42	def sub_value(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,31n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
43	  choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.to_nat((index - capacity(depth) : U32)) == Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))) : Nat}:
44	  Arithmetic.subtract(index,capacity(depth),capacity(1n+depth),Power.native_power_bound(1n+depth,limit),right_order(depth,index,choice),
45	    Order.transitive(Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),U32.to_nat(index),U32.to_nat(capacity(1n+depth)),
46	      Order.sub_le(U32.to_nat(index),U32.to_nat(capacity(depth))),Bounds.strict_le(U32.to_nat(index),U32.to_nat(capacity(1n+depth)),Bounds.as_nat_lt(index,capacity(1n+depth),bound))))
47	
48	def right_restores_index_full(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,31n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
49	  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.to_nat(index) == Nat.add(Shape.extent(depth),U32.to_nat((index - capacity(depth) : U32))) : Nat}:
50	  %Equal.sym(Nat,U32.to_nat((index - capacity(depth) : U32)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),sub_value(depth,index,limit,bound,choice)) :
51	    {U32.to_nat(index) == Nat.add(Shape.extent(depth),_) : Nat}
52	  %capacity_value(depth,child_limit_full(depth,limit)) : {U32.to_nat(index) == Nat.add(_,Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth)))) : Nat}
53	  Equal.sym(Nat,Nat.add(U32.to_nat(capacity(depth)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth)))),U32.to_nat(index),
54	    Equal.trans(Nat,Nat.add(U32.to_nat(capacity(depth)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth)))),
55	      Nat.add(Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),U32.to_nat(capacity(depth))),U32.to_nat(index),
56	      Order.commutative(U32.to_nat(capacity(depth)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth)))),Subtraction.restore(U32.to_nat(index),U32.to_nat(capacity(depth)),right_order(depth,index,choice))))
57	
58	def right_stays_in_child_full(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,31n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
59	  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.is_lt((index - capacity(depth) : U32),capacity(depth)) == True{} : Bool}:
60	  %Equal.sym(Bool,U32.is_lt((index - capacity(depth) : U32),capacity(depth)),Nat.is_lt(U32.to_nat((index - capacity(depth) : U32)),U32.to_nat(capacity(depth))),Comparison.lt((index - capacity(depth) : U32),capacity(depth))) : {_ == True{} : Bool}
61	  %Equal.sym(Nat,U32.to_nat((index - capacity(depth) : U32)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),sub_value(depth,index,limit,bound,choice)) :
62	    {Nat.is_lt(_,U32.to_nat(capacity(depth))) == True{} : Bool}
63	  Order.sub_lt(U32.to_nat(index),U32.to_nat(capacity(depth)),U32.to_nat(capacity(depth)),right_order(depth,index,choice),
64	    %Equal.sym(Nat,U32.to_nat(capacity(depth)),Shape.extent(depth),capacity_value(depth,child_limit_full(depth,limit))) :
65	      {Nat.is_lt(U32.to_nat(index),Nat.add(_,_)) == True{} : Bool}
66	    %Equal.sym(Nat,Nat.add(Shape.extent(depth),Shape.extent(depth)),Nat.double(Shape.extent(depth)),Addition.double(Shape.extent(depth))) : {Nat.is_lt(U32.to_nat(index),_) == True{} : Bool}
67	    natural_bound(1n+depth,index,limit,bound))
68	
69	def below_one_value(+index: U32,bound: {U32.is_lt(index,1) == True{} : Bool}) -> {0n == U32.to_nat(index) : Nat}:
70	  U32{+word} = index
71	  %Equal.sym(Word(32n),word,Word.zero(32n),WordEncoding.below_one_zero(31n,word,bound)) : {0n == Word.to_nat(32n,_) : Nat}
72	  {==}
73	
74	def unequal_words(+left: U32,+right: U32,different: {U32.is_eq(left,right) == False{} : Bool},equal: {left == right : U32}) -> Empty:
75	  WordEncoding.false_true(Equal.trans(Bool,False{},U32.is_eq(left,right),True{},Equal.sym(Bool,U32.is_eq(left,right),False{},different),
76	    %equal : {U32.is_eq(left,_) == True{} : Bool}
77	    %Equal.sym(Bool,U32.is_eq(left,left),Nat.is_eq(U32.to_nat(left),U32.to_nat(left)),Comparison.eq(left,left)) : {_ == True{} : Bool}
78	    Order.equal_reflexive(U32.to_nat(left))))
79	
80	def subtract_compared(+left: U32,+right: U32,+offset: U32,equal: Bool,
81	  compared: {U32.is_eq((left - offset : U32),(right - offset : U32)) == equal : Bool},different: {U32.is_eq(left,right) == False{} : Bool}) -> {equal == False{} : Bool}:
82	  match equal:
83	    case False{}: {==}
84	    case True{}:
85	      Empty.absurd({True{} == False{} : Bool},unequal_words(left,right,different,
86	        Equal.trans(U32,left,((left - offset : U32) + offset : U32),right,
87	          Equal.sym(U32,((left - offset : U32) + offset : U32),left,Subtraction.add_subtract(left,offset)),
88	          Equal.trans(U32,((left - offset : U32) + offset : U32),((right - offset : U32) + offset : U32),right,
89	            Equal.cong(U32,U32,value => (value + offset : U32),(left - offset : U32),(right - offset : U32),Arithmetic.equal_of_is_eq((left - offset : U32),(right - offset : U32),compared)),
90	            Subtraction.add_subtract(right,offset)))))
91	
92	def subtract_distinct(+left: U32,+right: U32,+offset: U32,different: {U32.is_eq(left,right) == False{} : Bool}) ->
93	  {U32.is_eq((left - offset : U32),(right - offset : U32)) == False{} : Bool}:
94	  subtract_compared(left,right,offset,U32.is_eq((left - offset : U32),(right - offset : U32)),{==},different)
95	
96	# Existing allocation proofs use the smaller, 30-bit allocation limit.
97	def child_limit(+depth: Nat,limit: {Nat.is_le(1n+depth,30n) == True{} : Bool}) -> {Nat.is_le(depth,30n) == True{} : Bool}:
98	  Bounds.strict_le(depth,30n,Bounds.predecessor_strict(depth,30n,limit))
99	
100	def right_restores_index(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,30n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
101	  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.to_nat(index) == Nat.add(Shape.extent(depth),U32.to_nat((index - capacity(depth) : U32))) : Nat}:
102	  right_restores_index_full(depth,index,Order.successor(1n+depth,30n,limit),bound,choice)
103	
104	def right_stays_in_child(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,30n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
105	  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.is_lt((index - capacity(depth) : U32),capacity(depth)) == True{} : Bool}:
106	  right_stays_in_child_full(depth,index,Order.successor(1n+depth,30n,limit),bound,choice)