[Draft] Support package-prefixed NET/Java code

SmithyDafnyMakefile.mk

@@ -154,7 +154,7 @@ clean-dafny-report:
 # Transpile the entire project's impl
 # For each index file listed in the project Makefile's PROJECT_INDEX variable,
 #   append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target
-_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
+_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
 _transpile_implementation_all: transpile_implementation
 
 # The `$(OUT)` and $(TARGET) variables are problematic.
@@ -189,22 +189,21 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src
 # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_implementation:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(DAFNY_OPTIONS) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+	translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(TRANSPILE_MODULE_NAME) \
+		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		$(TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES)
 
+
 # If the project under transpilation uses `replaceable` modules,
 #   it MUST define a SRC_INDEX variable per language.
 # The purpose and usage of this is described in the `transpile_implementation` comments.
@@ -222,27 +221,26 @@ _transpile_test_all: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
 #     append `-library:/path/to/Index.dfy` to the transpile target
 # Else: (i.e. single model/service in project), then:
 #   append `-library:/path/to/Index.dfy` to the transpile target
-_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, -library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), -library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
+_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, --library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), --library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
 # Transpile the entire project's tests
 _transpile_test_all: transpile_test
 
 # `find` looks for tests in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_test:
 	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-runAllTests:1 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--include-test-runner \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		$(TRANSLATION_RECORD) \
+		$(SOURCE_TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES) \
 
 # If we are not the StandardLibrary, transpile the StandardLibrary.
@@ -275,10 +273,12 @@ _polymorph:
 	$(OUTPUT_JAVA) \
 	$(OUTPUT_JAVA_TEST) \
 	$(OUTPUT_DOTNET) \
+	$(MODULE_NAME) \
 	$(OUTPUT_RUST) \
 	--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \
 	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
 	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	$(DEPENDENCY_MODULE_NAMES) \
 	--namespace $($(namespace_var)) \
 	$(OUTPUT_LOCAL_SERVICE_$(SERVICE)) \
 	$(AWS_SDK_CMD) \
@@ -292,13 +292,14 @@ _polymorph_wrapped:
 	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--properties-file $(LIBRARY_ROOT)/project.properties \
-	$(INPUT_DAFNY) \
 	$(OUTPUT_DAFNY_WRAPPED) \
 	$(OUTPUT_DOTNET_WRAPPED) \
 	$(OUTPUT_JAVA_WRAPPED) \
+	$(MODULE_NAME) \
 	--model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \
 	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
 	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	$(DEPENDENCY_MODULE_NAMES) \
 	--namespace $($(namespace_var)) \
 	--local-service-test \
 	$(AWS_SDK_CMD) \
@@ -369,8 +370,6 @@ polymorph_dotnet:
 
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
-_polymorph_dotnet: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_dotnet: _polymorph
 
 # Generates java code for all namespaces in this project
@@ -387,8 +386,6 @@ polymorph_java:
 
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
-_polymorph_java: INPUT_DAFNY=\
-	--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_java: _polymorph
 
 # Dependency for formatting generating Java code
@@ -419,13 +416,17 @@ transpile_net: | transpile_implementation_net transpile_test_net transpile_depen
 
 transpile_implementation_net: TARGET=cs
 transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny
+transpile_implementation_net: TRANSPILE_MODULE_NAME=$(if $(NET_NAMESPACE_NAME),--dotnet-namespace=$(NET_NAMESPACE_NAME).internaldafny,)
+transpile_implementation_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET)
 transpile_implementation_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_implementation_net: _transpile_implementation_all
 
 transpile_test_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_test_net: TEST_INDEX=$(NET_TEST_INDEX)
 transpile_test_net: TARGET=cs
 transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny
+transpile_test_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET)
+transpile_test_net: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/net/ImplementationFromDafny-cs.dtr
 transpile_test_net: _transpile_test_all
 
 transpile_dependencies_net: LANG=net
@@ -467,10 +468,14 @@ transpile_java: | transpile_implementation_java transpile_test_java transpile_de
 
 transpile_implementation_java: TARGET=java
 transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny
