Skip to content

Commit

Permalink
Merge pull request #1130 from aws/Golang/Primitives
Browse files Browse the repository at this point in the history 
feat: Check-in polymorph generated code
  • Loading branch information
@ShubhamChaturvedi7
ShubhamChaturvedi7 authored Dec 17, 2024
2 parents b6ee16e + 430dd49 commit 6477639
Show file tree
Hide file tree
Showing 19 changed files with 10,469 additions and 11 deletions.
6 changes: 3 additions & 3 deletions AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ECDH/externs.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ func (CompanionStruct_Default___) GenerateKeyPair(curveSpec AwsCryptographyPrimi
}

func (CompanionStruct_Default___) CalculateSharedSecret(curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec,
privateKeyInput AwsCryptographyPrimitivesTypes.ECCPrivateKey, publicKeyInput AwsCryptographyPrimitivesTypes.ECCPublicKey) Wrappers.Result {
privateKeyInput AwsCryptographyPrimitivesTypes.ECCPrivateKey, publicKeyInput AwsCryptographyPrimitivesTypes.ECCPublicKey) Wrappers.Result {

curve, err := getNativeEcdhCurve(curveSpec)
if err != nil {
Expand Down Expand Up @@ -112,7 +112,7 @@ func (CompanionStruct_Default___) CalculateSharedSecret(curveSpec AwsCryptograph
}

func (static CompanionStruct_Default___) CompressPublicKey(publicKeyInput dafny.Sequence,
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
// We only need this because elliptic.MarshalCompressed() doesn't return err handle and panics, so to avoid panic we pre-validate the key.
validate := static.ValidatePublicKey(curveSpec, publicKeyInput)

Expand All @@ -138,7 +138,7 @@ func (static CompanionStruct_Default___) CompressPublicKey(publicKeyInput dafny.
}

func (CompanionStruct_Default___) DecompressPublicKey(publicKeyInput dafny.Sequence,
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
publicKeyBytes := dafny.ToByteArray(publicKeyInput)

curve, err := getNativeEcdhCurve(curveSpec)
Expand Down
6 changes: 3 additions & 3 deletions AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/RSAEncryption/externs.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ func (CompanionStruct_Default___) GenerateKeyPairExtern(bits int32) (dafny.Seque
panic(err)
}
return dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PUBLIC KEY", Bytes: encodePublicKey})),
dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PRIVATE KEY", Bytes: encodePrivateKey}))
dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PRIVATE KEY", Bytes: encodePrivateKey}))
}

func (m_RSAEncryption_Ghost) RSA_GetRSAKeyModulusLengthExtern(publicKeyInput dafny.Sequence) Wrappers.Result {
Expand All @@ -52,7 +52,7 @@ func (m_RSAEncryption_Ghost) RSA_GetRSAKeyModulusLengthExtern(publicKeyInput daf
}

func (CompanionStruct_Default___) DecryptExtern(paddingMode AwsCryptographyPrimitivesTypes.RSAPaddingMode,
key dafny.Sequence, cipher_text dafny.Sequence) Wrappers.Result {
key dafny.Sequence, cipher_text dafny.Sequence) Wrappers.Result {
derPrivateKey, rest := pem.Decode(dafny.ToByteArray(key))
if len(rest) > 0 {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
Expand Down Expand Up @@ -89,7 +89,7 @@ func (CompanionStruct_Default___) DecryptExtern(paddingMode AwsCryptographyPrimi
}

func (CompanionStruct_Default___) EncryptExtern(paddingMode AwsCryptographyPrimitivesTypes.RSAPaddingMode,
key dafny.Sequence, plainText dafny.Sequence) Wrappers.Result {
key dafny.Sequence, plainText dafny.Sequence) Wrappers.Result {
derPublicKey, rest := pem.Decode(dafny.ToByteArray(key))
if len(rest) > 0 {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
Expand Down
10 changes: 5 additions & 5 deletions AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/Signature/externs.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ func (CompanionStruct_Default___) ExternKeyGen(algorithm AwsCryptographyPrimitiv
}

func (CompanionStruct_Default___) Sign(algorithm AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm,
key dafny.Sequence, msg dafny.Sequence) Wrappers.Result {
key dafny.Sequence, msg dafny.Sequence) Wrappers.Result {
privateKey, err := x509.ParsePKCS8PrivateKey(dafny.ToByteArray(key))
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
Expand Down Expand Up @@ -75,7 +75,7 @@ func (CompanionStruct_Default___) Sign(algorithm AwsCryptographyPrimitivesTypes.
}

func ECDSA_Verify(algorithm AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm, key dafny.Sequence,
msg dafny.Sequence, sig dafny.Sequence) Wrappers.Result {
msg dafny.Sequence, sig dafny.Sequence) Wrappers.Result {
curve, digestAlgo, _, err := getNativeEC(algorithm)
if err != nil {
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
Expand All @@ -92,8 +92,8 @@ func ECDSA_Verify(algorithm AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorit
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
dafny.SeqOfChars([]dafny.Char("Failed to decompress verification key")...)))
}
res := ecdsa.VerifyASN1(&ecdsa.PublicKey{Curve: curve, X: x, Y: y},dafny.ToByteArray(msgDigest.Dtor_value().(dafny.Sequence)),
dafny.ToByteArray(sig))
res := ecdsa.VerifyASN1(&ecdsa.PublicKey{Curve: curve, X: x, Y: y}, dafny.ToByteArray(msgDigest.Dtor_value().(dafny.Sequence)),
dafny.ToByteArray(sig))

return Wrappers.Companion_Result_.Create_Success_(res)
}
Expand All @@ -114,7 +114,7 @@ func generateKeyPair(curve elliptic.Curve) ([]byte, []byte, error) {
}

func getNativeEC(curveSpec AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm) (elliptic.Curve,
AwsCryptographyPrimitivesTypes.DigestAlgorithm, int, error) {
AwsCryptographyPrimitivesTypes.DigestAlgorithm, int, error) {
switch curveSpec {
case AwsCryptographyPrimitivesTypes.Companion_ECDSASignatureAlgorithm_.Create_ECDSA__P256_():
return elliptic.P256(), AwsCryptographyPrimitivesTypes.Companion_DigestAlgorithm_.Create_SHA__256_(), 71, nil
Expand Down
Loading

0 comments on commit 6477639

Please sign in to comment.