proof/AES_ConstructorProof.bend source
proof/AES_ConstructorProof.bend on the hub · documented module
import Base import ../libs/AES256GCM.bend as AES import ./AES_CertificateProof.bend as Certificate import ./AES_StringEqProof.bend as Logic def key_certificates(+bytes: List<&2, U32>, +first_size: {List.length(&2, U32, bytes) == 32n : Nat}, +first_valid: {AES.bytes_valid(bytes) == True{} : Bool}, +second_size: {List.length(&2, U32, bytes) == 32n : Nat}, +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) -> {AES.SecretKey{bytes, first_size, first_valid} == AES.SecretKey{bytes, second_size, second_valid} : AES.SecretKey}: Equal.trans(AES.SecretKey, AES.SecretKey{bytes, first_size, first_valid}, AES.SecretKey{bytes, second_size, first_valid}, AES.SecretKey{bytes, second_size, second_valid}, Equal.cong({List.length(&2, U32, bytes) == 32n : Nat}, AES.SecretKey, proof => AES.SecretKey{bytes, proof, first_valid}, first_size, second_size, Certificate.nat_unique(List.length(&2, U32, bytes), 32n, first_size, second_size)), Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.SecretKey, proof => AES.SecretKey{bytes, second_size, proof}, first_valid, second_valid, Certificate.bool_unique(AES.bytes_valid(bytes), True{}, first_valid, second_valid))) def key_accepts(+bytes: List<&2, U32>, +expected_size: {List.length(&2, U32, bytes) == 32n : Nat}, +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool}, size: Maybe<&0, {List.length(&2, U32, bytes) == 32n : Nat}>, valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>, size_present: {Maybe.is_some(&0, {List.length(&2, U32, bytes) == 32n : Nat}, size) == True{} : Bool}, valid_present: {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) -> {AES.key_from_proofs(bytes, size, valid) == Done{AES.SecretKey{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.SecretKey>}: match size valid: case None{} _: Empty.absurd({AES.key_from_proofs(bytes, size, valid) == Done{AES.SecretKey{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.SecretKey>}, Logic.false_true(size_present)) case _ None{}: Empty.absurd({AES.key_from_proofs(bytes, size, valid) == Done{AES.SecretKey{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.SecretKey>}, Logic.false_true(valid_present)) case Some{size_proof} Some{valid_proof}: Equal.cong(AES.SecretKey, Result<&2, &2, AES.Error, AES.SecretKey>, value => Done{value}, AES.SecretKey{bytes, size_proof, valid_proof}, AES.SecretKey{bytes, expected_size, expected_valid}, key_certificates(bytes, size_proof, valid_proof, expected_size, expected_valid)) def nonce_certificates(+bytes: List<&2, U32>, +first_size: {List.length(&2, U32, bytes) == 12n : Nat}, +first_valid: {AES.bytes_valid(bytes) == True{} : Bool}, +second_size: {List.length(&2, U32, bytes) == 12n : Nat}, +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) -> {AES.Nonce{bytes, first_size, first_valid} == AES.Nonce{bytes, second_size, second_valid} : AES.Nonce}: Equal.trans(AES.Nonce, AES.Nonce{bytes, first_size, first_valid}, AES.Nonce{bytes, second_size, first_valid}, AES.Nonce{bytes, second_size, second_valid}, Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce, proof => AES.Nonce{bytes, proof, first_valid}, first_size, second_size, Certificate.nat_unique(List.length(&2, U32, bytes), 12n, first_size, second_size)), Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce, proof => AES.Nonce{bytes, second_size, proof}, first_valid, second_valid, Certificate.bool_unique(AES.bytes_valid(bytes), True{}, first_valid, second_valid))) def nonce_accepts(+bytes: List<&2, U32>, +expected_size: {List.length(&2, U32, bytes) == 12n : Nat}, +expected_valid: {AES.bytes_valid(bytes) == True{} : Bool}, size: Maybe<&0, {List.length(&2, U32, bytes) == 12n : Nat}>, valid: Maybe<&0, {AES.bytes_valid(bytes) == True{} : Bool}>, size_present: {Maybe.is_some(&0, {List.length(&2, U32, bytes) == 12n : Nat}, size) == True{} : Bool}, valid_present: {Maybe.is_some(&0, {AES.bytes_valid(bytes) == True{} : Bool}, valid) == True{} : Bool}) -> {AES.nonce_from_proofs(bytes, size, valid) == Done{AES.Nonce{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.Nonce>}: match size valid: case None{} _: Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) == Done{AES.Nonce{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.Nonce>}, Logic.false_true(size_present)) case _ None{}: Empty.absurd({AES.nonce_from_proofs(bytes, size, valid) == Done{AES.Nonce{bytes, expected_size, expected_valid}} : Result<&2, &2, AES.Error, AES.Nonce>}, Logic.false_true(valid_present)) case Some{size_proof} Some{valid_proof}: Equal.cong(AES.Nonce, Result<&2, &2, AES.Error, AES.Nonce>, value => Done{value}, AES.Nonce{bytes, size_proof, valid_proof}, AES.Nonce{bytes, expected_size, expected_valid}, nonce_certificates(bytes, size_proof, valid_proof, expected_size, expected_valid)) def nonce_equal(+bytes: List<&2, U32>, +size: {List.length(&2, U32, bytes) == 12n : Nat}, +valid: {AES.bytes_valid(bytes) == True{} : Bool}, +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) -> @+expected_size: {List.length(&2, U32, expected) == 12n : Nat} -> @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} -> {AES.Nonce{bytes, size, valid} == AES.Nonce{expected, expected_size, expected_valid} : AES.Nonce}: %same : @+expected_size: {List.length(&2, U32, _) == 12n : Nat} -> @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} -> {AES.Nonce{bytes, size, valid} == AES.Nonce{_, expected_size, expected_valid} : AES.Nonce} expected_size => expected_valid => Equal.trans(AES.Nonce, AES.Nonce{bytes, size, valid}, AES.Nonce{bytes, expected_size, valid}, AES.Nonce{bytes, expected_size, expected_valid}, Equal.cong({List.length(&2, U32, bytes) == 12n : Nat}, AES.Nonce, proof => AES.Nonce{bytes, proof, valid}, size, expected_size, Certificate.nat_unique(List.length(&2, U32, bytes), 12n, size, expected_size)), Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Nonce, proof => AES.Nonce{bytes, expected_size, proof}, valid, expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes), True{}, valid, expected_valid)))