Skip to content

Add TestVectorModels: native Java data classes for test vector harness#2279

Draft
rishav-karanjit wants to merge 5 commits into
add-test-vector-nativelyfrom
rishav+ai/testvectorInJava/TestVectorModels
Draft

Add TestVectorModels: native Java data classes for test vector harness#2279
rishav-karanjit wants to merge 5 commits into
add-test-vector-nativelyfrom
rishav+ai/testvectorInJava/TestVectorModels

Conversation

@rishav-karanjit
Copy link
Copy Markdown
Member

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<K,V> → Map<K,V>
  • 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)

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

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<string> → nullable String (simpler for Java 8 target)
- Dafny seq<T> → List<T>, map<K,V> → Map<K,V>
- 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)
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<string> → nullable String (commented)
- Dafny seq<T> → List<T>, map<K,V> → Map<K,V>
- 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant