chore: More readme fixes (#270)

Just the README updates from #185:

* Calling out runtime libraries limitations in the top level README
* Moving codegen/README.md to codegen/smithy-dafny-codegen/README.md
* Updating a few inaccuracies in the codegen README

README.md

@@ -22,7 +22,12 @@ A generated Dafny client for AWS SQS targeting compilation to Java, for example,
 will contain Dafny source code, Java source code,
 and a dependency on a Java artifact such as `software.amazon.awssdk:sqs`.
 
-This support is provided as a `dafny-client-codegen` Smithy build plugin with a similar API to the other [Smithy code generators](https://smithy.io/2.0/implementations.html#client-code-generators), configured by entries in a `smithy-build.json` file. See the [`codegen/smithy-dafny-codegen`](codegen/smithy-dafny-codegen) directory for further details and examples.
+This support is provided as a `dafny-client-codegen` Smithy build plugin
+with a similar API to the other 
+[Smithy code generators](https://smithy.io/2.0/implementations.html#client-code-generators),
+configured by entries in a `smithy-build.json` file. 
+See the [`codegen/smithy-dafny-codegen`](codegen/smithy-dafny-codegen) directory for
+further details and examples.
 
 ## Generating multi-language libraries (a.k.a. "polymorphing")
 
@@ -53,6 +58,8 @@ See the [`codegen/smithy-dafny-codegen-cli`](codegen/smithy-dafny-codegen-cli) d
 
 ## Limitations
 
+### Completeness
+
 The code generators in this repository do not yet support all shapes and traits in the core Smithy specification
 or the related AWS traits specifications.
 Even for those that are supported, the implementation does not necessarily follow all of the recommendations
@@ -67,6 +74,18 @@ and safely assuming response structures are valid,
 with respect to a particular snapshot of that service's API constraints.
 However, it also means that future service changes that should be backwards-compatible may cause your Dafny code to break.
 
+### Runtime libraries
+
+Like other Smithy-based code generators, these tools will emit references to 
+[common runtime library code](https://smithy.io/2.0/guides/building-codegen/overview-and-concepts.html#runtime-libraries).
+However, at the time of writing this the Dafny ecosystem does not yet have mature package management features
+to support distributing and maintaining such libraries.
+An example of the required runtime functionality is located in
+`TestModels/dafny-dependencies/StandardLibrary`,
+but is not intended to be distributed as a shared library.
+We recommend making a copy of this code in your own projects
+as the copy maintained here may change in the future.
+
 ## Security
 
 See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.

codegen/README.md → codegen/smithy-dafny-codegen/README.md

@@ -70,14 +70,11 @@ are as follows:
    Note the exact version of the `software.amazon.smithy` dependencies MAY NOT need to be 
    `1.28.1` exactly, but MUST be consistent.
 
-3. Clone the GitHub repository for [smithy-dafny](https://github.com/awslabs/smithy-dafny)
-   somewhere nearby, being sure to initialize submodules.
-   If this repository is still private, reach out to aws-arg-[email protected]
-   for access.
+3. Make a copy of the `TestModels/dafny-dependencies/StandardLibrary` directory
+   for the generated code to refer to.
 
-   This is necessary because it contains reusable Dafny code that
-   the generated client will depend on, but is not yet independently distributed for
-   shared use.
+   This is necessary because the runtime library code the generated code will depend on
+   is not yet available as a shared Dafny library.
 
 4. Create a `smithy-build.json` file with the following contents,
    substituting "smithy.example#ExampleService" with the name of the service
@@ -92,7 +89,7 @@ are as follows:
                 "edition": "2023",
                 "service": "smithy.example#ExampleService",
                 "targetLanguages": ["dotnet"],
-                "includeDafnyPath": "[relative]/[path]/[to]/smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy"
+                "includeDafnyPath": "[relative]/[path]/[to]/StandardLibrary/src/Index.dfy"
             }
         }
     }
@@ -111,30 +108,25 @@ are as follows:
 7. Run `gradle build` (alternatively, you can use a
    [Gradle wrapper](https://docs.gradle.org/current/userguide/gradle_wrapper.html)).
 
-8. The generated client can be found in `build/smithyprojections/foo-client/source/dafny-client-codegen`.
+8. The generated client can be found under the `build/smithyprojections`,
+   the exact path depending on the name of the service.
+   For example, `build/smithyprojections/example-client/source/dafny-client-codegen`.
 
 See [the Smithy documentation](https://smithy.io/2.0/guides/building-models/gradle-plugin.html)
 for more information on building Smithy projects with Gradle.
 
-Note there are some caveats related to building the generated client code:
-
-1. If you specified Java as a target language,
-   the result will depend on the [dafny-java-conversion](https://github.com/awslabs/smithy-dafny/tree/main-1.x/dafny-java-conversion)
-   library, which is also not yet published.
-   The easiest workaround is to first run the `publishToLocalMaven` gradle task on a copy of the source for that library.
-
 ## Using projections
 
 This plugin does not yet handle all Smithy features, especially since
 at the time of writing this, Dafny itself does not have a strongly
-idiomatic representation for concepts such as Timestamps.
+idiomatic representation for some concepts.
 Fortunately, the Smithy Gradle plugin provides several
 ["transforms"](https://smithy.io/2.0/guides/building-models/build-config.html#transforms)
 that can be used to filter a service model
 to remove unsupported shapes.
 
 The following example removes all operations that transitively refer
-to some of the shape types that this plugin does not yet support:
+to one of the shape types that this plugin does not yet support:
 
 ```json
 {
@@ -145,7 +137,7 @@ to some of the shape types that this plugin does not yet support:
                 {
                     "name": "excludeShapesBySelector",
                     "args": {
-                        "selector": "operation :test(~> timestamp, double, float, resource)"
+                        "selector": "operation :test(~> document)"
                     }
                 }
             ],