Skip to content

Commit bfc7cb9

Browse files
author
Shubham Chaturvedi
committed
feat: Check-in polymorph generated code
1 parent 798214b commit bfc7cb9

19 files changed

Lines changed: 10469 additions & 11 deletions

File tree

‎AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ECDH/externs.go‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ func (CompanionStruct_Default___) GenerateKeyPair(curveSpec AwsCryptographyPrimi
4444
}
4545

4646
func (CompanionStruct_Default___) CalculateSharedSecret(curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec,
47-
privateKeyInput AwsCryptographyPrimitivesTypes.ECCPrivateKey, publicKeyInput AwsCryptographyPrimitivesTypes.ECCPublicKey) Wrappers.Result {
47+
privateKeyInput AwsCryptographyPrimitivesTypes.ECCPrivateKey, publicKeyInput AwsCryptographyPrimitivesTypes.ECCPublicKey) Wrappers.Result {
4848

4949
curve, err := getNativeEcdhCurve(curveSpec)
5050
if err != nil {
@@ -112,7 +112,7 @@ func (CompanionStruct_Default___) CalculateSharedSecret(curveSpec AwsCryptograph
112112
}
113113

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

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

140140
func (CompanionStruct_Default___) DecompressPublicKey(publicKeyInput dafny.Sequence,
141-
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
141+
curveSpec AwsCryptographyPrimitivesTypes.ECDHCurveSpec) Wrappers.Result {
142142
publicKeyBytes := dafny.ToByteArray(publicKeyInput)
143143

144144
curve, err := getNativeEcdhCurve(curveSpec)

‎AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/RSAEncryption/externs.go‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ func (CompanionStruct_Default___) GenerateKeyPairExtern(bits int32) (dafny.Seque
3434
panic(err)
3535
}
3636
return dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PUBLIC KEY", Bytes: encodePublicKey})),
37-
dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PRIVATE KEY", Bytes: encodePrivateKey}))
37+
dafny.SeqOfBytes(pem.EncodeToMemory(&pem.Block{Type: "RSA PRIVATE KEY", Bytes: encodePrivateKey}))
3838
}
3939

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

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

9191
func (CompanionStruct_Default___) EncryptExtern(paddingMode AwsCryptographyPrimitivesTypes.RSAPaddingMode,
92-
key dafny.Sequence, plainText dafny.Sequence) Wrappers.Result {
92+
key dafny.Sequence, plainText dafny.Sequence) Wrappers.Result {
9393
derPublicKey, rest := pem.Decode(dafny.ToByteArray(key))
9494
if len(rest) > 0 {
9595
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(

‎AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/Signature/externs.go‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ func (CompanionStruct_Default___) ExternKeyGen(algorithm AwsCryptographyPrimitiv
4242
}
4343

4444
func (CompanionStruct_Default___) Sign(algorithm AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm,
45-
key dafny.Sequence, msg dafny.Sequence) Wrappers.Result {
45+
key dafny.Sequence, msg dafny.Sequence) Wrappers.Result {
4646
privateKey, err := x509.ParsePKCS8PrivateKey(dafny.ToByteArray(key))
4747
if err != nil {
4848
return Wrappers.Companion_Result_.Create_Failure_(AwsCryptographyPrimitivesTypes.Companion_Error_.Create_AwsCryptographicPrimitivesError_(
@@ -75,7 +75,7 @@ func (CompanionStruct_Default___) Sign(algorithm AwsCryptographyPrimitivesTypes.
7575
}
7676

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

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

116116
func getNativeEC(curveSpec AwsCryptographyPrimitivesTypes.ECDSASignatureAlgorithm) (elliptic.Curve,
117-
AwsCryptographyPrimitivesTypes.DigestAlgorithm, int, error) {
117+
AwsCryptographyPrimitivesTypes.DigestAlgorithm, int, error) {
118118
switch curveSpec {
119119
case AwsCryptographyPrimitivesTypes.Companion_ECDSASignatureAlgorithm_.Create_ECDSA__P256_():
120120
return elliptic.P256(), AwsCryptographyPrimitivesTypes.Companion_DigestAlgorithm_.Create_SHA__256_(), 71, nil

0 commit comments

Comments
 (0)