proof/AES_StringEqProof.bend

qasim-bend-kit@0.1.0.2 · 40 lines · 6 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as Compare
3
4def false_type(b: Bool) -> Data:
5    match b:
6        case False{}: Unit
7        case True{}: Empty
8
9def false_true(e: {False{} == True{} : Bool}) -> Empty:
10    %e : false_type(_)
11    Unit{}
12
13def cmp_eq_of_true(c: Cmp,
14    accepted: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
15    match c:
16        case EQ{}: {==}
17        case LT{}: Empty.absurd({LT{} == EQ{} : Cmp}, false_true(accepted))
18        case GT{}: Empty.absurd({GT{} == EQ{} : Cmp}, false_true(accepted))
19
20def tag_is_snd(r: (String & String) & Cmp) ->
21    {Compare.comparison_tag(String, r) ==
22     Pair.snd(String & String, Cmp, r) : Cmp}:
23    match r:
24        case ((a, b), c): {==}
25
26def string_eq_sound(+a: String, +b: String,
27    accepted: {String.eq(a, b) == True{} : Bool}) -> {a == b : String}:
28    Compare.string_equal_from_comparison(a, b,
29        Equal.trans(Cmp,
30            Compare.comparison_tag(String, String.cmp(a, b)),
31            String.order(a, b), EQ{},
32            tag_is_snd(String.cmp(a, b)),
33            cmp_eq_of_true(String.order(a, b), accepted)))
34
35def string_eq_self(+s: String) ->
36    {String.eq(s, s) == True{} : Bool}:
37    Equal.cong((String & String) & Cmp, Bool,
38        result => Cmp.is_eq(Pair.snd(String & String, Cmp, result)),
39        String.cmp(s, s), ((s, s), EQ{}),
40        Compare.string_compare_self(s))