Repair batched evaluation proof (#833)

Signed-off-by: John Kastner <jkastner@amazon.com>

Author: john-h-kastner-aws

cedar-lean/Cedar/Thm.lean

@@ -22,4 +22,5 @@ import Cedar.Thm.Typechecking
 import Cedar.Thm.Validation
 import Cedar.Thm.WellTyped
 import Cedar.Thm.TPE
+import Cedar.Thm.BatchedEvaluator
 import Cedar.Thm.WellTypedVerification

cedar-lean/Cedar/Thm/Authorization.lean

@@ -16,6 +16,8 @@
 
 import Cedar.Spec
 import Cedar.Thm.Authorization.Authorizer
+import Cedar.Thm.Authorization.PolicySlice
+import Cedar.Thm.Authorization.Evaluator
 
 /-! This file contains basic theorems about Cedar's authorizer. -/
 

…lean/Cedar/Thm/TPE/BatchedEvaluator.lean …dar-lean/Cedar/Thm/BatchedEvaluator.leancedar-lean/Cedar/Thm/TPE/BatchedEvaluator.lean renamed to cedar-lean/Cedar/Thm/BatchedEvaluator.lean cedar-lean/Cedar/Thm/TPE/BatchedEvaluator.lean renamed to cedar-lean/Cedar/Thm/BatchedEvaluator.lean

@@ -29,7 +29,7 @@ in the code base at the moment.
 -/
 abbrev EntityLoader.WellBehaved (store: Entities) (loader: EntityLoader) : Prop :=
   ∀ s, s ⊆ (loader s).keys ∧
-       EntitiesRefine store ((loader s).mapOnValues EntityDataOption.asPartial)
+       EntitiesRefine store ((loader s).mapOnValues MaybeEntityData.asPartial)
 
 theorem as_partial_request_refines {req : Request} :
   RequestRefines req req.asPartialRequest := by
@@ -51,12 +51,12 @@ theorem any_refines_empty_entities :
   intro a e₂ h₁
   contradiction
 
--- Helper lemma for map append refinementSlicedEntities
+-- Helper lemma for map append refinement
 theorem entities_refine_append (es : Entities) (m1 m2 : PartialEntities) :
   EntitiesRefine es m1 → EntitiesRefine es m2 → EntitiesRefine es (m2 ++ m1) := by
   intro h1 h2
   unfold EntitiesRefine
-  intro a e₂ h_findSlicedEntities
+  intro a e₂ h_find
   rw [Map.find?_append] at h_find
   cases h_case : m2.find? a with
   | some e₂' =>
@@ -67,21 +67,21 @@ theorem entities_refine_append (es : Entities) (m1 m2 : PartialEntities) :
     rw [h_eq]
     exact h2 a e₂' h_case
   | none =>
-    have h_find1 : m1.find? a = some e₂ := byMaybeEntityData.asPartial
+    have h_find1 : m1.find? a = some e₂ := by
       rw [h_case] at h_find
-      simp only [Option.none_or] at h_fMaybeEntityData.asPartial
-      rw [h_find]MaybeEntityData.asPartial
+      simp only [Option.none_or] at h_find
+      rw [h_find]
     exact h1 a e₂ h_find1
 
 
 theorem direct_request_and_entities_refine (req : Request) (es : Entities) :
   RequestAndEntitiesRefine req es req.asPartialRequest es.asPartial := by
   constructor
-  · exact as_partiaMaybeEntityData.asPartial_refines
+  · exact as_partial_request_refines
   · unfold EntitiesRefine Entities.asPartial
     intro uid data₂ h_find
     have h_mapOnValues := Map.find?_mapOnValues_some' EntityData.asPartial h_find
-    obtain ⟨data₁, h_find₁, h_eq⟩ := h_MaybeEntityData.asPartial
+    obtain ⟨data₁, h_find₁, h_eq⟩ := h_mapOnValues
     exists data₁
     exact ⟨h_find₁,
            by rw [h_eq]; apply PartialIsValid.some; rfl,
@@ -105,8 +105,8 @@ theorem batched_eval_loop_eq_evaluate
   case h_1 => simp only
   case h_2 iters n=>
     let toLoad := (Set.filter (fun uid => (Map.find? current_store uid).isNone) x.allLiteralUIDs)
-    let newEntities := ((loader toLoad).mapOnValues EntityDataOption.asPartial)
-    let newStore :=SlicedEntitiesrent_store
+    let newEntities := ((loader toLoad).mapOnValues MaybeEntityData.asPartial)
+    let newStore := newEntities ++ current_store
 
     have h₀₂ := h₀
     specialize h₀₂ toLoad
@@ -120,7 +120,7 @@ theorem batched_eval_loop_eq_evaluate
         · unfold RequestAndEntitiesRefine at h₂
           exact h₂.right
         · apply h₅
-    let newRes := SlicedEntitiesasPartialRequest newStore
+    let newRes := TPE.evaluate x req.asPartialRequest newStore
     have h₇ : (Residual.evaluate newRes req es).toOption = (Residual.evaluate x req es).toOption := by
       subst newRes
       rw [← partial_evaluate_is_sound h₁ h₃ h₆]

cedar-lean/Cedar/Thm/Data.lean

@@ -14,6 +14,8 @@
  limitations under the License.
 -/
 
+import Cedar.Thm.Data.Applicative
+import Cedar.Thm.Data.Option
 import Cedar.Thm.Data.Control
 import Cedar.Thm.Data.List
 import Cedar.Thm.Data.LT

cedar-lean/Cedar/Thm/TPE.lean

@@ -25,6 +25,8 @@ import Cedar.Thm.TPE.PreservesTypeOf
 import Cedar.Thm.TPE.Policy
 import Cedar.Thm.TPE.Authorizer
 import Cedar.Thm.TPE.WellTyped
+import Cedar.Thm.TPE.WellTypedCases
+import Cedar.Thm.TPE.ErrorFree
 import Cedar.Thm.Validation
 import Cedar.Thm.Authorization
 

cedar-lean/Cedar/Thm/Validation.lean

@@ -23,6 +23,8 @@ import Cedar.Thm.Validation.Validator
 import Cedar.Thm.Validation.RequestEntityValidation
 import Cedar.Thm.Validation.EnvironmentValidation
 import Cedar.Thm.Validation.Levels
+import Cedar.Thm.Validation.SubstituteAction
+import Cedar.Thm.Validation.Typechecker
 
 /-!
 This file contains the top-level correctness properties for the Cedar validator.

cedar-lean/Cedar/Thm/Validation/Typechecker.lean

@@ -25,6 +25,10 @@ import Cedar.Thm.Validation.Typechecker.Record
 import Cedar.Thm.Validation.Typechecker.Set
 import Cedar.Thm.Validation.Typechecker.Or
 import Cedar.Thm.Validation.Typechecker.UnaryApp
+import Cedar.Thm.Validation.Typechecker.LUB
+import Cedar.Thm.Validation.Typechecker.WF
+import Cedar.Thm.Validation.Typechecker.Basic
+import Cedar.Thm.Validation.Typechecker.Types
 
 /-!
 This file contains useful definitions and lemmas about the `Typechecker` functions.

cedar-lean/lakefile.lean

@@ -62,23 +62,39 @@ lean_exe CedarSymTests where
 lean_exe Cli where
   root := `Cli.Main
 
+-- Check that a .lean file imports all files in its corresponding directory
+partial def checkThmFile (module : String) (paths : List System.FilePath) : IO Nat := do
+  let path := paths.head!
+  let dir := path.withExtension ""
+  if ← dir.isDir then
+    let contents ← paths.mapM IO.FS.readFile
+    let mod_files ← dir.readDir
+    let mut exitCode := 0
+
+    for file in mod_files.toList do
+      let file_name := file.fileName
+      if file_name.endsWith ".lean" then
+        let subModule := s!"{module}.{file_name.dropRight 5}"
+        let expectedImport := s!"import {subModule}\n"
+        if contents.all λ content => (content.replace expectedImport "" == content) then
+          IO.println s!"{path} missing import: {expectedImport}"
+          exitCode := 1
+        let subExitCode ← checkThmFile subModule [dir / file_name]
+        if subExitCode != 0 then
+          exitCode := subExitCode
+
+    return exitCode
+  else
+    return 0
+
 /--
-Check that Cedar.Thm imports all top level proofs.
+Check that Cedar.Thm imports all top level proofs recursively.
 
 USAGE:
   lake run checkThm
   lake lint
 -/
 @[lint_driver]
 script checkThm do
-  let thm ← IO.FS.readFile ⟨"Cedar/Thm.lean"⟩
-  let symcc ← IO.FS.readFile ⟨"SymCC.lean"⟩
-  let dir ← System.FilePath.readDir ⟨"Cedar/Thm/"⟩
-  for entry in dir.toList do
-    let fn := entry.fileName
-    if fn.endsWith ".lean" then
-      let ln := s!"import Cedar.Thm.{fn.dropRight 5}\n"
-      if thm.replace ln "" == thm && symcc.replace ln "" == symcc then
-        IO.println s!"Neither Cedar.Thm nor SymCC imports Cedar/Thm/{fn}"
-        return 1
-  return 0
+  let exitCode ← checkThmFile "Cedar.Thm" [⟨"Cedar/Thm.lean"⟩, ⟨"SymCC.lean"⟩]
+  return ⟨exitCode⟩