1 import Base 2 import ../libs/AES256GCM.bend as AES 3 import ./AES_CertificateProof.bend as Certificate 4 import ./AES_StringEqProof.bend as Logic 5 6 def 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 28 def 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)) 58 def 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 80 def 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 111 def 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)))