|
| 1 | +// Package AESEncryption |
| 2 | +// Dafny module AESEncryption compiled into Go |
| 3 | + |
| 4 | +package AESEncryption |
| 5 | + |
| 6 | +import ( |
| 7 | + os "os" |
| 8 | + |
| 9 | + m_AwsCryptographyPrimitivesTypes "github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/AwsCryptographyPrimitivesTypes" |
| 10 | + m_Random "github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives/Random" |
| 11 | + m_Actions "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Actions" |
| 12 | + m_Base64 "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Base64" |
| 13 | + m_Base64Lemmas "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Base64Lemmas" |
| 14 | + m_BoundedInts "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/BoundedInts" |
| 15 | + m_DivInternals "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/DivInternals" |
| 16 | + m_DivInternalsNonlinear "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/DivInternalsNonlinear" |
| 17 | + m_DivMod "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/DivMod" |
| 18 | + m_FileIO "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/FileIO" |
| 19 | + m_FloatCompare "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/FloatCompare" |
| 20 | + m_Functions "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Functions" |
| 21 | + m_GeneralInternals "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/GeneralInternals" |
| 22 | + m_GetOpt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/GetOpt" |
| 23 | + m_HexStrings "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/HexStrings" |
| 24 | + m_Logarithm "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Logarithm" |
| 25 | + m__Math "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Math_" |
| 26 | + m_ModInternals "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/ModInternals" |
| 27 | + m_ModInternalsNonlinear "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/ModInternalsNonlinear" |
| 28 | + m_Mul "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Mul" |
| 29 | + m_MulInternals "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/MulInternals" |
| 30 | + m_MulInternalsNonlinear "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/MulInternalsNonlinear" |
| 31 | + m_Power "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Power" |
| 32 | + m_Relations "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Relations" |
| 33 | + m_Seq "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Seq" |
| 34 | + m_Seq_MergeSort "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Seq_MergeSort" |
| 35 | + m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting" |
| 36 | + m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary" |
| 37 | + m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop" |
| 38 | + m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence" |
| 39 | + m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String" |
| 40 | + m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt" |
| 41 | + m_Streams "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Streams" |
| 42 | + m_UnicodeStrings "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/UnicodeStrings" |
| 43 | + m__Unicode "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Unicode_" |
| 44 | + m_Utf16EncodingForm "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Utf16EncodingForm" |
| 45 | + m_Utf8EncodingForm "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Utf8EncodingForm" |
| 46 | + m_Wrappers "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" |
| 47 | + m__System "github.com/dafny-lang/DafnyRuntimeGo/v4/System_" |
| 48 | + _dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" |
| 49 | +) |
| 50 | + |
| 51 | +var _ = os.Args |
| 52 | +var _ _dafny.Dummy__ |
| 53 | +var _ m__System.Dummy__ |
| 54 | +var _ m_Wrappers.Dummy__ |
| 55 | +var _ m_Relations.Dummy__ |
| 56 | +var _ m_Seq_MergeSort.Dummy__ |
| 57 | +var _ m__Math.Dummy__ |
| 58 | +var _ m_Seq.Dummy__ |
| 59 | +var _ m_BoundedInts.Dummy__ |
| 60 | +var _ m__Unicode.Dummy__ |
| 61 | +var _ m_Functions.Dummy__ |
| 62 | +var _ m_Utf8EncodingForm.Dummy__ |
| 63 | +var _ m_Utf16EncodingForm.Dummy__ |
| 64 | +var _ m_UnicodeStrings.Dummy__ |
| 65 | +var _ m_FileIO.Dummy__ |
| 66 | +var _ m_GeneralInternals.Dummy__ |
| 67 | +var _ m_MulInternalsNonlinear.Dummy__ |
| 68 | +var _ m_MulInternals.Dummy__ |
| 69 | +var _ m_Mul.Dummy__ |
| 70 | +var _ m_ModInternalsNonlinear.Dummy__ |
| 71 | +var _ m_DivInternalsNonlinear.Dummy__ |
| 72 | +var _ m_ModInternals.Dummy__ |
| 73 | +var _ m_DivInternals.Dummy__ |
| 74 | +var _ m_DivMod.Dummy__ |
| 75 | +var _ m_Power.Dummy__ |
| 76 | +var _ m_Logarithm.Dummy__ |
| 77 | +var _ m_StandardLibraryInterop.Dummy__ |
| 78 | +var _ m_StandardLibrary_UInt.Dummy__ |
| 79 | +var _ m_StandardLibrary_Sequence.Dummy__ |
| 80 | +var _ m_StandardLibrary_String.Dummy__ |
| 81 | +var _ m_StandardLibrary.Dummy__ |
| 82 | +var _ m_Streams.Dummy__ |
| 83 | +var _ m_Sorting.Dummy__ |
| 84 | +var _ m_HexStrings.Dummy__ |
| 85 | +var _ m_GetOpt.Dummy__ |
| 86 | +var _ m_FloatCompare.Dummy__ |
| 87 | +var _ m_Base64.Dummy__ |
| 88 | +var _ m_Base64Lemmas.Dummy__ |
| 89 | +var _ m_Actions.Dummy__ |
| 90 | +var _ m_AwsCryptographyPrimitivesTypes.Dummy__ |
| 91 | +var _ m_Random.Dummy__ |
| 92 | + |
| 93 | +type Dummy__ struct{} |
| 94 | + |
| 95 | +// Definition of class Default__ |
| 96 | +type Default__ struct { |
| 97 | + dummy byte |
| 98 | +} |
| 99 | + |
| 100 | +func New_Default___() *Default__ { |
| 101 | + _this := Default__{} |
| 102 | + |
| 103 | + return &_this |
| 104 | +} |
| 105 | + |
| 106 | +type CompanionStruct_Default___ struct { |
| 107 | +} |
| 108 | + |
| 109 | +var Companion_Default___ = CompanionStruct_Default___{} |
| 110 | + |
| 111 | +func (_this *Default__) Equals(other *Default__) bool { |
| 112 | + return _this == other |
| 113 | +} |
| 114 | + |
| 115 | +func (_this *Default__) EqualsGeneric(x interface{}) bool { |
| 116 | + other, ok := x.(*Default__) |
| 117 | + return ok && _this.Equals(other) |
| 118 | +} |
| 119 | + |
| 120 | +func (*Default__) String() string { |
| 121 | + return "AESEncryption.Default__" |
| 122 | +} |
| 123 | +func (_this *Default__) ParentTraits_() []*_dafny.TraitID { |
| 124 | + return [](*_dafny.TraitID){} |
| 125 | +} |
| 126 | + |
| 127 | +var _ _dafny.TraitOffspring = &Default__{} |
| 128 | + |
| 129 | +func (_static *CompanionStruct_Default___) EncryptionOutputFromByteSeq(s _dafny.Sequence, encAlg m_AwsCryptographyPrimitivesTypes.AES__GCM) m_AwsCryptographyPrimitivesTypes.AESEncryptOutput { |
| 130 | + var _0_cipherText _dafny.Sequence = (s).Take(((_dafny.IntOfUint32((s).Cardinality())).Minus(_dafny.IntOfInt32((encAlg).Dtor_tagLength()))).Uint32()) |
| 131 | + _ = _0_cipherText |
| 132 | + var _1_authTag _dafny.Sequence = (s).Drop(((_dafny.IntOfUint32((s).Cardinality())).Minus(_dafny.IntOfInt32((encAlg).Dtor_tagLength()))).Uint32()) |
| 133 | + _ = _1_authTag |
| 134 | + return m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Create_AESEncryptOutput_(_0_cipherText, _1_authTag) |
| 135 | +} |
| 136 | +func (_static *CompanionStruct_Default___) AESEncrypt(input m_AwsCryptographyPrimitivesTypes.AESEncryptInput) m_Wrappers.Result { |
| 137 | + var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Default()) |
| 138 | + _ = res |
| 139 | + var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() |
| 140 | + _ = _0_valueOrError0 |
| 141 | + _0_valueOrError0 = m_Wrappers.Companion_Default___.Need(((_dafny.IntOfUint32(((input).Dtor_iv()).Cardinality())).Cmp(_dafny.IntOfInt32(((input).Dtor_encAlg()).Dtor_ivLength())) == 0) && ((_dafny.IntOfUint32(((input).Dtor_key()).Cardinality())).Cmp(_dafny.IntOfInt32(((input).Dtor_encAlg()).Dtor_keyLength())) == 0), m_AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(_dafny.SeqOfString("Request does not match algorithm."))) |
| 142 | + if (_0_valueOrError0).IsFailure() { |
| 143 | + res = (_0_valueOrError0).PropagateFailure() |
| 144 | + return res |
| 145 | + } |
| 146 | + var _let_tmp_rhs0 m_AwsCryptographyPrimitivesTypes.AESEncryptInput = input |
| 147 | + _ = _let_tmp_rhs0 |
| 148 | + var _1_encAlg m_AwsCryptographyPrimitivesTypes.AES__GCM = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESEncryptInput_AESEncryptInput).EncAlg |
| 149 | + _ = _1_encAlg |
| 150 | + var _2_iv _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESEncryptInput_AESEncryptInput).Iv |
| 151 | + _ = _2_iv |
| 152 | + var _3_key _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESEncryptInput_AESEncryptInput).Key |
| 153 | + _ = _3_key |
| 154 | + var _4_msg _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESEncryptInput_AESEncryptInput).Msg |
| 155 | + _ = _4_msg |
| 156 | + var _5_aad _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESEncryptInput_AESEncryptInput).Aad |
| 157 | + _ = _5_aad |
| 158 | + var _6_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(m_AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Default()) |
| 159 | + _ = _6_valueOrError1 |
| 160 | + var _out0 m_Wrappers.Result |
| 161 | + _ = _out0 |
| 162 | + _out0 = m_AESEncryption.AES_GCM.AESEncryptExtern(_1_encAlg, _2_iv, _3_key, _4_msg, _5_aad) |
| 163 | + _6_valueOrError1 = _out0 |
| 164 | + if (_6_valueOrError1).IsFailure() { |
| 165 | + res = (_6_valueOrError1).PropagateFailure() |
| 166 | + return res |
| 167 | + } |
| 168 | + var _7_value m_AwsCryptographyPrimitivesTypes.AESEncryptOutput |
| 169 | + _ = _7_value |
| 170 | + _7_value = (_6_valueOrError1).Extract().(m_AwsCryptographyPrimitivesTypes.AESEncryptOutput) |
| 171 | + var _8_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() |
| 172 | + _ = _8_valueOrError2 |
| 173 | + _8_valueOrError2 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_7_value).Dtor_cipherText()).Cardinality())).Cmp(_dafny.IntOfUint32((_4_msg).Cardinality())) == 0, m_AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(_dafny.SeqOfString("AESEncrypt did not return cipherText of expected length"))) |
| 174 | + if (_8_valueOrError2).IsFailure() { |
| 175 | + res = (_8_valueOrError2).PropagateFailure() |
| 176 | + return res |
| 177 | + } |
| 178 | + var _9_valueOrError3 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() |
| 179 | + _ = _9_valueOrError3 |
| 180 | + _9_valueOrError3 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32(((_7_value).Dtor_authTag()).Cardinality())).Cmp(_dafny.IntOfInt32((_1_encAlg).Dtor_tagLength())) == 0, m_AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(_dafny.SeqOfString("AESEncryption did not return valid tag"))) |
| 181 | + if (_9_valueOrError3).IsFailure() { |
| 182 | + res = (_9_valueOrError3).PropagateFailure() |
| 183 | + return res |
| 184 | + } |
| 185 | + res = m_Wrappers.Companion_Result_.Create_Success_(_7_value) |
| 186 | + return res |
| 187 | + return res |
| 188 | +} |
| 189 | +func (_static *CompanionStruct_Default___) AESDecrypt(input m_AwsCryptographyPrimitivesTypes.AESDecryptInput) m_Wrappers.Result { |
| 190 | + var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) |
| 191 | + _ = res |
| 192 | + var _0_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() |
| 193 | + _ = _0_valueOrError0 |
| 194 | + _0_valueOrError0 = m_Wrappers.Companion_Default___.Need((((_dafny.IntOfUint32(((input).Dtor_key()).Cardinality())).Cmp(_dafny.IntOfInt32(((input).Dtor_encAlg()).Dtor_keyLength())) == 0) && ((_dafny.IntOfUint32(((input).Dtor_iv()).Cardinality())).Cmp(_dafny.IntOfInt32(((input).Dtor_encAlg()).Dtor_ivLength())) == 0)) && ((_dafny.IntOfUint32(((input).Dtor_authTag()).Cardinality())).Cmp(_dafny.IntOfInt32(((input).Dtor_encAlg()).Dtor_tagLength())) == 0), m_AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(_dafny.SeqOfString("Request does not match algorithm."))) |
| 195 | + if (_0_valueOrError0).IsFailure() { |
| 196 | + res = (_0_valueOrError0).PropagateFailure() |
| 197 | + return res |
| 198 | + } |
| 199 | + var _let_tmp_rhs0 m_AwsCryptographyPrimitivesTypes.AESDecryptInput = input |
| 200 | + _ = _let_tmp_rhs0 |
| 201 | + var _1_encAlg m_AwsCryptographyPrimitivesTypes.AES__GCM = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).EncAlg |
| 202 | + _ = _1_encAlg |
| 203 | + var _2_key _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).Key |
| 204 | + _ = _2_key |
| 205 | + var _3_cipherTxt _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).CipherTxt |
| 206 | + _ = _3_cipherTxt |
| 207 | + var _4_authTag _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).AuthTag |
| 208 | + _ = _4_authTag |
| 209 | + var _5_iv _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).Iv |
| 210 | + _ = _5_iv |
| 211 | + var _6_aad _dafny.Sequence = _let_tmp_rhs0.Get_().(m_AwsCryptographyPrimitivesTypes.AESDecryptInput_AESDecryptInput).Aad |
| 212 | + _ = _6_aad |
| 213 | + var _7_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq) |
| 214 | + _ = _7_valueOrError1 |
| 215 | + var _out0 m_Wrappers.Result |
| 216 | + _ = _out0 |
| 217 | + _out0 = m_AESEncryption.AES_GCM.AESDecryptExtern(_1_encAlg, _2_key, _3_cipherTxt, _4_authTag, _5_iv, _6_aad) |
| 218 | + _7_valueOrError1 = _out0 |
| 219 | + if (_7_valueOrError1).IsFailure() { |
| 220 | + res = (_7_valueOrError1).PropagateFailure() |
| 221 | + return res |
| 222 | + } |
| 223 | + var _8_value _dafny.Sequence |
| 224 | + _ = _8_value |
| 225 | + _8_value = (_7_valueOrError1).Extract().(_dafny.Sequence) |
| 226 | + var _9_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Outcome_.Default() |
| 227 | + _ = _9_valueOrError2 |
| 228 | + _9_valueOrError2 = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_3_cipherTxt).Cardinality())).Cmp(_dafny.IntOfUint32((_8_value).Cardinality())) == 0, m_AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(_dafny.SeqOfString("AESDecrypt did not return plaintext of expected length"))) |
| 229 | + if (_9_valueOrError2).IsFailure() { |
| 230 | + res = (_9_valueOrError2).PropagateFailure() |
| 231 | + return res |
| 232 | + } |
| 233 | + res = m_Wrappers.Companion_Result_.Create_Success_(_8_value) |
| 234 | + return res |
| 235 | + return res |
| 236 | +} |
| 237 | +func (_static *CompanionStruct_Default___) CreateAESEncryptExternSuccess(output m_AwsCryptographyPrimitivesTypes.AESEncryptOutput) m_Wrappers.Result { |
| 238 | + return m_Wrappers.Companion_Result_.Create_Success_(output) |
| 239 | +} |
| 240 | +func (_static *CompanionStruct_Default___) CreateAESEncryptExternFailure(error_ m_AwsCryptographyPrimitivesTypes.Error) m_Wrappers.Result { |
| 241 | + return m_Wrappers.Companion_Result_.Create_Failure_(error_) |
| 242 | +} |
| 243 | +func (_static *CompanionStruct_Default___) CreateAESDecryptExternSuccess(bytes _dafny.Sequence) m_Wrappers.Result { |
| 244 | + return m_Wrappers.Companion_Result_.Create_Success_(bytes) |
| 245 | +} |
| 246 | +func (_static *CompanionStruct_Default___) CreateAESDecryptExternFailure(error_ m_AwsCryptographyPrimitivesTypes.Error) m_Wrappers.Result { |
| 247 | + return m_Wrappers.Companion_Result_.Create_Failure_(error_) |
| 248 | +} |
| 249 | + |
| 250 | +// End of class Default__ |
0 commit comments