+transpile_implementation_java: TRANSPILE_MODULE_NAME=$(if $(JAVA_PACKAGE_NAME),--java-package-name=$(JAVA_PACKAGE_NAME).internaldafny,)
+transpile_implementation_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA)
 transpile_implementation_java: _transpile_implementation_all _mv_implementation_java
 
 transpile_test_java: TARGET=java
 transpile_test_java: OUT=runtimes/java/TestsFromDafny
+transpile_test_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA)
+transpile_test_java: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr
 transpile_test_java: _transpile_test_all _mv_test_java
 
 # Currently Dafny compiles to Java by changing the directory name.

TestModels/Constraints/Makefile

@@ -24,3 +24,17 @@ polymorph:
 	make polymorph_dafny
 	make polymorph_java
 	make polymorph_dotnet
+
+# Java
+
+JAVA_PACKAGE_NAME=simple.constraints
+
+TRANSLATION_RECORD_JAVA:= \
+    --translation-record ../dafny-dependencies/StandardLibrary/runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr
+
+# NET
+
+NET_NAMESPACE_NAME=simple.constraints
+
+TRANSLATION_RECORD_NET:= \
+    --translation-record ../dafny-dependencies/StandardLibrary/runtimes/net/ImplementationFromDafny-cs.dtr

TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java

@@ -0,0 +1,33 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+package WrappedSimpleConstraintsService;
+
+import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result;
+import simple.constraints.SimpleConstraints;
+import simple.constraints.ToNative;
+import simple.constraints.internaldafny.types.Error;
+import simple.constraints.internaldafny.types.ISimpleConstraintsClient;
+import simple.constraints.internaldafny.types.SimpleConstraintsConfig;
+import simple.constraints.wrapped.TestSimpleConstraints;
+
+public class __default extends _ExternBase___default {
+
+  public static Result<
+    ISimpleConstraintsClient,
+    Error
+  > WrappedSimpleConstraints(SimpleConstraintsConfig config) {
+    simple.constraints.model.SimpleConstraintsConfig wrappedConfig =
+      ToNative.SimpleConstraintsConfig(config);
+    simple.constraints.SimpleConstraints impl = SimpleConstraints
+      .builder()
+      .SimpleConstraintsConfig(wrappedConfig)
+      .build();
+    TestSimpleConstraints wrappedClient = TestSimpleConstraints
+      .builder()
+      .impl(impl)
+      .build();
+    return simple.constraints.internaldafny.SimpleConstraints.__default.CreateSuccessOfClient(
+      wrappedClient
+    );
+  }
+}

TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs

@@ -1,17 +1,20 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-using Wrappers_Compile;
+using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers;
+using simple.constraints.internaldafny.types;
 using Simple.Constraints;
 using Simple.Constraints.Wrapped;
-using TypeConversion = Simple.Constraints.TypeConversion ;
-namespace simple.constraints.internaldafny.wrapped
+using TypeConversion = Simple.Constraints.TypeConversion;
+namespace WrappedSimpleConstraintsService
 {
-    public partial class __default {
-        public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) {
+    public partial class __default
+    {
+        public static _IResult<simple.constraints.internaldafny.types.ISimpleConstraintsClient, simple.constraints.internaldafny.types._IError> WrappedSimpleConstraints(simple.constraints.internaldafny.types._ISimpleConstraintsConfig config)
+        {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config);
-            var impl = new SimpleConstraints(wrappedConfig);
+            var impl = new Simple.Constraints.SimpleConstraints(wrappedConfig);
             var wrappedClient = new SimpleConstraintsShim(impl);
-            return Result<types.ISimpleConstraintsClient, types._IError>.create_Success(wrappedClient);
+            return Result<simple.constraints.internaldafny.types.ISimpleConstraintsClient, simple.constraints.internaldafny.types._IError>.create_Success(wrappedClient);
         }
     }
 }

TestModels/Constraints/src/Index.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "SimpleConstraintsImpl.dfy"
 
