proofs/u32_full_range.bend
stelliferous@0.0.3.0 · 114 lines · 0 definitions
1# Exact conversions over the complete U32 range. Tensor stride-zero extents may
2# exceed the physical array capacity, so storage-capacity bounds are insufficient.
3import Base
4import stelliferous@0.0.3.0/proofs/nat_order.bend as Order
5import stelliferous@0.0.3.0/proofs/u32_successor.bend as U32Successor
6import stelliferous@0.0.3.0/proofs/nat_to_u32_bounds.bend as Bounds
7import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
8import stelliferous@0.0.3.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
9import stelliferous@0.0.3.0/proofs/word_multiplication.bend as Multiplication
10
11def ones(width: Nat) -> Word(width):
12 match width:
13 case 0n: WNil{}
14 case 1n+rest: WCon{True{},ones(rest)}
15
16def equal_low_less(+comparison: Cmp) -> {Cmp.is_lt(Word.cmp.fin(True{},True{},comparison)) == Cmp.is_lt(comparison) : Bool}:
17 match comparison:
18 case LT{}: {==}
19 case EQ{}: {==}
20 case GT{}: {==}
21
22def finish_bounded(+bit: Bool,+comparison: Cmp,ordered: {Cmp.is_le(comparison) == True{} : Bool}) ->
23 {Cmp.is_le(Word.cmp.fin(bit,True{},comparison)) == True{} : Bool}:
24 match bit comparison:
25 case False{} LT{}: {==}
26 case False{} EQ{}: {==}
27 case False{} GT{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(ordered))
28 case True{} LT{}: {==}
29 case True{} EQ{}: {==}
30 case True{} GT{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(ordered))
31
32def bounded(+width: Nat,+word: Word(width)) -> {Cmp.is_le(Word.cmp(width,word,ones(width))) == True{} : Bool}:
33 match width:
34 case 0n: {==}
35 case 1n+ +rest:
36 WCon{bit,+tail} = word
37 finish_bounded(bit,Word.cmp(rest,tail,ones(rest)),bounded(rest,tail))
38
39def increment(+width: Nat,+word: Word(width),below: {Cmp.is_lt(Word.cmp(width,word,ones(width))) == True{} : Bool}) ->
40 {Word.to_nat(width,Word.inc(width,word)) == 1n+Word.to_nat(width,word) : Nat}:
41 match width:
42 case 0n: Empty.absurd({0n == 1n : Nat},WordEncoding.false_true(below))
43 case 1n+ +rest:
44 match word:
45 case WCon{False{},tail}: {==}
46 case WCon{True{},+tail}:
47 %increment(rest,tail,{
48 %equal_low_less(Word.cmp(rest,tail,ones(rest))) : {_ == True{} : Bool}
49 below : {Cmp.is_lt(Word.cmp(rest,tail,ones(rest))) == True{} : Bool}}) :
50 {Nat.double(Word.to_nat(rest,Word.inc(rest,tail))) == Nat.double(_) : Nat}
51 {==}
52
53def maximum(+value: U32) -> {U32.is_le(value,4294967295) == True{} : Bool}:
54 U32{+word} = value
55 bounded(32n,word)
56
57def successor(+value: U32,below: {U32.is_lt(value,4294967295) == True{} : Bool}) ->
58 {U32.to_nat(U32.add(value,1)) == 1n+U32.to_nat(value) : Nat}:
59 U32{+word} = value
60 %Equal.sym(Word(32n),Word.add(32n,word,Word.inc(32n,Word.zero(32n))),Word.inc(32n,word),U32Successor.add_one(32n,word)) :
61 {Word.to_nat(32n,_) == 1n+Word.to_nat(32n,word) : Nat}
62 increment(32n,word,below)
63
64def roundtrip(+value: Nat,+capacity: U32,inside: {Nat.is_le(value,U32.to_nat(capacity)) == True{} : Bool}) ->
65 {U32.to_nat(U32.from_nat(value)) == value : Nat}:
66 match value:
67 case 0n: {==}
68 case 1n+ +previous:
69 +below = Bounds.predecessor_strict(previous,U32.to_nat(capacity),inside)
70 +exact = roundtrip(previous,capacity,Bounds.strict_le(previous,U32.to_nat(capacity),below))
71 %exact : {U32.to_nat(U32.inc(U32.from_nat(previous))) == 1n+_ : Nat}
72 %Bounds.add_one(U32.from_nat(previous)) : {U32.to_nat(_) == 1n+U32.to_nat(U32.from_nat(previous)) : Nat}
73 successor(U32.from_nat(previous),Bounds.uint_trans(U32.from_nat(previous),capacity,4294967295,
74 Bounds.native_bound(previous,capacity,exact,below),maximum(capacity)))
75
76def add(+left: U32,+right: U32,+capacity: U32,
77 inside: {Nat.is_le(Nat.add(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
78 {U32.to_nat(U32.add(left,right)) == Nat.add(U32.to_nat(left),U32.to_nat(right)) : Nat}:
79 %Equal.sym(U32,U32.add(left,right),U32.from_nat(Nat.add(U32.to_nat(left),U32.to_nat(right))),Arithmetic.native_add(left,right)) :
80 {U32.to_nat(_) == Nat.add(U32.to_nat(left),U32.to_nat(right)) : Nat}
81 roundtrip(Nat.add(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
82
83def subtract(+left: U32,+right: U32,+capacity: U32,
84 ordered: {Nat.is_le(U32.to_nat(right),U32.to_nat(left)) == True{} : Bool},
85 inside: {Nat.is_le(Nat.sub(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
86 {U32.to_nat(U32.sub(left,right)) == Nat.sub(U32.to_nat(left),U32.to_nat(right)) : Nat}:
87 %Equal.sym(U32,U32.sub(left,right),U32.from_nat(Nat.sub(U32.to_nat(left),U32.to_nat(right))),Arithmetic.native_subtract(left,right,ordered)) :
88 {U32.to_nat(_) == Nat.sub(U32.to_nat(left),U32.to_nat(right)) : Nat}
89 roundtrip(Nat.sub(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
90
91def multiply(+left: U32,+right: U32,+capacity: U32,
92 inside: {Nat.is_le(Nat.mul(U32.to_nat(left),U32.to_nat(right)),U32.to_nat(capacity)) == True{} : Bool}) ->
93 {U32.to_nat(U32.mul(left,right)) == Nat.mul(U32.to_nat(left),U32.to_nat(right)) : Nat}:
94 %Equal.sym(U32,U32.mul(left,right),U32.from_nat(Nat.mul(U32.to_nat(left),U32.to_nat(right))),Multiplication.native_multiply(left,right)) :
95 {U32.to_nat(_) == Nat.mul(U32.to_nat(left),U32.to_nat(right)) : Nat}
96 roundtrip(Nat.mul(U32.to_nat(left),U32.to_nat(right)),capacity,inside)
97
98# Subtracting a common interval origin preserves its strict upper bound.
99def interval_inside(+low: U32,+high: U32,+position: U32,
100 +lower: {U32.is_le(low,position) == True{} : Bool},+upper: {U32.is_lt(position,high) == True{} : Bool}) ->
101 {Nat.is_lt(U32.to_nat((position - low : U32)),U32.to_nat((high - low : U32))) == True{} : Bool}:
102 +ln = U32.to_nat(low)
103 +hn = U32.to_nat(high)
104 +pn = U32.to_nat(position)
105 +ordered = Bounds.as_nat_le(low,position,lower)
106 +before = Bounds.as_nat_lt(position,high,upper)
107 +low_high = Order.le_lt_trans(ln,pn,hn,ordered,before)
108 +local = Nat.sub(pn,ln)
109 +relative_exact = subtract(position,low,position,ordered,Order.sub_le(pn,ln))
110 +range_exact = subtract(high,low,high,Bounds.strict_le(ln,hn,low_high),Order.sub_le(hn,ln))
111 %Equal.sym(Nat,U32.to_nat((position - low : U32)),local,relative_exact) : {Nat.is_lt(_,U32.to_nat((high - low : U32))) == True{} : Bool}
112 %Equal.sym(Nat,U32.to_nat((high - low : U32)),Nat.sub(hn,ln),range_exact) : {Nat.is_lt(local,_) == True{} : Bool}
113 %Equal.sym(Bool,Nat.is_lt(local,Nat.sub(hn,ln)),Nat.is_lt(Nat.add(ln,local),hn),Order.subtraction_lt(hn,ln,local)) : {_ == True{} : Bool}
114 %Equal.sym(Nat,Nat.add(ln,local),pn,Order.restore_shift(ln,pn,ordered)) : {Nat.is_lt(_,hn) == True{} : Bool} before