proofs/nat_to_u32_bounds.bend
stelliferous@0.0.2.0 · 86 lines · 9 definitions
1
2import Base
3import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32Successor
4import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
5import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
6
7def predecessor_strict(+a: Nat,+b: Nat,h: {Nat.is_le(1n+a,b) == True{} : Bool}) -> {Nat.is_lt(a,b) == True{} : Bool}:
8 match a b:
9 case 0n 0n:
10 Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(h))
11 case 0n 1n+bp:
12 {==}
13 case 1n+ap 0n:
14 Empty.absurd({Nat.is_lt(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
15 case 1n+ap 1n+bp:
16 predecessor_strict(ap,bp,h)
17
18def strict_le(+a: Nat,+b: Nat,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_le(a,b) == True{} : Bool}:
19 match a b:
20 case 0n 0n:
21 {==}
22 case 0n 1n+bp:
23 {==}
24 case 1n+ap 0n:
25 Empty.absurd({Nat.is_le(1n+ap,0n) == True{} : Bool},WordEncoding.false_true(h))
26 case 1n+ap 1n+bp:
27 strict_le(ap,bp,h)
28
29def add_one(+i: U32) -> {U32.add(i,1) == U32.inc(i) : U32}:
30 match i:
31 case U32{+w}:
32 %U32Successor.add_one(32n,w) : {U32{Word.add(32n,w,Word.inc(32n,Word.zero(32n)))} == U32{_} : U32}
33 {==}
34
35def native_bound(+n: Nat,+cap: U32,e: {U32.to_nat(U32.from_nat(n)) == n : Nat},h: {Nat.is_lt(n,
36 U32.to_nat(cap)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(n),cap) == True{} : Bool}:
37 %Equal.sym(Bool,U32.is_lt(U32.from_nat(n),cap),Nat.is_lt(U32.to_nat(U32.from_nat(n)),U32.to_nat(cap)),Comparison.lt(U32.from_nat(n),
38 cap)) : {_ == True{} : Bool}
39 %Equal.sym(Nat,U32.to_nat(U32.from_nat(n)),n,e) : {Nat.is_lt(_,U32.to_nat(cap)) == True{} : Bool}
40 h
41
42def nat_trans(+a: Nat,+b: Nat,+c: Nat,ab: {Nat.is_lt(a,b) == True{} : Bool},bc: {Nat.is_le(b,c) == True{} : Bool}) -> {Nat.is_lt(a,
43 c) == True{} : Bool}:
44 match a b c:
45 case 0n 0n c:
46 Empty.absurd({Nat.is_lt(0n,c) == True{} : Bool},WordEncoding.false_true(ab))
47 case 0n 1n+b 0n:
48 Empty.absurd({Nat.is_lt(0n,0n) == True{} : Bool},WordEncoding.false_true(bc))
49 case 0n 1n+b 1n+c:
50 {==}
51 case 1n+a 0n c:
52 Empty.absurd({Nat.is_lt(1n+a,c) == True{} : Bool},WordEncoding.false_true(ab))
53 case 1n+a 1n+b 0n:
54 Empty.absurd({Nat.is_lt(1n+a,0n) == True{} : Bool},WordEncoding.false_true(bc))
55 case 1n+a 1n+b 1n+c:
56 nat_trans(a,b,c,ab,bc)
57
58def as_nat_lt(+a: U32,+b: U32,h: {U32.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(a),U32.to_nat(b)) == True{} : Bool}:
59 %Comparison.lt(a,b) : {_ == True{} : Bool}
60 h
61
62def as_nat_le(+a: U32,+b: U32,h: {U32.is_le(a,b) == True{} : Bool}) -> {Nat.is_le(U32.to_nat(a),U32.to_nat(b)) == True{} : Bool}:
63 %Comparison.le(a,b) : {_ == True{} : Bool}
64 h
65
66def uint_trans(+a: U32,+b: U32,+c: U32,ab: {U32.is_lt(a,b) == True{} : Bool},bc: {U32.is_le(b,c) == True{} : Bool}) -> {U32.is_lt(a,
67 c) == True{} : Bool}:
68 %Equal.sym(Bool,U32.is_lt(a,c),Nat.is_lt(U32.to_nat(a),U32.to_nat(c)),Comparison.lt(a,c)) : {_ == True{} : Bool}
69 nat_trans(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c),as_nat_lt(a,b,ab),as_nat_le(b,c,bc))
70
71law roundtrip:
72 for +n: Nat
73 for +cap: U32
74 for +cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool}
75 for h: {Nat.is_le(n,U32.to_nat(cap)) == True{} : Bool}
76 {U32.to_nat(U32.from_nat(n)) == n : Nat}
77def roundtrip(n,cap,cap_ok,h):
78 match n:
79 case 0n:
80 {==}
81 case 1n+ +p:
82 +small = predecessor_strict(p,U32.to_nat(cap),h)
83 +previous = roundtrip(p,cap,cap_ok,strict_le(p,U32.to_nat(cap),small))
84 %previous : {U32.to_nat(U32.inc(U32.from_nat(p))) == 1n+_ : Nat}
85 %add_one(U32.from_nat(p)) : {U32.to_nat(_) == 1n+U32.to_nat(U32.from_nat(p)) : Nat}
86 U32Successor.successor(U32.from_nat(p))(uint_trans(U32.from_nat(p),cap,2147483648,native_bound(p,cap,previous,small),cap_ok))