Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Check-in polymorph generated code #1130

Merged
merged 3 commits into from
Dec 17, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
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
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
Loading