-module {:extern "simple.constraints.internaldafny" } SimpleConstraints refines AbstractSimpleConstraintsService {
+module {:extern "SimpleConstraints" } SimpleConstraints refines AbstractSimpleConstraintsService {
   import Operations = SimpleConstraintsImpl
 
   function method DefaultSimpleConstraintsConfig(): SimpleConstraintsConfig {

TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "../Model/SimpleConstraintsTypesWrapped.dfy"
 
-module {:extern "simple.constraints.internaldafny.wrapped"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {
+module {:extern "WrappedSimpleConstraintsService"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {
     import WrappedService = SimpleConstraints
     function method WrappedDefaultSimpleConstraintsConfig(): SimpleConstraintsConfig {
         SimpleConstraintsConfig

TestModels/dafny-dependencies/StandardLibrary/Makefile

@@ -6,6 +6,8 @@ CORES=2
 include ../../SharedMakefile.mk
 
 MAX_RESOURCE_COUNT=500000000
+JAVA_PACKAGE_NAME=software.amazon.cryptography.standardlibrary
+NET_NAMESPACE_NAME=software.amazon.cryptography.standardlibrary
 
 # define standard colors
 ifneq (,$(findstring xterm,${TERM}))
@@ -86,21 +88,19 @@ transpile_dependencies:
 
 # Override SharedMakefile's transpile_implementation to not reference
 # StandardLibrary as a Library
+transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
 transpile_implementation:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		$(DAFNY_OPTIONS) \
-		-out $(OUT)
+	translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(TRANSPILE_MODULE_NAME)
 
 # Override SharedMakefile's build_java to not install
 # StandardLibrary as a dependency

TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java

@@ -1,13 +1,13 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-package UTF8;
+package software.amazon.cryptography.standardlibrary.internaldafny.UTF8;
 
 import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence;
 import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence;
 import static software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer;
 import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String;
 
-import Wrappers_Compile.Result;
+import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result;
 import dafny.DafnySequence;
 import java.nio.ByteBuffer;
 import java.nio.CharBuffer;
@@ -22,7 +22,7 @@
 // If we wanted to increase performance,
 // we could declare this NOT thread/concurrent safe,
 // and reset the coder everytime.
-public class __default extends UTF8._ExternBase___default {
+public class __default extends _ExternBase___default {
 
   // This is largely copied from Polymorph's dafny-java-conversion:
   // software.amazon.smithy.dafny.conversion.ToDafny.Simple.DafnyUtf8Bytes

TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs

@@ -4,13 +4,13 @@
 using System;
 using System.Text;
 
-using Wrappers_Compile;
+using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers;
 using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
 using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;
 
-namespace UTF8 {
+namespace software.amazon.cryptography.standardlibrary.internaldafny.UTF8 {
     public partial class __default {
         public static _IResult<ibyteseq, icharseq> Encode(icharseq str) {
             UTF8Encoding utf8 = new UTF8Encoding(false, true);

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java

@@ -129,10 +129,7 @@ public Map<Path, TokenTree> generate() {
       namespace
     );
     final TokenTree typesModuleHeader = Token.of(
-      "module {:extern \"%s\" } %s".formatted(
-          DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId(
-            serviceShape.getId()
-          ),
+      "module {:extern \"types\"} %s".formatted(
           typesModuleName
         )
     );

codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java

@@ -881,7 +881,7 @@ private String dafnyTypeForOptionalMember(
 
     final String baseType = dafnyTypeForShape(memberShape.getTarget());
     final String prefix = concrete ? "" : "_I";
-    return "Wrappers_Compile.%sOption<%s>".formatted(prefix, baseType);
+    return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%sOption<%s>".formatted(prefix, baseType);
   }
 
   private String dafnyTypeForService(final ServiceShape serviceShape) {
@@ -1060,7 +1060,7 @@ private String dafnyTypeForResult(
     final boolean concrete
   ) {
     final String resultType = concrete ? "Result" : "_IResult";
-    return "Wrappers_Compile.%s<%s, %s>".formatted(
+    return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%s<%s, %s>".formatted(
         resultType,
         valueType,
         errorType