From 0f315b8b47f667960aaf7fe67b3f11d6b29a5ce6 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 14 May 2026 20:39:51 -0700 Subject: [PATCH 1/4] Add TestVectorModels: native Java data classes for test vector harness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What: Replaces Dafny-generated datatypes from JsonConfig_Compile (Record, LargeRecord, TableConfig, SimpleQuery, ComplexQuery, ComplexTest, IoTest, WriteTest, DecryptTest, RoundTripTest, ConfigPair) with idiomatic Java. Decisions: - Used public final fields instead of getters (test harness code, not public API) - Dafny Option → nullable String (simpler for Java 8 target) - Dafny seq → List, map → Map - Dafny nat (BigInteger) → int for Record.number (test vectors won't exceed int range) - Dafny ConfigName type alias → plain String - Dafny tuple (ConfigName, ConfigName) → ConfigPair class - DynamoDbTableEncryptionConfig references the native SDK model type directly - AttributeValue uses AWS SDK v2 type (software.amazon.awssdk.services.dynamodb.model) - Added TABLE_NAME and HASH_NAME constants (from Dafny source) Not included: JSON parsing logic, factory methods, test runners (future PRs) Verification: gradle compileJava passes (BUILD SUCCESSFUL) --- .../testvectors/TestVectorModels.java | 190 ++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java diff --git a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java new file mode 100644 index 0000000000..66f6dc859e --- /dev/null +++ b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java @@ -0,0 +1,190 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.cryptography.dbencryptionsdk.dynamodb.testvectors; + +import java.util.List; +import java.util.Map; +import software.amazon.awssdk.services.dynamodb.model.AttributeValue; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTableEncryptionConfig; + +/** + * Pure data classes used throughout the test vector harness. + * These replace the Dafny-generated datatypes from JsonConfig_Compile. + */ +public final class TestVectorModels { + + public static final String TABLE_NAME = "GazelleVectorTable"; + public static final String HASH_NAME = "RecNum"; + + private TestVectorModels() {} + + public static final class Record { + public final int number; + public final Map item; + + public Record(int number, Map item) { + this.number = number; + this.item = item; + } + } + + public static final class LargeRecord { + public final String name; + public final Map item; + + public LargeRecord(String name, Map item) { + this.name = name; + this.item = item; + } + } + + public static final class TableConfig { + public final String name; + public final DynamoDbTableEncryptionConfig config; + public final boolean vanilla; + + public TableConfig( + String name, + DynamoDbTableEncryptionConfig config, + boolean vanilla + ) { + this.name = name; + this.config = config; + this.vanilla = vanilla; + } + } + + public static final class SimpleQuery { + public final String index; // nullable + public final String keyExpr; // nullable + public final String filterExpr; // nullable + public final List failConfigs; + + public SimpleQuery( + String index, + String keyExpr, + String filterExpr, + List failConfigs + ) { + this.index = index; + this.keyExpr = keyExpr; + this.filterExpr = filterExpr; + this.failConfigs = failConfigs; + } + } + + public static final class ComplexQuery { + public final SimpleQuery query; + public final List pass; + public final List fail; + + public ComplexQuery( + SimpleQuery query, + List pass, + List fail + ) { + this.query = query; + this.pass = pass; + this.fail = fail; + } + } + + public static final class ComplexTest { + public final String config; + public final List queries; + public final List failures; + + public ComplexTest( + String config, + List queries, + List failures + ) { + this.config = config; + this.queries = queries; + this.failures = failures; + } + } + + public static final class RoundTripTest { + public final Map configs; + public final List records; + + public RoundTripTest( + Map configs, + List records + ) { + this.configs = configs; + this.records = records; + } + } + + public static final class WriteTest { + public final TableConfig config; + public final List records; + public final String fileName; + + public WriteTest( + TableConfig config, + List records, + String fileName + ) { + this.config = config; + this.records = records; + this.fileName = fileName; + } + } + + public static final class DecryptTest { + public final TableConfig config; + public final List encryptedRecords; + public final List plaintextRecords; + + public DecryptTest( + TableConfig config, + List encryptedRecords, + List plaintextRecords + ) { + this.config = config; + this.encryptedRecords = encryptedRecords; + this.plaintextRecords = plaintextRecords; + } + } + + public static final class IoTest { + public final String name; + public final TableConfig writeConfig; + public final TableConfig readConfig; + public final List records; + public final Map names; + public final Map values; + public final List queries; + + public IoTest( + String name, + TableConfig writeConfig, + TableConfig readConfig, + List records, + Map names, + Map values, + List queries + ) { + this.name = name; + this.writeConfig = writeConfig; + this.readConfig = readConfig; + this.records = records; + this.names = names; + this.values = values; + this.queries = queries; + } + } + + public static final class ConfigPair { + public final String first; + public final String second; + + public ConfigPair(String first, String second) { + this.first = first; + this.second = second; + } + } +} From d8f92216d782d6f69d45abe24afcfea19c370945 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Thu, 14 May 2026 20:39:51 -0700 Subject: [PATCH 2/4] Add TestVectorModels: native Java data classes for test vector harness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What: Replaces Dafny-generated datatypes from JsonConfig_Compile (Record, LargeRecord, TableConfig, SimpleQuery, ComplexQuery, ComplexTest, IoTest, WriteTest, DecryptTest, RoundTripTest, ConfigPair) with idiomatic Java. Decisions: - Used public final fields (test harness code, not public API) - Dafny Option → nullable String (commented) - Dafny seq → List, map → Map - Dafny nat (BigInteger) → int for Record.number - Dafny ConfigName type alias → plain String - Dafny tuple (ConfigName, ConfigName) → ConfigPair class - DynamoDbTableEncryptionConfig references the native SDK model type directly - AttributeValue uses AWS SDK v2 type - All collections defensively copied (Collections.unmodifiableList/Map) - Objects.requireNonNull on all required fields - equals/hashCode on Record and TableConfig (used in assertions) - Java 8 compatible (no List.copyOf, no records, no @Nullable annotation) Not included: JSON parsing logic, factory methods, test runners (future PRs) Verification: gradle compileJava passes (BUILD SUCCESSFUL) --- .../testvectors/TestVectorModels.java | 238 ++++++++++++++++++ 1 file changed, 238 insertions(+) create mode 100644 TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java diff --git a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java new file mode 100644 index 0000000000..392fc7e715 --- /dev/null +++ b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java @@ -0,0 +1,238 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +package software.amazon.cryptography.dbencryptionsdk.dynamodb.testvectors; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import software.amazon.awssdk.services.dynamodb.model.AttributeValue; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTableEncryptionConfig; + +/** + * Replacement for Dafny-generated test vector model types. + * All collections are defensively copied to unmodifiable forms. + */ +public final class TestVectorModels { + + public static final String TABLE_NAME = "GazelleVectorTable"; + public static final String HASH_NAME = "RecNum"; + + private TestVectorModels() {} + + public static final class Record { + public final int number; + public final Map item; + + public Record(int number, Map item) { + this.number = number; + this.item = unmodifiableMap(Objects.requireNonNull(item, "item")); + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (!(o instanceof Record)) return false; + Record r = (Record) o; + return number == r.number && item.equals(r.item); + } + + @Override + public int hashCode() { + return 31 * number + item.hashCode(); + } + } + + public static final class LargeRecord { + public final String name; + public final Map item; + + public LargeRecord(String name, Map item) { + this.name = Objects.requireNonNull(name, "name"); + this.item = unmodifiableMap(Objects.requireNonNull(item, "item")); + } + } + + public static final class TableConfig { + public final String name; + public final DynamoDbTableEncryptionConfig config; // null when vanilla == true + public final boolean vanilla; + + public TableConfig( + String name, + DynamoDbTableEncryptionConfig config, + boolean vanilla + ) { + this.name = Objects.requireNonNull(name, "name"); + this.config = config; + this.vanilla = vanilla; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (!(o instanceof TableConfig)) return false; + TableConfig t = (TableConfig) o; + return vanilla == t.vanilla + && name.equals(t.name) + && Objects.equals(config, t.config); + } + + @Override + public int hashCode() { + int h = name.hashCode(); + h = 31 * h + (config != null ? config.hashCode() : 0); + h = 31 * h + Boolean.hashCode(vanilla); + return h; + } + } + + public static final class SimpleQuery { + public final String index; // nullable + public final String keyExpr; // nullable + public final String filterExpr; // nullable + public final List failConfigs; + + public SimpleQuery( + String index, + String keyExpr, + String filterExpr, + List failConfigs + ) { + this.index = index; + this.keyExpr = keyExpr; + this.filterExpr = filterExpr; + this.failConfigs = unmodifiableList( + Objects.requireNonNull(failConfigs, "failConfigs")); + } + } + + public static final class ComplexQuery { + public final SimpleQuery query; + public final List pass; + public final List fail; + + public ComplexQuery( + SimpleQuery query, + List pass, + List fail + ) { + this.query = Objects.requireNonNull(query, "query"); + this.pass = unmodifiableList(Objects.requireNonNull(pass, "pass")); + this.fail = unmodifiableList(Objects.requireNonNull(fail, "fail")); + } + } + + public static final class ComplexTest { + public final String config; + public final List queries; + public final List failures; + + public ComplexTest( + String config, + List queries, + List failures + ) { + this.config = Objects.requireNonNull(config, "config"); + this.queries = unmodifiableList(Objects.requireNonNull(queries, "queries")); + this.failures = unmodifiableList(Objects.requireNonNull(failures, "failures")); + } + } + + public static final class RoundTripTest { + public final Map configs; + public final List records; + + public RoundTripTest( + Map configs, + List records + ) { + this.configs = unmodifiableMap(Objects.requireNonNull(configs, "configs")); + this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + } + } + + public static final class WriteTest { + public final TableConfig config; + public final List records; + public final String fileName; + + public WriteTest( + TableConfig config, + List records, + String fileName + ) { + this.config = Objects.requireNonNull(config, "config"); + this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + this.fileName = Objects.requireNonNull(fileName, "fileName"); + } + } + + public static final class DecryptTest { + public final TableConfig config; + public final List encryptedRecords; + public final List plaintextRecords; + + public DecryptTest( + TableConfig config, + List encryptedRecords, + List plaintextRecords + ) { + this.config = Objects.requireNonNull(config, "config"); + this.encryptedRecords = unmodifiableList( + Objects.requireNonNull(encryptedRecords, "encryptedRecords")); + this.plaintextRecords = unmodifiableList( + Objects.requireNonNull(plaintextRecords, "plaintextRecords")); + } + } + + public static final class IoTest { + public final String name; + public final TableConfig writeConfig; + public final TableConfig readConfig; + public final List records; + public final Map names; + public final Map values; + public final List queries; + + public IoTest( + String name, + TableConfig writeConfig, + TableConfig readConfig, + List records, + Map names, + Map values, + List queries + ) { + this.name = Objects.requireNonNull(name, "name"); + this.writeConfig = Objects.requireNonNull(writeConfig, "writeConfig"); + this.readConfig = Objects.requireNonNull(readConfig, "readConfig"); + this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + this.names = unmodifiableMap(Objects.requireNonNull(names, "names")); + this.values = unmodifiableMap(Objects.requireNonNull(values, "values")); + this.queries = unmodifiableList(Objects.requireNonNull(queries, "queries")); + } + } + + public static final class ConfigPair { + public final String first; + public final String second; + + public ConfigPair(String first, String second) { + this.first = Objects.requireNonNull(first, "first"); + this.second = Objects.requireNonNull(second, "second"); + } + } + + // Java 8 compatible defensive copy helpers + + private static List unmodifiableList(List src) { + return Collections.unmodifiableList(new ArrayList<>(src)); + } + + private static Map unmodifiableMap(Map src) { + return Collections.unmodifiableMap(new HashMap<>(src)); + } +} From 4507d6075a67a5a75ffa404905d8aac53f12ca73 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 15 May 2026 09:20:21 -0700 Subject: [PATCH 3/4] m --- .../testvectors/TestVectorModels.java | 62 +++++++++++++------ 1 file changed, 43 insertions(+), 19 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java index 392fc7e715..46ec63def0 100644 --- a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java +++ b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java @@ -23,6 +23,7 @@ public final class TestVectorModels { private TestVectorModels() {} public static final class Record { + public final int number; public final Map item; @@ -46,6 +47,7 @@ public int hashCode() { } public static final class LargeRecord { + public final String name; public final Map item; @@ -56,6 +58,7 @@ public LargeRecord(String name, Map item) { } public static final class TableConfig { + public final String name; public final DynamoDbTableEncryptionConfig config; // null when vanilla == true public final boolean vanilla; @@ -75,9 +78,11 @@ public boolean equals(Object o) { if (this == o) return true; if (!(o instanceof TableConfig)) return false; TableConfig t = (TableConfig) o; - return vanilla == t.vanilla - && name.equals(t.name) - && Objects.equals(config, t.config); + return ( + vanilla == t.vanilla && + name.equals(t.name) && + Objects.equals(config, t.config) + ); } @Override @@ -90,9 +95,10 @@ public int hashCode() { } public static final class SimpleQuery { - public final String index; // nullable - public final String keyExpr; // nullable - public final String filterExpr; // nullable + + public final String index; // nullable + public final String keyExpr; // nullable + public final String filterExpr; // nullable public final List failConfigs; public SimpleQuery( @@ -104,12 +110,13 @@ public SimpleQuery( this.index = index; this.keyExpr = keyExpr; this.filterExpr = filterExpr; - this.failConfigs = unmodifiableList( - Objects.requireNonNull(failConfigs, "failConfigs")); + this.failConfigs = + unmodifiableList(Objects.requireNonNull(failConfigs, "failConfigs")); } } public static final class ComplexQuery { + public final SimpleQuery query; public final List pass; public final List fail; @@ -126,6 +133,7 @@ public ComplexQuery( } public static final class ComplexTest { + public final String config; public final List queries; public final List failures; @@ -136,12 +144,15 @@ public ComplexTest( List failures ) { this.config = Objects.requireNonNull(config, "config"); - this.queries = unmodifiableList(Objects.requireNonNull(queries, "queries")); - this.failures = unmodifiableList(Objects.requireNonNull(failures, "failures")); + this.queries = + unmodifiableList(Objects.requireNonNull(queries, "queries")); + this.failures = + unmodifiableList(Objects.requireNonNull(failures, "failures")); } } public static final class RoundTripTest { + public final Map configs; public final List records; @@ -149,12 +160,15 @@ public RoundTripTest( Map configs, List records ) { - this.configs = unmodifiableMap(Objects.requireNonNull(configs, "configs")); - this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + this.configs = + unmodifiableMap(Objects.requireNonNull(configs, "configs")); + this.records = + unmodifiableList(Objects.requireNonNull(records, "records")); } } public static final class WriteTest { + public final TableConfig config; public final List records; public final String fileName; @@ -165,12 +179,14 @@ public WriteTest( String fileName ) { this.config = Objects.requireNonNull(config, "config"); - this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + this.records = + unmodifiableList(Objects.requireNonNull(records, "records")); this.fileName = Objects.requireNonNull(fileName, "fileName"); } } public static final class DecryptTest { + public final TableConfig config; public final List encryptedRecords; public final List plaintextRecords; @@ -181,14 +197,19 @@ public DecryptTest( List plaintextRecords ) { this.config = Objects.requireNonNull(config, "config"); - this.encryptedRecords = unmodifiableList( - Objects.requireNonNull(encryptedRecords, "encryptedRecords")); - this.plaintextRecords = unmodifiableList( - Objects.requireNonNull(plaintextRecords, "plaintextRecords")); + this.encryptedRecords = + unmodifiableList( + Objects.requireNonNull(encryptedRecords, "encryptedRecords") + ); + this.plaintextRecords = + unmodifiableList( + Objects.requireNonNull(plaintextRecords, "plaintextRecords") + ); } } public static final class IoTest { + public final String name; public final TableConfig writeConfig; public final TableConfig readConfig; @@ -209,14 +230,17 @@ public IoTest( this.name = Objects.requireNonNull(name, "name"); this.writeConfig = Objects.requireNonNull(writeConfig, "writeConfig"); this.readConfig = Objects.requireNonNull(readConfig, "readConfig"); - this.records = unmodifiableList(Objects.requireNonNull(records, "records")); + this.records = + unmodifiableList(Objects.requireNonNull(records, "records")); this.names = unmodifiableMap(Objects.requireNonNull(names, "names")); this.values = unmodifiableMap(Objects.requireNonNull(values, "values")); - this.queries = unmodifiableList(Objects.requireNonNull(queries, "queries")); + this.queries = + unmodifiableList(Objects.requireNonNull(queries, "queries")); } } public static final class ConfigPair { + public final String first; public final String second; From 71c98790fe3556e1725032487e9a4131601aeb83 Mon Sep 17 00:00:00 2001 From: rishav-karanjit Date: Fri, 15 May 2026 09:23:39 -0700 Subject: [PATCH 4/4] m --- .../dynamodb/testvectors/TestVectorModels.java | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java index 2ea7fd978f..2c608dabd2 100644 --- a/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java +++ b/TestVectors/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/testvectors/TestVectorModels.java @@ -108,20 +108,12 @@ public SimpleQuery( this.index = index; this.keyExpr = keyExpr; this.filterExpr = filterExpr; -<<<<<<< HEAD this.failConfigs = unmodifiableList(Objects.requireNonNull(failConfigs, "failConfigs")); -======= - this.failConfigs = failConfigs; ->>>>>>> 0f315b8b47f667960aaf7fe67b3f11d6b29a5ce6 } } public static final class ComplexQuery { -<<<<<<< HEAD - -======= ->>>>>>> 0f315b8b47f667960aaf7fe67b3f11d6b29a5ce6 public final SimpleQuery query; public final List pass; public final List fail; @@ -188,10 +180,6 @@ public WriteTest( } public static final class DecryptTest { -<<<<<<< HEAD - -======= ->>>>>>> 0f315b8b47f667960aaf7fe67b3f11d6b29a5ce6 public final TableConfig config; public final List encryptedRecords; public final List plaintextRecords;