proof/AES_CertificateProof.bend

qasim-bend-kit@0.1.0.2 · 137 lines · 16 definitions

1import Base
2
3# Decidable equality makes certificates for Bool and Nat unique. These lemmas
4# compare proofs without evaluating the computation that produced each proof.
5def bool_code(a: Bool, b: Bool) -> Data:
6    match a b:
7        case False{} False{}: Unit
8        case True{} True{}: Unit
9        case _ _: Empty
10
11def bool_code_refl(a: Bool) -> bool_code(a, a):
12    match a:
13        case False{}: Unit{}
14        case True{}: Unit{}
15
16def bool_encode(+a: Bool, +b: Bool, proof: {a == b : Bool}) -> bool_code(a, b):
17    %proof : bool_code(a, _)
18    bool_code_refl(a)
19
20def bool_decode(+a: Bool, +b: Bool, code: bool_code(a, b)) -> {a == b : Bool}:
21    match a b:
22        case False{} False{}: {==}
23        case True{} True{}: {==}
24        case False{} True{}: Empty.absurd({a == b : Bool}, code)
25        case True{} False{}: Empty.absurd({a == b : Bool}, code)
26
27def bool_decode_refl(+a: Bool) ->
28    {bool_decode(a, a, bool_code_refl(a)) == {==} : {a == a : Bool}}:
29    match a:
30        case False{}: {==}
31        case True{}: {==}
32
33def bool_decode_encode(+a: Bool, +b: Bool, +proof: {a == b : Bool}) ->
34    {bool_decode(a, b, bool_encode(a, b, proof)) == proof : {a == b : Bool}}:
35    %path@proof : {bool_decode(a, _, bool_encode(a, _, path)) == path :
36        {a == _ : Bool}}
37    bool_decode_refl(a)
38
39def bool_code_unique(+a: Bool, +b: Bool,
40    +first: bool_code(a, b), second: bool_code(a, b)) ->
41    {first == second : bool_code(a, b)}:
42    match a b:
43        case False{} False{}:
44            match first second:
45                case Unit{} Unit{}: {==}
46        case True{} True{}:
47            match first second:
48                case Unit{} Unit{}: {==}
49        case False{} True{}:
50            Empty.absurd({first == second : bool_code(a, b)}, first)
51        case True{} False{}:
52            Empty.absurd({first == second : bool_code(a, b)}, first)
53
54def bool_unique(+a: Bool, +b: Bool,
55    +first: {a == b : Bool}, +second: {a == b : Bool}) ->
56    {first == second : {a == b : Bool}}:
57    +first_code = bool_encode(a, b, first)
58    +second_code = bool_encode(a, b, second)
59    codes_same = bool_code_unique(a, b, first_code, second_code)
60    decoded_same = Equal.cong(bool_code(a, b), {a == b : Bool},
61        code => bool_decode(a, b, code), first_code, second_code, codes_same)
62    Equal.trans({a == b : Bool}, first, bool_decode(a, b, first_code), second,
63        Equal.sym({a == b : Bool}, bool_decode(a, b, first_code), first,
64            bool_decode_encode(a, b, first)),
65        Equal.trans({a == b : Bool}, bool_decode(a, b, first_code),
66            bool_decode(a, b, second_code), second, decoded_same,
67            bool_decode_encode(a, b, second)))
68
69def nat_code(a: Nat, b: Nat) -> Data:
70    match a b:
71        case 0n 0n: Unit
72        case 1n+p 1n+q: nat_code(p, q)
73        case _ _: Empty
74
75def nat_code_refl(a: Nat) -> nat_code(a, a):
76    match a:
77        case 0n: Unit{}
78        case 1n+p: nat_code_refl(p)
79
80def nat_encode(+a: Nat, +b: Nat, proof: {a == b : Nat}) -> nat_code(a, b):
81    %proof : nat_code(a, _)
82    nat_code_refl(a)
83
84def nat_decode(+a: Nat, +b: Nat, code: nat_code(a, b)) -> {a == b : Nat}:
85    match a b:
86        case 0n 0n: {==}
87        case 0n 1n+q: Empty.absurd({a == b : Nat}, code)
88        case 1n+p 0n: Empty.absurd({a == b : Nat}, code)
89        case 1n+p 1n+q:
90            Equal.cong(Nat, Nat, value => 1n+value, p, q,
91                nat_decode(p, q, code))
92
93def nat_decode_refl(+a: Nat) ->
94    {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}:
95    match a:
96        case 0n: {==}
97        case 1n+p:
98            %Equal.sym({p == p : Nat},
99                nat_decode(p, p, nat_code_refl(p)), {==},
100                nat_decode_refl(p)) :
101                {Equal.cong(Nat, Nat, value => 1n+value, p, p, _) == {==} :
102                    {1n+p == 1n+p : Nat}}
103            {==}
104
105def nat_decode_encode(+a: Nat, +b: Nat, +proof: {a == b : Nat}) ->
106    {nat_decode(a, b, nat_encode(a, b, proof)) == proof : {a == b : Nat}}:
107    %path@proof : {nat_decode(a, _, nat_encode(a, _, path)) == path :
108        {a == _ : Nat}}
109    nat_decode_refl(a)
110
111def nat_code_unique(+a: Nat, +b: Nat,
112    +first: nat_code(a, b), second: nat_code(a, b)) ->
113    {first == second : nat_code(a, b)}:
114    match a b:
115        case 0n 0n:
116            match first second:
117                case Unit{} Unit{}: {==}
118        case 0n 1n+q:
119            Empty.absurd({first == second : nat_code(a, b)}, first)
120        case 1n+p 0n:
121            Empty.absurd({first == second : nat_code(a, b)}, first)
122        case 1n+p 1n+q: nat_code_unique(p, q, first, second)
123
124def nat_unique(+a: Nat, +b: Nat,
125    +first: {a == b : Nat}, +second: {a == b : Nat}) ->
126    {first == second : {a == b : Nat}}:
127    +first_code = nat_encode(a, b, first)
128    +second_code = nat_encode(a, b, second)
129    codes_same = nat_code_unique(a, b, first_code, second_code)
130    decoded_same = Equal.cong(nat_code(a, b), {a == b : Nat},
131        code => nat_decode(a, b, code), first_code, second_code, codes_same)
132    Equal.trans({a == b : Nat}, first, nat_decode(a, b, first_code), second,
133        Equal.sym({a == b : Nat}, nat_decode(a, b, first_code), first,
134            nat_decode_encode(a, b, first)),
135        Equal.trans({a == b : Nat}, nat_decode(a, b, first_code),
136            nat_decode(a, b, second_code), second, decoded_same,
137            nat_decode_encode(a, b, second)))