Validation soundness - Complete#383
Conversation
khieta
left a comment
khieta
left a comment
There was a problem hiding this comment.
Good start Bhakti! Thanks for the PR 🙂
It occurred to me that the partial evaluation proofs also have to reason about a substitution function (see Partial.Value.subst), so maybe you can look there for inspiration about how to verify substituteAction. Would also be great to unify these definitions, if at all possible.
| # We expect a copy of `cedar-policy/cedar` present in this directory, but do | ||
| # not track it in version control. | ||
| cedar/ | ||
| /cedar-policy/cedar |
There was a problem hiding this comment.
Probably don't want to change this since CI expects the cedar/ path
There was a problem hiding this comment.
Ah, so this line messes up stuff on macos because of case sensitivity; i can restore it but it just means the entire cedar-lean/cedar directory is ignored when i commit. i can just manually change it back and forth for now but it could be worth resolving
emina
left a comment
emina
left a comment
There was a problem hiding this comment.
Thanks for the PR; very nice progress! :)
Some small comments included.
|
|
||
| -- forM and mapM | ||
|
|
||
| theorem forM_mapM {α β : Type} (f : α → Except β PUnit) (xs : List α) (ys : List PUnit) : |
There was a problem hiding this comment.
Formatting nit: see here for a guide on indentation and formatting.
We would usually format this theorem statement so that the name of the theorem and arguments are on one line, the hypotheses and conclusion are indented and on separate lines, := by is on its own line and not indented, and the proof body is indented. For example:
theorem forM_mapM {α β : Type} (f : α → Except β PUnit) (xs : List α) (ys : List PUnit) :
xs.mapM f = Except.ok ys → xs.forM f = Except.ok ()
:= by
intro h₀
rw [List.mapM_ok_iff_forall₂] at h₀
sorry
complete proof of the soundness of the cedar validator
|
This PR is now complete with the proof of soundness of the Cedar validator. |
emina
left a comment
emina
left a comment
There was a problem hiding this comment.
Really nice PR, thank you!
Left some minor comments on formatting but approving the PR otherwise.
…edar-spec into bhaktish/validator-soundness
khieta
left a comment
khieta
left a comment
There was a problem hiding this comment.
Thanks for all the hard work 🙂 Left a couple minor comments on naming
| theorem evaluates_subst_ite {i t e : Expr} {request : Request} {entities : Entities} | ||
| (ih₁ : EvaluatesSubst i request entities) | ||
| (ih₂ : EvaluatesSubst t request entities) | ||
| (ih₃ : EvaluatesSubst e request entities) : | ||
| evaluate (substituteAction request.action (Expr.ite i t e)) request entities = | ||
| evaluate (Expr.ite i t e) request entities |
There was a problem hiding this comment.
I think it would be a little cleaner to move these proofs about substituteAction to their own file (e.g., Thm/Validation/SubstituteAction.lean)
There was a problem hiding this comment.
@emina said keeping things in one file < 1000 lines was ideal for like easy access -- any thoughts here? I would probably opt for a different file too.
There was a problem hiding this comment.
Ah, I should have clarify: we normally keep the main theorem in a separate (small) file, and all the auxiliary ones in separate (usually) big files. An example of the main theorem: https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/Thm/Typechecking.lean
There was a problem hiding this comment.
I don't feel strongly, so fine either way
There was a problem hiding this comment.
I think I'd personally prefer if files were capped at something more like 500 lines, not 1000 lines -- for larger files, there's probably a sensible way to split it up. But our current codebase definitely has a bunch of large files. Not merge blocking for sure
There was a problem hiding this comment.
I separated it out
| def SubstituteActionPreservesEvaluation (expr : Expr) (request : Request) (entities : Entities) : Prop := | ||
| evaluate (substituteAction request.action expr) request entities = evaluate expr request entities |
There was a problem hiding this comment.
Just noticed that you're only using this predicate in hypotheses below. Is there a reason you don't use it in the main lemma statement?
There was a problem hiding this comment.
Just following the structure of the typechecker proofs -- no real reason to do it this way, I guess.
cdisselkoen
left a comment
cdisselkoen
left a comment
There was a problem hiding this comment.
Looks good. Minor naming suggestion for the generic (List) lemma, for consistency with other mapM lemmas
5 participants
Description of changes:
This PR contains the proof of soundness of the Cedar validator.