~/jendhub

proofs/bounded_u32_arithmetic.bend

stelliferous@0.0.2.0 · 120 lines · 17 definitions

1# Machine operations -> unbounded Nat, with explicit no-overflow obligations.
2import Base
3import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
4import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication
5import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Subtraction
6import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
7import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
8import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
9import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
10
11def count_within(+count: U32,+length: Nat,+capacity: U32,+upper: U32,exact: {U32.to_nat(count) == length : Nat},
12  room: {Nat.is_le(length,U32.to_nat(capacity)) == True{} : Bool},capacity_bound: {U32.is_le(capacity,upper) == True{} : Bool}) ->
13  {U32.is_le(count,upper) == True{} : Bool}:
14  %Equal.sym(Bool,U32.is_le(count,upper),Nat.is_le(U32.to_nat(count),U32.to_nat(upper)),Comparison.le(count,upper)) : {_ == True{} : Bool}
15  %Equal.sym(Nat,U32.to_nat(count),length,exact) : {Nat.is_le(_,U32.to_nat(upper)) == True{} : Bool}
16  Order.transitive(length,U32.to_nat(capacity),U32.to_nat(upper),room,Bounds.as_nat_le(capacity,upper,capacity_bound))
17
18def native_roundtrip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
19  match a:
20    case U32{+w}:
21      %Equal.sym(U32,U32.from_nat(Word.to_nat(32n,w)),U32{WordArithmetic.encode(Word.to_nat(32n,w),32n)},
22        WordArithmetic.native_encoding(Word.to_nat(32n,w))) : {_ == U32{w} : U32}
23      %Equal.sym(Word(32n),WordArithmetic.encode(Word.to_nat(32n,w),32n),w,Multiplication.word_roundtrip(32n,w)) : {U32{_} == U32{w} : U32}
24      {==}
25
26def native_add(+a: U32,+b: U32) -> {U32.add(a,b) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}:
27  %native_roundtrip(a) : {U32.add(_,b) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}
28  %native_roundtrip(b) : {U32.add(U32.from_nat(U32.to_nat(a)),_) == U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))) : U32}
29  WordArithmetic.native_add(U32.to_nat(a),U32.to_nat(b))
30
31def add_zero(+value: U32) -> {(value + 0 : U32) == value : U32}:
32  %native_roundtrip(value) : {(value + 0 : U32) == _ : U32}
33  %Addition.zero_right(U32.to_nat(value)) : {(value + 0 : U32) == U32.from_nat(_) : U32}
34  native_add(value,0)
35
36def add_commutative(+left: U32,+right: U32) -> {(left + right : U32) == (right + left : U32) : U32}:
37  %Equal.sym(U32,(left + right : U32),U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))),native_add(left,right)) :
38    {_ == (right + left : U32) : U32}
39  %Equal.sym(U32,(right + left : U32),U32.from_nat(Nat.add(U32.to_nat(right),U32.to_nat(left))),native_add(right,left)) :
40    {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == _ : U32}
41  %Order.commutative(U32.to_nat(left),U32.to_nat(right)) :
42    {U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))) == U32.from_nat(_) : U32}
43  {==}
44
45def add_zero_left(+value: U32) -> {(0 + value : U32) == value : U32}:
46  Equal.trans(U32,(0 + value : U32),(value + 0 : U32),value,add_commutative(0,value),add_zero(value))
47
48def multiply_zero_left(+value: U32) -> {(0 * value : U32) == 0 : U32}:
49  Multiplication.native_multiply(0,value)
50
51# These are modular identities, so they require no no-overflow assumption.
52def encoded_add_associative(+a: Nat,+b: Nat,+c: Nat) ->
53  {((U32.from_nat(a) + U32.from_nat(b) : U32) + U32.from_nat(c) : U32) == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}:
54  %Equal.sym(U32,(U32.from_nat(a) + U32.from_nat(b) : U32),U32.from_nat(Nat.add(a,b)),WordArithmetic.native_add(a,b)) :
55    {(_ + U32.from_nat(c) : U32) == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}
56  %Equal.sym(U32,(U32.from_nat(Nat.add(a,b)) + U32.from_nat(c) : U32),U32.from_nat(Nat.add(Nat.add(a,b),c)),WordArithmetic.native_add(Nat.add(a,b),c)) :
57    {_ == (U32.from_nat(a) + (U32.from_nat(b) + U32.from_nat(c) : U32) : U32) : U32}
58  %Equal.sym(U32,(U32.from_nat(b) + U32.from_nat(c) : U32),U32.from_nat(Nat.add(b,c)),WordArithmetic.native_add(b,c)) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == (U32.from_nat(a) + _ : U32) : U32}
59  %Equal.sym(U32,(U32.from_nat(a) + U32.from_nat(Nat.add(b,c)) : U32),U32.from_nat(Nat.add(a,Nat.add(b,c))),WordArithmetic.native_add(a,Nat.add(b,c))) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == _ : U32}
60  %Addition.associative(a,b,c) : {U32.from_nat(Nat.add(Nat.add(a,b),c)) == U32.from_nat(_) : U32}
61  {==}
62
63def add_associative(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) + c : U32) == (a + (b + c : U32) : U32) : U32}:
64  %native_roundtrip(a) : {((_ + b : U32) + c : U32) == (_ + (b + c : U32) : U32) : U32}
65  %native_roundtrip(b) : {((U32.from_nat(U32.to_nat(a)) + _ : U32) + c : U32) == (U32.from_nat(U32.to_nat(a)) + (_ + c : U32) : U32) : U32}
66  %native_roundtrip(c) : {((U32.from_nat(U32.to_nat(a)) + U32.from_nat(U32.to_nat(b)) : U32) + _ : U32) == (U32.from_nat(U32.to_nat(a)) + (U32.from_nat(U32.to_nat(b)) + _ : U32) : U32) : U32}
67  encoded_add_associative(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c))
68
69def subtract_from_sum(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}:
70  %Subtraction.add_subtract(b,c) : {((a + _ : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}
71  %add_associative(a,(b - c : U32),c) : {(_ - c : U32) == (a + (b - c : U32) : U32) : U32}
72  Subtraction.subtract_add((a + (b - c : U32) : U32),c)
73
74def add_after_subtract(+value: U32,+padding: U32,+offset: U32) ->
75  {((value - padding : U32) + offset : U32) == ((value + offset : U32) - padding : U32) : U32}:
76  %Equal.sym(U32,((value - padding : U32) + offset : U32),(offset + (value - padding : U32) : U32),add_commutative((value - padding : U32),offset)) :
77    {_ == ((value + offset : U32) - padding : U32) : U32}
78  %add_commutative(offset,value) : {(offset + (value - padding : U32) : U32) == (_ - padding : U32) : U32}
79  Equal.sym(U32,((offset + value : U32) - padding : U32),(offset + (value - padding : U32) : U32),subtract_from_sum(offset,value,padding))
80
81def native_subtract(+a: U32,+b: U32,h: {Nat.is_le(U32.to_nat(b),U32.to_nat(a)) == True{} : Bool}) -> {U32.sub(a,
82    b) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}:
83  %native_roundtrip(a) : {U32.sub(_,b) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}
84  %native_roundtrip(b) : {U32.sub(U32.from_nat(U32.to_nat(a)),_) == U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))) : U32}
85  Subtraction.encoded_subtract(U32.to_nat(a),U32.to_nat(b),h)
86
87def add(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Nat.add(U32.to_nat(a),U32.to_nat(b)),
88      U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.add(a,b)) == Nat.add(U32.to_nat(a),U32.to_nat(b)) : Nat}:
89  %Equal.sym(U32,U32.add(a,b),U32.from_nat(Nat.add(U32.to_nat(a),U32.to_nat(b))),native_add(a,b)) : {U32.to_nat(_) == Nat.add(U32.to_nat(a),
90      U32.to_nat(b)) : Nat}
91  Bounds.roundtrip(Nat.add(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
92
93def subtract(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},ordered: {Nat.is_le(U32.to_nat(b),
94      U32.to_nat(a)) == True{} : Bool},h: {Nat.is_le(Nat.sub(U32.to_nat(a),U32.to_nat(b)),
95      U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.sub(a,b)) == Nat.sub(U32.to_nat(a),U32.to_nat(b)) : Nat}:
96  %Equal.sym(U32,U32.sub(a,b),U32.from_nat(Nat.sub(U32.to_nat(a),U32.to_nat(b))),native_subtract(a,b,
97      ordered)) : {U32.to_nat(_) == Nat.sub(U32.to_nat(a),U32.to_nat(b)) : Nat}
98  Bounds.roundtrip(Nat.sub(U32.to_nat(a),U32.to_nat(b)),cap,cap_ok,h)
99
100def remove_prefix(+value: U32,+base: U32,+local: Nat,+capacity: U32,capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
101  +exact: {U32.to_nat(value) == Nat.add(U32.to_nat(base),local) : Nat},room: {Nat.is_le(U32.to_nat(value),U32.to_nat(capacity)) == True{} : Bool}) ->
102  {U32.to_nat((value - base : U32)) == local : Nat}:
103  +local_room = Order.transitive(local,Nat.add(U32.to_nat(base),local),U32.to_nat(capacity),
104    %Order.commutative(local,U32.to_nat(base)) : {Nat.is_le(local,_) == True{} : Bool} Order.le_add(local,U32.to_nat(base)),
105    %exact : {Nat.is_le(_,U32.to_nat(capacity)) == True{} : Bool} room)
106  Equal.trans(Nat,U32.to_nat((value - base : U32)),Nat.sub(U32.to_nat(value),U32.to_nat(base)),local,
107    subtract(value,base,capacity,capacity_ok,
108      %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.is_le(U32.to_nat(base),_) == True{} : Bool} Order.le_add(U32.to_nat(base),local),
109      %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.is_le(Nat.sub(_,U32.to_nat(base)),U32.to_nat(capacity)) == True{} : Bool}
110      %Equal.sym(Nat,Nat.sub(Nat.add(U32.to_nat(base),local),U32.to_nat(base)),local,Order.subtract_shift(U32.to_nat(base),local)) : {Nat.is_le(_,U32.to_nat(capacity)) == True{} : Bool} local_room),
111    %Equal.sym(Nat,U32.to_nat(value),Nat.add(U32.to_nat(base),local),exact) : {Nat.sub(_,U32.to_nat(base)) == local : Nat} Order.subtract_shift(U32.to_nat(base),local))
112
113def subtract_zero(+value: U32) -> {(value - 0 : U32) == value : U32}:
114  Equal.trans(U32,(value - 0 : U32),U32.from_nat(Nat.sub(U32.to_nat(value),0n)),value,native_subtract(value,0,Order.zero_le(U32.to_nat(value))),
115    Equal.trans(U32,U32.from_nat(Nat.sub(U32.to_nat(value),0n)),U32.from_nat(U32.to_nat(value)),value,
116      Equal.cong(Nat,U32,U32.from_nat,Nat.sub(U32.to_nat(value),0n),U32.to_nat(value),Order.subtract_zero(U32.to_nat(value))),native_roundtrip(value)))
117
118def multiply(+a: U32,+b: U32,+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Nat.mul(U32.to_nat(a),U32.to_nat(b)),
119      U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32.mul(a,b)) == Nat.mul(U32.to_nat(a),U32.to_nat(b)) : Nat}:
120  Multiplication.bounded_multiply(a,b,cap,cap_ok,h)