Shape Closure in Smithy Dafny

[texastony]

Issue

Which of the shapes in a Smithy Model path
(--model arguements to the CLI)
are represented by the output of Smithy Dafny
is surprisingly ambiguous.

Is it all the Shapes?
Clearly not, since a subject may depend on another (local) service,
and the dependencies shapes should not be represented in the output,
at least not entirely.

(By not entirely, I mean that they do not need a data structure definition,
but they may need import or conversion logic represented in the output.)

Is it all the Shapes in the namespace?

That seems to be the implied behavior,
but what about nested namespaces?

We have a real world example in the MPL's Key Store.

Is it just all the Shapes in the Service's closure, as the Smithy Spec suggests?

Clearly not,
as we need the "orphaned" shapes.

So what is it?

And how we can write tests that ensure all the output languages,
Dafny included,
behave the same with respect to shape closure.

Related Issues:

• OrphanedShapes TestModel #622
• Align need for orphaned shape generation better with Smithy code generation recommendations/idioms #627

[texastony]

Tooling to audit

Is there a Smithy CLI tool that can audit
a Model path for shapes outside of the service closure?

If so,
could we run that tool to see all the shapes
that, by Smithy's default behavior,
are ignored?

That... that might be a cheap "something".

Line Coverage

We could add test line coverage behavior to the execution of the "wrapped local service test" target.

Particularly if we can tell the line coverage mechanism to
only measure the "glue" of the MPL,
that would give us some indication of what we might be missing,
AND could be used to improve on the test coverage of the MPL.

[robin-aws]

I agree it makes sense to have this issue separate from #627 at least - that one is about changing smithy-dafny configuration to align better with the Smithy spec and other code generators, but this one can be about clarifying the current behavior and mechanisms related to that.

IMO the current behavior is to generate for all shapes in a given namespace (i.e. the --namespace polymorph CLI option). That might not be true across all languages, but I'd call it a bug if not.

Nested namespaces is a fair question, but FWIW I made --namespace specifiable multiple times as part of #591, so that might be an easy solution.