proof/AES_ConstructorProof.bend
qasim-bend-kit@0.1.0.2 · 135 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_CertificateProof.bend as Certificate
4import qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend as Logic
5
6def key_certificates(+bytes: List<&2, U32>,
7 +first_size: {List.length(&2, U32, bytes) == 32n : Nat},
8 +first_valid: {AES.bytes_valid(bytes) == True{} : Bool},
9 +second_size: {List.length(&2, U32, bytes) == 32n : Nat},
10 +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
11 {AES.SecretKey{bytes, first_size, first_valid} ==
12 AES.SecretKey{bytes, second_size, second_valid} : AES.SecretKey}:
13 Equal.trans(AES.SecretKey,
14 AES.SecretKey{bytes, first_size, first_valid},
15 AES.SecretKey{bytes, second_size, first_valid},
16 AES.SecretKey{bytes, second_size, second_valid},
17 Equal.cong({List.length(&2, U32, bytes) == 32n : Nat}, AES.SecretKey,
18 proof => AES.SecretKey{bytes, proof, first_valid},
19 first_size, second_size,
20 Certificate.nat_unique(List.length(&2, U32, bytes), 32n,
21 first_size, second_size)),
22 Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.SecretKey,
23 proof => AES.SecretKey{bytes, second_size, proof},
24 first_valid, second_valid,
25 Certificate.bool_unique(AES.bytes_valid(bytes), True{},
26 first_valid, second_valid)))
27
28def key_accepts(+bytes: List<&2, U32>,
29 +expected_size: {List.length(&2, U32, bytes) == 32n : Nat},
30 +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool},
31 size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>,
32 valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
33 size_present: {Maybe.is_some(&0,
34 {List.length(&2, U32, bytes) == 32n : Nat}, size) == True{} : Bool},
35 valid_present: {Maybe.is_some(&0,
36 {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) ->
37 {AES.key_from_proofs(bytes, size, valid) ==
38 Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
39 Result<&2, &2, AES.Error, AES.SecretKey>}:
40 match size valid:
41 case None{} _:
42 Empty.absurd({AES.key_from_proofs(bytes, size, valid) ==
43 Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
44 Result<&2, &2, AES.Error, AES.SecretKey>},
45 Logic.false_true(size_present))
46 case _ None{}:
47 Empty.absurd({AES.key_from_proofs(bytes, size, valid) ==
48 Done{AES.SecretKey{bytes, expected_size, expected_valid}} :
49 Result<&2, &2, AES.Error, AES.SecretKey>},
50 Logic.false_true(valid_present))
51 case Some{size_proof} Some{valid_proof}:
52 Equal.cong(AES.SecretKey,
53 Result<&2, &2, AES.Error, AES.SecretKey>, value => Done{value},
54 AES.SecretKey{bytes, size_proof, valid_proof},
55 AES.SecretKey{bytes, expected_size, expected_valid},
56 key_certificates(bytes, size_proof, valid_proof,
57 expected_size, expected_valid))
58def nonce_certificates(+bytes: List<&2, U32>,
59 +first_size: {List.length(&2, U32, bytes) == 12n : Nat},
60 +first_valid: {AES.bytes_valid(bytes) == True{} : Bool},
61 +second_size: {List.length(&2, U32, bytes) == 12n : Nat},
62 +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
63 {AES.Nonce{bytes, first_size, first_valid} ==
64 AES.Nonce{bytes, second_size, second_valid} : AES.Nonce}:
65 Equal.trans(AES.Nonce,
66 AES.Nonce{bytes, first_size, first_valid},
67 AES.Nonce{bytes, second_size, first_valid},
68 AES.Nonce{bytes, second_size, second_valid},
69 Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce,
70 proof => AES.Nonce{bytes, proof, first_valid},
71 first_size, second_size,
72 Certificate.nat_unique(List.length(&2, U32, bytes), 12n,
73 first_size, second_size)),
74 Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce,
75 proof => AES.Nonce{bytes, second_size, proof},
76 first_valid, second_valid,
77 Certificate.bool_unique(AES.bytes_valid(bytes), True{},
78 first_valid, second_valid)))
79
80def nonce_accepts(+bytes: List<&2, U32>,
81 +expected_size: {List.length(&2, U32, bytes) == 12n : Nat},
82 +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool},
83 size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>,
84 valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>,
85 size_present: {Maybe.is_some(&0,
86 {List.length(&2, U32, bytes) == 12n : Nat}, size) == True{} : Bool},
87 valid_present: {Maybe.is_some(&0,
88 {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) ->
89 {AES.nonce_from_proofs(bytes, size, valid) ==
90 Done{AES.Nonce{bytes, expected_size, expected_valid}} :
91 Result<&2, &2, AES.Error, AES.Nonce>}:
92 match size valid:
93 case None{} _:
94 Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
95 Done{AES.Nonce{bytes, expected_size, expected_valid}} :
96 Result<&2, &2, AES.Error, AES.Nonce>},
97 Logic.false_true(size_present))
98 case _ None{}:
99 Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) ==
100 Done{AES.Nonce{bytes, expected_size, expected_valid}} :
101 Result<&2, &2, AES.Error, AES.Nonce>},
102 Logic.false_true(valid_present))
103 case Some{size_proof} Some{valid_proof}:
104 Equal.cong(AES.Nonce,
105 Result<&2, &2, AES.Error, AES.Nonce>, value => Done{value},
106 AES.Nonce{bytes, size_proof, valid_proof},
107 AES.Nonce{bytes, expected_size, expected_valid},
108 nonce_certificates(bytes, size_proof, valid_proof,
109 expected_size, expected_valid))
110
111def nonce_equal(+bytes: List<&2, U32>,
112 +size: {List.length(&2, U32, bytes) == 12n : Nat},
113 +valid: {AES.bytes_valid(bytes) == True{} : Bool},
114 +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
115 @+expected_size: {List.length(&2, U32, expected) == 12n : Nat} ->
116 @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
117 {AES.Nonce{bytes, size, valid} ==
118 AES.Nonce{expected, expected_size, expected_valid} : AES.Nonce}:
119 %same :
120 @+expected_size: {List.length(&2, U32, _) == 12n : Nat} ->
121 @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
122 {AES.Nonce{bytes, size, valid} ==
123 AES.Nonce{_, expected_size, expected_valid} : AES.Nonce}
124 expected_size => expected_valid =>
125 Equal.trans(AES.Nonce, AES.Nonce{bytes, size, valid},
126 AES.Nonce{bytes, expected_size, valid},
127 AES.Nonce{bytes, expected_size, expected_valid},
128 Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce,
129 proof => AES.Nonce{bytes, proof, valid}, size, expected_size,
130 Certificate.nat_unique(List.length(&2, U32, bytes), 12n,
131 size, expected_size)),
132 Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce,
133 proof => AES.Nonce{bytes, expected_size, proof}, valid,
134 expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
135 True{}, valid, expected_valid)))