Skip to content

Commit

Permalink
Move Java helper methods out of extern class
Browse files Browse the repository at this point in the history
  • Loading branch information
robin-aws committed Oct 11, 2024
1 parent 193be7a commit 326802c
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
import software.amazon.cryptography.primitives.internaldafny.types.Error;
import software.amazon.cryptography.primitives.model.AwsCryptographicPrimitivesError;

public class HMac extends _ExternBase_HMac {
public class HMac extends _ExternBase___default {

private String algorithm;
private Mac hmac;
Expand Down
16 changes: 9 additions & 7 deletions AwsCryptographyPrimitives/src/HKDF/HMAC.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -63,13 +63,7 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC {
// since their calling pattern is different between different versions of Dafny
// (i.e. after 4.2, explicit type descriptors are required).

static function CreateHMacSuccess(hmac: HMac): Result<HMac, Types.Error> {
Success(hmac)
}

static function CreateHMacFailure(error: Types.Error): Result<HMac, Types.Error> {
Failure(error)
}
}

// HMAC Digest is safe to make a Dafny function
Expand All @@ -78,11 +72,19 @@ module {:options "-functionSyntax:4"} {:extern "HMAC"} HMAC {
: ( output: Result<seq<uint8>, Types.Error> )
ensures output.Success? ==> |output.value| == HashDigest.Length(input.digestAlgorithm)

// The next two functions are for the benefit of the extern implementation to call,
// The following functions are for the benefit of the extern implementation to call,
// avoiding direct references to generic datatype constructors
// since their calling pattern is different between different versions of Dafny
// (i.e. after 4.2, explicit type descriptors are required).

function CreateHMacSuccess(hmac: HMac): Result<HMac, Types.Error> {
Success(hmac)
}

function CreateHMacFailure(error: Types.Error): Result<HMac, Types.Error> {
Failure(error)
}

function CreateDigestSuccess(bytes: seq<uint8>): Result<seq<uint8>, Types.Error> {
Success(bytes)
}
Expand Down

0 comments on commit 326802c

Please sign in to comment.