proofs/storage_address_bounds.bend
stelliferous@0.0.3.0 · 106 lines · 0 definitions
1# Machine address bounds for balanced storage, independent of element values.
2import Base
3import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
4import stelliferous@0.0.3.0/proofs/natural_addition.bend as Addition
5import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
6import stelliferous@0.0.3.0/proofs/word_power_of_two.bend as Power
7import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
8import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
9import stelliferous@0.0.3.0/proofs/u32_comparison.bend as Comparison
10import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
11import stelliferous@0.0.3.0/proofs/word_subtraction.bend as Subtraction
12
13def capacity(depth: Nat) -> U32:
14 U32.shln(1,depth)
15
16def 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
22def 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
28def 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
33def 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
36def 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
42def 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
48def 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
58def 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
69def 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
74def 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
80def 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
92def 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.
97def 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
100def 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
104def 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)