Skip to content

Commit

Permalink
fix: line breaks
Browse files Browse the repository at this point in the history
  • Loading branch information
Shubham Chaturvedi committed Dec 12, 2024
1 parent 34a48fc commit 21536c7
Show file tree
Hide file tree
Showing 6 changed files with 157 additions and 77 deletions.
44 changes: 30 additions & 14 deletions AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/AESEncryption/externs.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,76 +14,92 @@ var m_AESEncryption struct {
AES_GCM CompanionStruct_Default___
}

func (CompanionStruct_Default___) AESDecryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, key dafny.Sequence, cipherText dafny.Sequence, authTag dafny.Sequence, iv dafny.Sequence, aad dafny.Sequence) Wrappers.Result {
func (CompanionStruct_Default___) AESDecryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, key dafny.Sequence,
cipherText dafny.Sequence, authTag dafny.Sequence, iv dafny.Sequence, aad dafny.Sequence) Wrappers.Result {

keyBytes := dafny.ToByteArray(key)
cipherTextBytes := dafny.ToByteArray(cipherText)
authTagBytes := dafny.ToByteArray(authTag)
ivBytes := dafny.ToByteArray(iv)
aadBytes := dafny.ToByteArray(aad)

if algo.Dtor_keyLength() != int32(len(keyBytes)) {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...)))

}

if algo.Dtor_ivLength() != int32(len(ivBytes)) {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...)))
}

if algo.Dtor_tagLength() != int32(len(authTagBytes)) {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm tag length %d doesn't match actual tag length %d ", algo.Dtor_tagLength(), len(authTagBytes)).Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm tag length %d doesn't match actual tag length %d ", algo.Dtor_tagLength(), len(authTagBytes)).Error())...)))
}

block, err := aes.NewCipher(keyBytes)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(err.Error())...)))
}

if algo.Is_AES__GCM() {
gcm, err := cipher.NewGCM(block)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(err.Error())...)))
}

plaintext, err := gcm.Open(nil, ivBytes, append(cipherTextBytes, authTagBytes...), aadBytes)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(err.Error())...)))
}
return Wrappers.Companion_Result_.Create_Success_(dafny.SeqOfBytes(plaintext))
}
return Wrappers.Companion_Result_.Create_Failure_(false)
}

func (CompanionStruct_Default___) AESEncryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, iv dafny.Sequence, key dafny.Sequence, msg dafny.Sequence, aad dafny.Sequence) Wrappers.Result {
func (CompanionStruct_Default___) AESEncryptExtern(algo AwsCryptographyPrimitivesTypes.AES__GCM, iv dafny.Sequence,
key dafny.Sequence, msg dafny.Sequence, aad dafny.Sequence) Wrappers.Result {

keyBytes := dafny.ToByteArray(key)
ivBytes := dafny.ToByteArray(iv)
aadBytes := dafny.ToByteArray(aad)

if algo.Dtor_keyLength() != int32(len(keyBytes)) {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm key length %d doesn't match actual key length %d ", algo.Dtor_keyLength(), len(keyBytes)).Error())...)))

}

if algo.Dtor_ivLength() != int32(len(ivBytes)) {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("algorithm iv length %d doesn't match actual iv length %d ", algo.Dtor_ivLength(), len(ivBytes)).Error())...)))
}

block, err := aes.NewCipher(keyBytes)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(err.Error())...)))
}

if algo.Is_AES__GCM() {
gcm, err := cipher.NewGCM(block)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(err.Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(err.Error())...)))
}

cipherText := gcm.Seal(nil, ivBytes, dafny.ToByteArray(msg), aadBytes)
if cipherText == nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(dafny.SeqOfChars([]dafny.Char(fmt.Errorf("failed to do AES_GCM Encrypt with the given parameters").Error())...)))
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char(fmt.Errorf("failed to do AES_GCM Encrypt with the given parameters").Error())...)))
}
return Wrappers.Companion_Result_.Create_Success_(AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Create_AESEncryptOutput_(dafny.SeqOfBytes(cipherText[:len(cipherText)-gcm.Overhead()]), dafny.SeqOfBytes(cipherText[len(cipherText)-gcm.Overhead():])))
return Wrappers.Companion_Result_.Create_Success_(AwsCryptographyPrimitivesTypes.Companion_AESEncryptOutput_.Create_AESEncryptOutput_(
dafny.SeqOfBytes(cipherText[:len(cipherText)-gcm.Overhead()]), dafny.SeqOfBytes(cipherText[len(cipherText)-gcm.Overhead():])))
}
return Wrappers.Companion_Result_.Create_Failure_(false)
}
Loading

0 comments on commit 21536c7

Please sign in to comment.