First pass at the Lean soundness lemma #143
Conversation
| ∃ attrTys descendantTys, ets.find? uid.ty = some (attrTys, descendantTys) ∧ | ||
| InstanceOfType data.attrs (.record attrTys) ∧ | ||
| ∀ ancestor, ancestor ∈ data.ancestors → | ||
| ∃ descendants, ets.find? ancestor.ty = some descendants ∧ uid.ty ∈ descendantTys |
There was a problem hiding this comment.
This doesn't look right to me. EntityTypeStore maps an EntityType to the set of its ancestor types, rather than its descendent types. See here.
IIRC, the Dafny formalization had this flipped compared to how it's defined in the EntityStore, and in the Lean formalization, we decided to keep the direction consistent (always ancestors).
There was a problem hiding this comment.
Ah, I didn't look closely enough at the definition of EntityTypeStore.descendentOf. The formalization in Dafny matches the Rust code (the store tracks ancestors while the schema tracks descendants). Do we want to match the Rust code to simplify DRT, or switch to the more consistent formalization?
There was a problem hiding this comment.
My vote would be for the more consistent formalization :)
There was a problem hiding this comment.
Updated to the more consistent formalization. Please review commit 38081e7 when you get a chance
|
Thanks for the feedback @emina 😀 I addressed all of your comments, aside from the threads not marked as "resolved" above. |
|
Thank you for the great PR! :) |
| with the ancestor information in the action store. | ||
| -/ | ||
| def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop := | ||
| ∀ uid data, entities.find? uid = some data → |
There was a problem hiding this comment.
Does this need something to limit uid to those that are actions?
There was a problem hiding this comment.
Good catch. I think it needs to be something along the lines of
∀ uid data, entities.find? uid = some data → as.contains uid → ...
| CapabilitiesInvariant c request entities | ||
|
|
||
| -- Easy property: the empty capability set satisifies the invariant | ||
| theorem empty_CapabilitiesInvariant (request : Request) (entities : Entities) : |
There was a problem hiding this comment.
I personally don't like this mixed naming style
There was a problem hiding this comment.
Yeah it's a little ugly. Switched to a consistent style for lemma names in the most recent commit.
| with the ancestor information in the action store. | ||
| -/ | ||
| def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop := | ||
| ∀ uid data, entities.find? uid = some data → |
There was a problem hiding this comment.
Good catch. I think it needs to be something along the lines of
∀ uid data, entities.find? uid = some data → as.contains uid → ...
Issue #, if available:
Description of changes:
This PR adds a top-level definition for validation and sketches the soundness property. It does not include proofs -- these will come in future PRs.
Disclaimer:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.