Robin aws/smithy init example

TestModels/SQSExtended/Makefile

@@ -0,0 +1,37 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+
+TRANSPILE_TESTS_IN_RUST=1
+
+include ../SharedMakefile.mk
+
+SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
+
+PROJECT_SERVICES := \
+	SQSExtended
+
+MAIN_SERVICE_FOR_RUST := SQSExtended
+
+# Dependencies external to this project
+# Order is important
+# In java they MUST be built
+# in the order they depend on each other
+PROJECT_DEPENDENCIES := \
+	aws-sdks/sqs-via-cli
+
+PROJECT_INDEX := \
+	aws-sdks/sqs-via-cli/src/Index.dfy
+
+SERVICE_NAMESPACE_SQSExtended=polymorph.tutorial.sqsextended
+
+# Dependencies for each local service
+SERVICE_DEPS_SQSExtended := \
+	aws-sdks/sqs-via-cli
+
+clean: _clean
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
+	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+

TestModels/SQSExtended/build.gradle.kts

@@ -0,0 +1,22 @@
+plugins {
+    `java-library`
+    `maven-publish`
+    id("software.amazon.smithy.gradle.smithy-jar").version("1.1.0")
+}
+
+repositories {
+    mavenLocal()
+    mavenCentral()
+}
+
+smithy {
+
+}
+
+dependencies {
+    implementation("software.amazon.smithy:smithy-model:1.52.0")
+    implementation("software.amazon.smithy:smithy-aws-traits:1.52.0")
+    implementation("software.amazon.smithy:smithy-rules-engine:1.52.0")
+    implementation("software.amazon.smithy.dafny:sqs-model:1.0")
+}
+

TestModels/SQSExtended/model/sqsextended.smithy

@@ -0,0 +1,67 @@
+$version: "2"
+
+namespace polymorph.tutorial.sqsextended
+
+use com.amazonaws.sqs#Message
+
+@aws.polymorph#localService(
+  sdkId: "SQSExtended",
+  config: SQSExtendedClientConfig,
+  configRequired: true,
+  dependencies: [
+    com.amazonaws.sqs#AmazonSQS
+  ]
+)
+service AmazonSQSExtended {
+  version: "2021-11-01",
+  resources: [ MessageHandler ],
+  operations: [
+    HandleMessages,
+  ],
+  errors: [SQSExtendedError],
+}
+structure SQSExtendedClientConfig {
+  @required
+  sqsClient: SQSClientReference
+}
+@error("server")
+structure SQSExtendedError {
+  @required
+  message: String
+}
+
+@aws.polymorph#reference(service: com.amazonaws.sqs#AmazonSQS)
+structure SQSClientReference {}
+
+resource MessageHandler {
+  operations: [
+    HandleMessage,
+  ],
+}
+
+@aws.polymorph#reference(resource: MessageHandler)
+structure MessageHandlerReference {}
+
+operation HandleMessage {
+  input := {
+    @required
+    message: Message
+  }
+  errors: [RetryMessageError]
+}
+
+@error("client")
+structure RetryMessageError {
+  @required
+  message: String
+}
+
+operation HandleMessages {
+  input := {
+    @required
+    receiveRequest: com.amazonaws.sqs#ReceiveMessageRequest,
+
+    @required
+    handler: MessageHandlerReference
+  }
+}

TestModels/SQSExtended/runtimes/java/build.gradle.kts

@@ -0,0 +1,84 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+import java.io.File
+import java.io.FileInputStream
+import java.util.Properties
+import java.net.URI
+import javax.annotation.Nullable
+
+tasks.wrapper {
+    gradleVersion = "7.6"
+}
+
+plugins {
+    `java-library`
+    `maven-publish`
+}
+
+var props = Properties().apply {
+    load(FileInputStream(File(rootProject.rootDir, "../../project.properties")))
+}
+var dafnyVersion = props.getProperty("dafnyVersion")
+
+group = "polymorph.tutorial.sqsextended"
+version = "1.0-SNAPSHOT"
+description = "AmazonSQSExtended"
+
+java {
+    toolchain.languageVersion.set(JavaLanguageVersion.of(8))
+    sourceSets["main"].java {
+        srcDir("src/main/java")
+        srcDir("src/main/dafny-generated")
+        srcDir("src/main/smithy-generated")
+    }
+    sourceSets["test"].java {
+        srcDir("src/test/java")
+        srcDir("src/test/dafny-generated")
+        srcDir("src/test/smithy-generated")
+    }
+}
+
+repositories {
+    mavenCentral()
+    mavenLocal()
+}
+
+dependencies {
+    implementation("org.dafny:DafnyRuntime:${dafnyVersion}")
+    implementation("software.amazon.smithy.dafny:conversion:0.1.1")
+    implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
+    // TODO: name needs fixing
+    implementation("com.amazonaws.sqs:AmazonSQS:1.0-SNAPSHOT")
+    implementation(platform("software.amazon.awssdk:bom:2.19.1"))
+    implementation("software.amazon.awssdk:sqs")
+    testImplementation("org.testng:testng:7.5")
+}
+
+publishing {
+    publications.create<MavenPublication>("mavenLocal") {
+        groupId = group as String?
+        artifactId = description
+        from(components["java"])
+    }
+    publications.create<MavenPublication>("maven") {
+        groupId = group as String?
+        artifactId = description
+        from(components["java"])
+    }
+    repositories { mavenLocal() }
+}
+
+tasks.withType<JavaCompile>() {
+    options.encoding = "UTF-8"
+}
+
+tasks {
+    register("runTests", JavaExec::class.java) {
+        mainClass.set("TestsFromDafny")
+        classpath = sourceSets["test"].runtimeClasspath
+    }
+}
+
+tasks.named<Test>("test") {
+    useTestNG()
+}

