Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

smithy-dafny doesn't reject models with operations bound to multiple resource shapes #646

Open
robin-aws opened this issue Oct 18, 2024 · 1 comment
Open

smithy-dafny doesn't reject models with operations bound to multiple resource shapes #646

robin-aws opened this issue Oct 18, 2024 · 1 comment
Milestone
Support the DB ES...

Comments

@robin-aws
Copy link
Contributor

See https://github.com/smithy-lang/smithy-dafny/actions/runs/11409521976/job/31749989210.
@robin-aws robin-aws changed the title Rust doesn't handle operations on different resources with the same name Rust doesn't handle operations bound to multiple resource shapes Oct 18, 2024
@robin-aws
Copy link
Contributor Author

Actually, the test model that triggered this was invalid in the first place - operations cannot be bound multiple times: https://smithy.io/2.0/spec/service-types.html#service-closure

So the real bug is that Smithy validation allowed the model?

@robin-aws robin-aws changed the title Rust doesn't handle operations bound to multiple resource shapes smithy-dafny doesn't reject models with operations bound to multiple resource shapes Oct 18, 2024
robin-aws added a commit that referenced this issue Oct 18, 2024
@robin-aws
working around #646
2967451
seebees added a commit that referenced this issue Oct 18, 2024
@seebees
feat: Change MutableLocalStateTrait
a0540d2 
The original MutableLocalStateTrait
used pure dynamic frames.
But moving forward we are trying to move
to seperated classes.
These constructs would let a class
have internal state that is represented
by the reper/ValidState style invariant
but this mutation would not leak
into callers `modfies` clause.

At this time such a language feature does not exist.
So we aproximate it with an axiom.

working around #646
seebees added a commit that referenced this issue Oct 18, 2024
@seebees
feat: Change MutableLocalStateTrait
80f3e42 
The original MutableLocalStateTrait
used pure dynamic frames.
But moving forward we are trying to move
to seperated classes.
These constructs would let a class
have internal state that is represented
by the reper/ValidState style invariant
but this mutation would not leak
into callers `modfies` clause.

At this time such a language feature does not exist.
So we aproximate it with an axiom.

working around #646
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
Support the DB ESDK and MPL (GA)
Development

No branches or pull requests
1 participant
@robin-aws