Skip to content

Commit

Permalink
feat: Change MutableLocalStateTrait
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@seebees
seebees committed Oct 9, 2024
1 parent f01e40b commit 477ec52
Show file tree
Hide file tree
Showing 2 changed files with 109 additions and 41 deletions.
142 changes: 101 additions & 41 deletions ...hy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -511,6 +511,7 @@ public TokenTree generateServiceTraitDefinition(ServiceShape serviceShape) {
generateEnsuresPubliclyPredicate(serviceShape, operation),
generateBodilessOperationMethodThatEnsuresCallEvents(
serviceShape,
Optional.empty(),
operation,
ImplementationType.CODEGEN
),
Expand Down Expand Up @@ -585,7 +586,7 @@ public TokenTree generateReferenceTraitDefinition(
.stream()
.flatMap(operation ->
Stream.of(
generateResourceOperationMethod(serviceShape, operation),
generateResourceOperationMethod(serviceShape, Optional.of(resource), operation),
TokenTree.empty()
)
)
Expand Down Expand Up @@ -755,20 +756,14 @@ private TokenTree generateMutableInvariantInterface(ShapeId shapeId) {
nameResolver.mutableStateFunctionName(),
nameResolver.callHistoryFieldName()
),
mutableState
? """
// Given that you are mutating state,
// your %s function is going to get complicated.
""".formatted(nameResolver.validStateInvariantName())
: """
"""
// If you do not need to mutate anything:
// %s := {%s};
""".formatted(
""".formatted(
nameResolver.mutableStateFunctionName(),
nameResolver.callHistoryFieldName()
),
"ghost %s %s: set<object>".formatted(
mutableState ? "var" : "const",
"ghost const %s: set<object>".formatted(
nameResolver.mutableStateFunctionName()
),
"// For an unassigned field defined in a trait,",
Expand All @@ -789,26 +784,7 @@ private TokenTree generateMutableInvariantInterface(ShapeId shapeId) {
"// You MUST also ensure %s in your constructor.".formatted(
nameResolver.validStateInvariantName()
),
mutableState
? """
// Not only will you need to ensure
// that all your mutable elements are contained in %s,
// you MUST also ensure
// that your invariant does not rely on %s.
// This means your invariant will begin to look like:
// && %1$s in %2$s
// && this in %2$s // so we can read property
// && property in %2$s // so we can read properties of property
// && property != %1$s as object // property really is not %1$s!
// && (forall m <- property.Modifies // everything in property.Modifies
// :: m in %2$s - %1$s) // is in %2$s and really is not %1$s!
""".formatted(
nameResolver.callHistoryFieldName(),
nameResolver.mutableStateFunctionName()
)
: "",
"predicate %s()".formatted(nameResolver.validStateInvariantName()),
mutableState ? readsClause : "",
"ensures %s() ==> %s in %s".formatted(
nameResolver.validStateInvariantName(),
nameResolver.callHistoryFieldName(),
Expand All @@ -817,12 +793,45 @@ private TokenTree generateMutableInvariantInterface(ShapeId shapeId) {
)
.dropEmpty()
.lineSeparated()
.append(TokenTree.empty())
.append(mutableState
? TokenTree.of(
TokenTree.of("""
// Need to update all these words
//
// Not only will you need to ensure
// that all your mutable elements are contained in %s,
// you MUST also ensure
// that your invariant does not rely on %s.
// This means your invariant will begin to look like:
// && %1$s in %2$s
// && this in %2$s // so we can read property
// && property in %2$s // so we can read properties of property
// && property != %1$s as object // property really is not %1$s!
// && (forall m <- property.Modifies // everything in property.Modifies
// :: m in %2$s - %1$s) // is in %2$s and really is not %1$s!
""".formatted(
nameResolver.callHistoryFieldName(),
nameResolver.mutableStateFunctionName()
)
),
TokenTree.of("""
ghost var InternalModifies: set<object>
predicate InternalValidState()
reads this`InternalModifies, InternalModifies
ensures InternalValidState() ==> History !in InternalModifies
""")
)
: TokenTree.empty()
)
.lineSeparated();
}

private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents(
final ServiceShape serviceShape,
final Optional<ResourceShape> resource,
final ShapeId operationShapeId,
final ImplementationType implementationType
) {
Expand Down Expand Up @@ -868,12 +877,13 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents(
.of(
generateMutableInvariantForMethod(
serviceShape,
resource,
operationShapeId,
implementationType
),
generateEnsuresForEnsuresPubliclyPredicate(operationShapeId),
!implementationType.equals(ImplementationType.ABSTRACT)
? generateEnsuresHistoricalCallEvents(operationShapeId)
? generateEnsuresHistoricalCallEvents(serviceShape, resource, operationShapeId)
: TokenTree.empty()
)
.dropEmpty()
Expand Down Expand Up @@ -904,18 +914,22 @@ private TokenTree generateBodilessOperationMethodThatEnsuresCallEvents(

private TokenTree generateResourceOperationMethod(
final ServiceShape serviceShape,
final Optional<ResourceShape> resource,
final ShapeId operationShapeId
) {
final OperationShape operationShape = model.expectShape(
operationShapeId,
OperationShape.class
);

final boolean mutableState = resource.isPresent() && resource.get().hasTrait(MutableLocalStateTrait.class);

return TokenTree
.of(
generateEnsuresPubliclyPredicate(serviceShape, operationShapeId),
generateBodilessOperationMethodThatEnsuresCallEvents(
serviceShape,
resource,
operationShapeId,
ImplementationType.CODEGEN
),
Expand All @@ -924,6 +938,19 @@ private TokenTree generateResourceOperationMethod(
// and return the result
TokenTree
.of(
mutableState
? TokenTree.of(
"""
// There needs to be a bit of comments here
""",
"assume {:axiom} %s < %s && %s();"
.formatted(
nameResolver.dynamicMutableStateFunctionName(),
nameResolver.mutableStateFunctionName(),
nameResolver.dynamicValidStateInvariantName()
)
)
: TokenTree.empty(),
TokenTree
.of("output :=")
.append(
Expand All @@ -936,6 +963,7 @@ private TokenTree generateResourceOperationMethod(
.append(TokenTree.of("(input);")),
generateAccumulateHistoricalCallEvents(operationShapeId)
)
.dropEmpty()
.lineSeparated()
.braced(),
// This is method for the library developer to implement
Expand All @@ -959,6 +987,7 @@ private TokenTree generateResourceOperationMethod(
generateOperationReturnsClause(serviceShape, operationShape),
generateMutableInvariantForMethod(
serviceShape,
resource,
operationShapeId,
ImplementationType.DEVELOPER
),
Expand Down Expand Up @@ -1012,6 +1041,7 @@ public enum ImplementationType {

private TokenTree generateMutableInvariantForMethod(
final ServiceShape serviceShape,
final Optional<ResourceShape> resource,
final ShapeId operationShapeId,
final ImplementationType implementationType
) {
Expand All @@ -1023,14 +1053,17 @@ private TokenTree generateMutableInvariantForMethod(
: "";

final TokenTree requires = OperationMemberRequires(
resource,
operationShapeId,
implementationType
);
final TokenTree ensures = OperationMemberEnsures(
resource,
operationShapeId,
implementationType
);
final TokenTree modifiesSet = OperationModifiesInputs(
resource,
operationShapeId,
implementationType
);
Expand Down Expand Up @@ -1061,16 +1094,20 @@ private TokenTree generateMutableInvariantForMethod(
}

private TokenTree OperationMemberRequires(
final Optional<ResourceShape> resource,
final ShapeId operationShapeId,
final ImplementationType implementationType
) {

final String validStateInvariantName =
nameResolver.validStateInvariantName();
final OperationShape operationShape = model.expectShape(
operationShapeId,
OperationShape.class
);

final boolean mutableState = resource.isPresent() && resource.get().hasTrait(MutableLocalStateTrait.class);

final TokenTree inputReferencesThatNeedValidState = operationShape
.getInput()
.map(shapeId ->
Expand All @@ -1096,19 +1133,28 @@ private TokenTree OperationMemberRequires(
.orElse(TokenTree.empty());
return Token
.of(
!implementationType.equals(ImplementationType.ABSTRACT)
? "\n && %s()".formatted(validStateInvariantName)
: "\n && %s(config)".formatted(nameResolver.validConfigPredicate())
implementationType.equals(ImplementationType.ABSTRACT)
? "\n && %s(config)".formatted(nameResolver.validConfigPredicate())
: implementationType.equals(ImplementationType.DEVELOPER) && mutableState
? "\n && %s()".formatted(nameResolver.dynamicValidStateInvariantName())
// The expectation here is
// || implementationType.equals(ImplementationType.CODEGEN)
// || (implementationType.equals(ImplementationType.DEVELOPER) && !mutableState)
: "\n && %s()".formatted(validStateInvariantName)
)
.append(inputReferencesThatNeedValidState)
.dropEmpty()
.prependToNonEmpty(Token.of("requires"));
}

private TokenTree OperationMemberEnsures(
final Optional<ResourceShape> resource,
final ShapeId operationShapeId,
final ImplementationType implementationType
) {

final boolean mutableState = resource.isPresent() && resource.get().hasTrait(MutableLocalStateTrait.class);

final OperationShape operationShape = model.expectShape(
operationShapeId,
OperationShape.class
Expand Down Expand Up @@ -1147,9 +1193,14 @@ private TokenTree OperationMemberEnsures(
return TokenTree
.of(
Token.of(
!implementationType.equals(ImplementationType.ABSTRACT)
? "&& %s()".formatted(validStateInvariantName)
: "&& %s(config)".formatted(nameResolver.validConfigPredicate())
implementationType.equals(ImplementationType.ABSTRACT)
? "&& %s(config)".formatted(nameResolver.validConfigPredicate())
: implementationType.equals(ImplementationType.DEVELOPER) && mutableState
? "&& %s()".formatted(nameResolver.dynamicValidStateInvariantName())
// The expectation here is
// || implementationType.equals(ImplementationType.CODEGEN)
// || (implementationType.equals(ImplementationType.DEVELOPER) && !mutableState)
: "&& %s()".formatted(validStateInvariantName)
),
outputReferencesThatNeedValidState
)
Expand Down Expand Up @@ -1230,7 +1281,7 @@ private TokenTree OperationMemberValidState(
// so if they are added to our output
// then we can not prove freshness of these items
final TokenTree removeInputs = direction == InputOutput.OUTPUT
? OperationModifiesInputs(operationShape.getId(), implementationType)
? OperationModifiesInputs(Optional.empty(), operationShape.getId(), implementationType)
.prependSeperated(Token.of("\n -"))
: TokenTree.empty();

Expand Down Expand Up @@ -1423,9 +1474,13 @@ private TokenTree OperationMemberValidState_UnionHelper(


private TokenTree OperationModifiesInputs(
final Optional<ResourceShape> resource,
final ShapeId operationShapeId,
final ImplementationType implementationType
) {

final boolean mutableState = resource.isPresent() && resource.get().hasTrait(MutableLocalStateTrait.class);

final OperationShape operationShape = model.expectShape(
operationShapeId,
OperationShape.class
Expand All @@ -1447,9 +1502,9 @@ private TokenTree OperationModifiesInputs(
// This lets us keep track of any additional modifications
implementationType == ImplementationType.ABSTRACT
// The abstract operations do not have a class with a `Modifies` property
? Token.of(
"%s(config)".formatted(nameResolver.modifiesInternalConfig())
)
? Token.of("%s(config)".formatted(nameResolver.modifiesInternalConfig()))
: implementationType.equals(ImplementationType.DEVELOPER) && mutableState
? Token.of("%s".format(nameResolver.dynamicMutableStateFunctionName()))
// The class has a `Modifies` property
// The `- {History} is important for consumers
// otherwise if they use multiple APIs
Expand Down Expand Up @@ -1685,6 +1740,8 @@ private TokenTree OperationMemberModifies_UnionHelper(
}

private TokenTree generateEnsuresHistoricalCallEvents(
final ServiceShape serviceShape,
final Optional<ResourceShape> resource,
final ShapeId operationShapeId
) {
final OperationShape operationShape = model.expectShape(
Expand Down Expand Up @@ -2017,6 +2074,7 @@ public TokenTree generateAbstractServiceModule(ServiceShape serviceShape) {
.lineSeparated(),
generateBodilessOperationMethodThatEnsuresCallEvents(
serviceShape,
Optional.empty(),
operation,
ImplementationType.CODEGEN
),
Expand Down Expand Up @@ -3019,6 +3077,7 @@ private TokenTree generateAbstractOperationsModule(
generateEnsuresPubliclyPredicate(serviceShape, operation),
generateBodilessOperationMethodThatEnsuresCallEvents(
serviceShape,
Optional.empty(),
operation,
ImplementationType.ABSTRACT
)
Expand Down Expand Up @@ -3102,6 +3161,7 @@ private TokenTree generateTemplateOperationsModule(
TokenTree.of("{true}"),
generateBodilessOperationMethodThatEnsuresCallEvents(
serviceShape,
Optional.empty(),
operation,
ImplementationType.DEVELOPER
),
Expand Down
8 changes: 8 additions & 0 deletions ...-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyNameResolver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -336,10 +336,18 @@ public String mutableStateFunctionName() {
return "Modifies";
}

public String dynamicMutableStateFunctionName() {
return "InternalModifies";
}

public String validStateInvariantName() {
return "ValidState";
}

public String dynamicValidStateInvariantName() {
return "InternalValidState";
}

public String callHistoryFieldName() {
return "History";
}
Expand Down

0 comments on commit 477ec52

Please sign in to comment.