proof/AES_LengthLimitProof.bend
qasim-bend-kit@0.1.0.2 · 110 lines · 5 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as ZipLengthProof
4
5def bool_and_true_right(+a: Bool, +b: Bool,
6 both: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
7 match a b:
8 case False{} False{}:
9 Empty.absurd({False{} == True{} : Bool},
10 ZipLengthProof.false_true(both))
11 case False{} True{}: {==}
12 case True{} False{}:
13 Empty.absurd({False{} == True{} : Bool},
14 ZipLengthProof.false_true(both))
15 case True{} True{}: {==}
16
17def predecessor(n: Nat) -> Nat:
18 match n:
19 case 0n: 0n
20 case 1n+p: p
21
22def length_limit_go_same(+a: List<&2, U32>, +b: List<&2, U32>,
23 +low: U32, +high: U32, +max_low: U32, +max_high: U32,
24 +within: Bool,
25 same_length: {List.length(&2, U32, a) ==
26 List.length(&2, U32, b) : Nat}) ->
27 {AES.bytes_length_limit.go(List.length(&2, U32, a), a,
28 low, high, max_low, max_high, within) ==
29 AES.bytes_length_limit.go(List.length(&2, U32, b), b,
30 low, high, max_low, max_high, within) : Bool}:
31 match a b within:
32 case Nil{} Nil{} _: {==}
33 case Nil{} y <> ys _:
34 mismatch = Equal.cong(Nat, Bool,
35 n => Nat.is_eq(0n, n),
36 List.length(&2, U32, Nil{}),
37 List.length(&2, U32, y <> ys), same_length)
38 Empty.absurd(
39 {AES.bytes_length_limit.go(0n, Nil{}, low, high,
40 max_low, max_high, within) ==
41 AES.bytes_length_limit.go(
42 List.length(&2, U32, y <> ys), y <> ys,
43 low, high, max_low, max_high, within) : Bool},
44 ZipLengthProof.false_true(Equal.sym(Bool,
45 True{}, False{}, mismatch)))
46 case x <> xs Nil{} _:
47 mismatch = Equal.cong(Nat, Bool,
48 n => Nat.is_eq(n, 0n),
49 List.length(&2, U32, x <> xs),
50 List.length(&2, U32, Nil{}), same_length)
51 Empty.absurd(
52 {AES.bytes_length_limit.go(
53 List.length(&2, U32, x <> xs), x <> xs,
54 low, high, max_low, max_high, within) ==
55 AES.bytes_length_limit.go(0n, Nil{}, low, high,
56 max_low, max_high, within) : Bool},
57 ZipLengthProof.false_true(mismatch))
58 case x <> xs y <> ys False{}: {==}
59 case x <> xs y <> ys True{}:
60 tail_length = Equal.cong(Nat, Nat, predecessor,
61 List.length(&2, U32, x <> xs),
62 List.length(&2, U32, y <> ys), same_length)
63 +next_low = U32.add(low, 1)
64 +next_high = Bool.pick(U32, U32.is_eq(next_low, 0),
65 U32.add(high, 1), high)
66 next_within = AES.length_pair_within(next_low, next_high,
67 max_low, max_high)
68 length_limit_go_same(xs, ys, next_low, next_high,
69 max_low, max_high, next_within, tail_length)
70
71def bytes_length_limit_same(+a: List<&2, U32>, +b: List<&2, U32>,
72 +max_low: U32, +max_high: U32,
73 same_length: {List.length(&2, U32, a) ==
74 List.length(&2, U32, b) : Nat}) ->
75 {AES.bytes_length_limit(a, max_low, max_high) ==
76 AES.bytes_length_limit(b, max_low, max_high) : Bool}:
77 length_limit_go_same(a, b, 0, 0, max_low, max_high, True{},
78 same_length)
79
80def plaintext_valid_same_length(+ciphertext: List<&2, U32>,
81 +plaintext: List<&2, U32>,
82 ciphertext_bytes_valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
83 plaintext_is_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
84 same_length: {List.length(&2, U32, ciphertext) ==
85 List.length(&2, U32, plaintext) : Nat}) ->
86 {AES.plaintext_valid(ciphertext) == True{} : Bool}:
87 length_limit_eq = bytes_length_limit_same(ciphertext, plaintext,
88 4294967264, 15, same_length)
89 plaintext_limit = bool_and_true_right(AES.bytes_valid(plaintext),
90 AES.bytes_length_limit(plaintext, 4294967264, 15),
91 plaintext_is_valid)
92 ciphertext_limit = Equal.trans(Bool,
93 AES.bytes_length_limit(ciphertext, 4294967264, 15),
94 AES.bytes_length_limit(plaintext, 4294967264, 15), True{},
95 length_limit_eq, plaintext_limit)
96 Equal.trans(Bool, AES.plaintext_valid(ciphertext),
97 Bool.and(True{}, True{}), True{},
98 Equal.trans(Bool,
99 Bool.and(AES.bytes_valid(ciphertext),
100 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
101 Bool.and(True{},
102 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
103 Bool.and(True{}, True{}),
104 Equal.cong(Bool, Bool, valid => Bool.and(valid,
105 AES.bytes_length_limit(ciphertext, 4294967264, 15)),
106 AES.bytes_valid(ciphertext), True{}, ciphertext_bytes_valid),
107 Equal.cong(Bool, Bool, within => Bool.and(True{}, within),
108 AES.bytes_length_limit(ciphertext, 4294967264, 15), True{},
109 ciphertext_limit)),
110 {==})