TestModels/SQSExtended/runtimes/java/src/main/java/Dafny/polymorph/tutorial/sqsextended/__default.java

@@ -0,0 +1,5 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+package polymorph.tutorial.sqsextended.internaldafny;
+
+public class __default extends _ExternBase___default {}

TestModels/SQSExtended/runtimes/rust/Cargo.toml

@@ -0,0 +1,28 @@
+[package]
+name = "extended_sqs"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+wrapped-client = []
+
+[dependencies]
+aws-sdk-sqs = "1.45.0"
+aws-config = "1.5.4"
+aws-smithy-runtime = {version = "1.6.0", features = ["client"] }
+aws-smithy-runtime-api = {version = "1.7.0", features = ["client"] }
+aws-smithy-types = "1.2.0"
+# TODO: Wrong path according to the tutorial instructions
+dafny_runtime = { path = "../../../../../TestModels/dafny-dependencies/dafny_runtime_rust"}
+
+[dev-dependencies]
+extended_sqs = { path = ".", features = ["wrapped-client"] }
+
+[dependencies.tokio]
+version = "1.26.0"
+features = ["full"]
+
+[lib]
+path = "src/implementation_from_dafny.rs"

TestModels/SQSExtended/smithy-build.json

@@ -0,0 +1,13 @@
+{
+  "version": "1.0",
+  "sources": ["model"],
+  "maven": {
+      "dependencies": [
+        "software.amazon.smithy.dafny:smithy-dafny-codegen:0.1.0",
+        "software.amazon.smithy.dafny:sqs-model:1.0"
+      ],
+      "repositories": [
+        { "url": "file:///Users/salkeldr/.m2/repository/" }
+      ]
+  }
+}

TestModels/SQSExtended/src/Index.dfy

@@ -0,0 +1,33 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+include "SQSExtendedImpl.dfy"
+
+module {:extern "polymorph.tutorial.sqsextended.internaldafny" } SQSExtended refines AbstractPolymorphTutorialSqsextendedService {
+  import Operations = AmazonSQSExtendedImpl
+
+  method SQSExtended(config: SQSExtendedClientConfig)
+    returns (res: Result<SQSExtendedClient, Error>)
+    ensures res.Success? ==> 
+      && res.value.ValidState()
+      && fresh(res.value.History)
+  {
+    var client := new SQSExtendedClient(Operations.Config(
+                                        sqsClient := config.sqsClient
+                                        ));
+    return Success(client);
+  }
+
+  class SQSExtendedClient... {
+    predicate ValidState() {
+      && Operations.ValidInternalConfig?(config)
+      && History !in Operations.ModifiesInternalConfig(config)
+      && Modifies == Operations.ModifiesInternalConfig(config) + {History}
+    }
+
+    constructor(config: Operations.InternalConfig) {
+      this.config := config;
+      History := new IAmazonSQSExtendedClientCallHistory();
+      Modifies := Operations.ModifiesInternalConfig(config) + {History};
+    }
+  }
+}

TestModels/SQSExtended/src/SQSExtendedImpl.dfy

@@ -0,0 +1,59 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
+include "../Model/PolymorphTutorialSqsextendedTypes.dfy"
+module AmazonSQSExtendedImpl refines AbstractPolymorphTutorialSqsextendedOperations {
+  datatype Config = Config(
+    nameonly sqsClient : ComAmazonawsSqsTypes.ISQSClient
+  )
+  type InternalConfig = Config
+  predicate ValidInternalConfig?(config: InternalConfig)
+  {
+    config.sqsClient.ValidState()
+  }
+  function ModifiesInternalConfig(config: InternalConfig): set<object>
+  {
+    config.sqsClient.Modifies
+  }
+  predicate HandleMessagesEnsuresPublicly(input: HandleMessagesInput , output: Result<(), Error>)
+  {true}
+
+
+
+  method HandleMessages ( config: InternalConfig , input: HandleMessagesInput )
+    returns (output: Result<(), Error>)
+
+  {
+    var queueUrl := input.receiveRequest.QueueUrl;
+
+    var maybeMessagesResult := config.sqsClient.ReceiveMessage(input.receiveRequest);
+    var messagesResult :- maybeMessagesResult.MapFailure(e => ComAmazonawsSqs(e));
+    // TODO: Handle error better
+    expect messagesResult.Messages.Some?;
+    var messages :- expect messagesResult.Messages;
+
+    for i := 0 to |messages| {
+      var message := messages[i];
+      // TODO: Handle error better
+      var receiptHandle :- expect message.ReceiptHandle;
+
+      var messageResult := input.handler.HandleMessage(HandleMessageInput(message := message));
+
+      if messageResult.Success? {
+        var deleteResult := config.sqsClient.DeleteMessage(ComAmazonawsSqsTypes.DeleteMessageRequest(
+                                                             QueueUrl := queueUrl,
+                                                             ReceiptHandle := receiptHandle
+                                                           ));
+      } else {
+        // TODO: Handle retryable errors
+        var deleteResult := config.sqsClient.ChangeMessageVisibility(ComAmazonawsSqsTypes.ChangeMessageVisibilityRequest(
+                                                                       QueueUrl := queueUrl,
+                                                                       ReceiptHandle := receiptHandle,
+                                                                       VisibilityTimeout := 0
+                                                                     ));
+      }
+    }
+
+    output := Success(());
+  }
+}