Skip to content

Repair batched evaluation proof #833

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
john-h-kastner-aws wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Repair batched evaluation proof #833

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
38a8ab2
repair batched evaluation proof
john-h-kastner-aws Jan 22, 2026
e5eb486
recursive checkThm
john-h-kastner-aws Jan 22, 2026
03f3cf3
stricter recursive import check
john-h-kastner-aws Jan 22, 2026
01e4fcc
Restore `\n` in expected import text
john-h-kastner-aws Jan 22, 2026
d0b828e
rebase and add import
john-h-kastner-aws Jan 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions cedar-lean/Cedar/Thm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 2 additions & 0 deletions cedar-lean/Cedar/Thm/Authorization.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
22 changes: 11 additions & 11 deletions ...-lean/Cedar/Thm/TPE/BatchedEvaluator.lean → cedar-lean/Cedar/Thm/BatchedEvaluator.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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₂' =>
Expand All @@ -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,
Expand All @@ -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
Expand All @@ -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₆]
Expand Down
2 changes: 2 additions & 0 deletions cedar-lean/Cedar/Thm/Data.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions cedar-lean/Cedar/Thm/TPE.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ import Cedar.Thm.TPE.Conversion
import Cedar.Thm.TPE.Soundness
import Cedar.Thm.TPE.PreservesTypeOf
import Cedar.Thm.TPE.WellTyped
import Cedar.Thm.TPE.WellTypedCases
import Cedar.Thm.TPE.ErrorFree
import Cedar.Thm.Validation

/-!
Expand Down
2 changes: 2 additions & 0 deletions cedar-lean/Cedar/Thm/Validation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 4 additions & 0 deletions cedar-lean/Cedar/Thm/Validation/Typechecker.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
40 changes: 28 additions & 12 deletions cedar-lean/lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