Conversation
john-h-kastner-aws
changed the title
khieta
left a comment
khieta
left a comment
There was a problem hiding this comment.
Overall looks good. I left a few small comments.
khieta
left a comment
khieta
left a comment
There was a problem hiding this comment.
A couple more quick comments.
| function lubEntity(lub1: EntityLUB, lub2: EntityLUB): EntityLUB { | ||
| lub1.union(lub2) | ||
| function lubEntity(lub1: EntityLUB, lub2: EntityLUB, m: ValidationMode): Result<EntityLUB> { | ||
| if m.isStrict() && lub1 != lub2 |
There was a problem hiding this comment.
In strict mode, do you also want to check that neither are AnyEntity?
There was a problem hiding this comment.
For strict mode this already gives E </: AnyEntity for E where E != AnyEntity. I could change it so that AnyEntity </: AnyEntity, but then subtyping isn't reflexive (which is strange). I don't think it really matters one way or the other since AnyEntity shouldn't be constructed by the strict typechecker as along as it doesn't show up in the request environment anywhere.
john-h-kastner-aws
force-pushed
the
feature/jkastner/simpl_strict_validation
branch
from
61f4208 to
fd1a16c
Compare
|
|
||
| // The ValidationMode determines whether to use permissive or strict typechecking | ||
| datatype ValidationMode = Permissive | Strict { | ||
| predicate isStrict() { |
There was a problem hiding this comment.
I wonder if it makes sense to use the Strict? method Dafny automatically generates instead.
There was a problem hiding this comment.
I think you're right
| attrsTag.OpenAttributes? | ||
| } | ||
|
|
||
| predicate isStrictType() { |
| Entity(lub: EntityLUB) | | ||
| Extension(Name) | ||
| { | ||
| predicate isStrictType() { |
| { | ||
| assert subty(getType(ei2s[i],effs), eltType); | ||
| SubtyTrans(getType(ei2s[i],effs), eltType, Type.Entity(AnyEntity)); | ||
| assert subty(getType(ei2s[i],effs), eltType,ValidationMode.Permissive); |
There was a problem hiding this comment.
[nit] noticed we aren't consistent about spaces after commas. Unfortunately, it doesn't seem like formatting in vscode handles this.
There was a problem hiding this comment.
dafny format doesn't either unfortunately.
4 participants
Issue #, if available:
cedar-policy/rfcs#19
cedar-policy/cedar#282
Description of changes:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.