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