Skip to content

[in progress] Convergence of Batched Evaluation to a Value #737

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

Draft
oflatt wants to merge 4 commits into
base: main
Choose a base branch
from
Draft

[in progress] Convergence of Batched Evaluation to a Value #737

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
82dd360
working on termination proof
oflatt Aug 29, 2025
86f4127
fix rebase
oflatt Sep 11, 2025
edb615b
small build errors
oflatt Sep 11, 2025
73ba185
small progress
oflatt Sep 11, 2025
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
10 changes: 5 additions & 5 deletions cedar-lean/Cedar/TPE/BatchedEvaluator.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ Loads everything requested by the set of entity ids,
Loading more entities than requested is okay.
See `EntityLoader.WellBehaved` for a formal definition.
-/
abbrev EntityLoader := Set EntityUID → Map EntityUID MaybeEntityData
abbrev EntityLoader := Set EntityUID → SlicedEntities

/--
The batched evaluation loop
Expand All @@ -46,15 +46,15 @@ def batchedEvalLoop
(residual : Residual)
(req : Request)
(loader : EntityLoader)
(store : PartialEntities)
(store : SlicedEntities)
: Nat → Residual
| 0 => residual
| n + 1 =>
let toLoad := residual.allLiteralUIDs.filter (λ uid => (store.find? uid).isNone)
let newEntities := ((loader toLoad).mapOnValues MaybeEntityData.asPartial)
let newStore := newEntities ++ store
let newEntities := (loader toLoad)
let newStore: SlicedEntities := newEntities ++ store

match Cedar.TPE.evaluate residual req.asPartialRequest newStore with
match Cedar.TPE.evaluate residual req.asPartialRequest newStore.asPartial with
| .val v _ty => .val v _ty
| newRes => batchedEvalLoop newRes req loader newStore n

Expand Down
2 changes: 1 addition & 1 deletion cedar-lean/Cedar/TPE/Input.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ def MaybeEntityData.asPartial :
| some d =>
d.asPartial

def EntitiesWithMissing.asPartial (store: SlicedEntities) : PartialEntities :=
def SlicedEntities.asPartial (store: SlicedEntities) : PartialEntities :=
store.mapOnValues MaybeEntityData.asPartial

end Cedar.TPE
34 changes: 34 additions & 0 deletions cedar-lean/Cedar/TPE/Residual.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,40 @@ decreasing_by
simp at *
omega

def Residual.treeSize (r: Residual) : Nat :=
match r with
| Residual.val _ _ => 1
| Residual.var _ _ => 2
| Residual.error _ => 2
| Residual.ite cond thenExpr elseExpr _ =>
2 + cond.treeSize + thenExpr.treeSize + elseExpr.treeSize
| Residual.and a b _ =>
2 + a.treeSize + b.treeSize
| Residual.or a b _ =>
2 + a.treeSize + b.treeSize
| Residual.unaryApp _ expr _ =>
2 + expr.treeSize
| Residual.binaryApp _ a b _ =>
2 + a.treeSize + b.treeSize
| Residual.getAttr expr _ _ =>
2 + expr.treeSize
| Residual.hasAttr expr _ _ =>
2 + expr.treeSize
| Residual.set ls _ =>
2 + (ls.map₁ (fun ⟨r, _⟩ =>
r.treeSize)).sum
| Residual.record map _ =>
2 + (map.map₁ (fun ⟨(_, r), _⟩ => r.treeSize)).sum
| Residual.call _ args _ =>
2 + (args.map₁ (fun ⟨r, _⟩ => r.treeSize)).sum
termination_by sizeOf r
decreasing_by
any_goals
simp
omega
all_goals sorry




mutual
Expand Down
4 changes: 4 additions & 0 deletions cedar-lean/Cedar/Thm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,4 +21,8 @@ import Cedar.Thm.Typechecking
import Cedar.Thm.Validation
import Cedar.Thm.WellTyped
import Cedar.Thm.TPE
-- TODO move BatchedEvaluator to own folder
-- TODO prove termination and remove BatchedTermination here
import Cedar.Thm.TPE.BatchedEvaluator
import Cedar.Thm.TPE.BatchedTermination
import Cedar.Thm.WellTypedVerification
34 changes: 25 additions & 9 deletions cedar-lean/Cedar/Thm/Data/Map.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -363,6 +363,16 @@ theorem find?_mem_toList {α β} [LT α] [DecidableLT α] [DecidableEq α] {m :
simp only [beq_iff_eq] at h₃ ; subst h₃
exact List.mem_of_find?_eq_some h₂

theorem in_keys_iff_find?_some [DecidableEq α] {k : α} {m : Map α β}:
(k ∈ m) ↔ ∃v, m.find? k = some v
:= by
constructor
case mp =>
intro h₁
sorry
case mpr =>
sorry

/--
The `mpr` direction of this does not need the `wf` precondition and, in fact,
is available separately as `find?_mem_toList` above
Expand Down Expand Up @@ -939,18 +949,15 @@ theorem in_mapOnValues_in_kvs [LT α] [DecidableLT α] [StrictLT α] [DecidableE
/--
Slightly different formulation of `in_mapOnValues_in_kvs`
-/
theorem in_mapOnValues_in_kvs' [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {f : β → γ} {m : Map α β} {k : α} {v' : γ}
(wf : m.WellFormed) :
theorem in_mapOnValues_in_kvs' {f : β → γ} {m : Map α β} {k : α} {v' : γ}:
(k, v') ∈ (m.mapOnValues f).kvs →
∃ v, f v = v' ∧ (k, v) ∈ m.kvs
:= by
rw [mapOnValues_eq_make_map f wf]
unfold toList
intro h₁
replace h₁ := make_mem_list_mem h₁
replace ⟨(k', v'), h₁, h₂⟩ := List.mem_map.mp h₁
simp only [Prod.mk.injEq] at h₂ ; replace ⟨h₂', h₂⟩ := h₂ ; subst k' h₂
exists v'
simp [mapOnValues, Map.kvs]
intro x y h xk h₂
subst xk
subst h₂
exists y

/-! ### mapMOnValues -/

Expand Down Expand Up @@ -1662,4 +1669,13 @@ theorem find?_append
cases List.find? (fun x => x.fst == k) m₂.kvs <;> simp
. simp

theorem mapOnValues_append
[LT α] [StrictLT α] [DecidableEq α] [DecidableLT α]
{m₁ m₂ : Map α β} {k : α}:
(m₁ ++ m₂).mapOnValues f = (m₁.mapOnValues f) ++ (m₂.mapOnValues f)
:= by
simp [mapOnValues]
simp [HAppend.hAppend]
sorry

end Cedar.Data.Map
73 changes: 44 additions & 29 deletions cedar-lean/Cedar/Thm/TPE/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).asPartial)

theorem as_partial_request_refines {req : Request} :
RequestRefines req req.asPartialRequest := by
Expand All @@ -51,52 +51,66 @@ theorem any_refines_empty_entities :
intro a e₂ h₁
contradiction

-- Helper lemma for map append refinementSlicedEntities
theorem entities_refine_append (es : Entities) (m1 m2 : PartialEntities) :
EntitiesRefine es m1 → EntitiesRefine es m2 → EntitiesRefine es (m2 ++ m1) := by
theorem withMissing_asPartial_append {m1 m2 : SlicedEntities} :
SlicedEntities.asPartial (m1 ++ m2) = m1.asPartial ++ m2.asPartial := by
sorry

-- Helper lemma for map append refinement
theorem entities_refine_withMissing_asPartial_append (es : Entities) (m2 m1 : SlicedEntities) :
EntitiesRefine es m1.asPartial → EntitiesRefine es m2.asPartial → EntitiesRefine es (SlicedEntities.asPartial (m1 ++ m2)) := by
intro h1 h2
unfold EntitiesRefine
intro a e₂ h_findSlicedEntities
intro a e₂ h_find
rw [withMissing_asPartial_append] at h_find

rw [Map.find?_append] at h_find
cases h_case : m2.find? a with
| some e₂' =>
have h_eq : e₂ = e₂' := by
rw [h_case] at h_find
simp only [Option.some_or, Option.some.injEq] at h_find
rw [h_find]
cases h_case : m1.find? a with
| some e₁' =>
unfold SlicedEntities.asPartial at h_find
have h_find₂ : Map.find? m1.asPartial a = some e₁'.asPartial := by
unfold SlicedEntities.asPartial
exact Map.find?_mapOnValues_some MaybeEntityData.asPartial h_case
have h_eq : e₂ = e₁'.asPartial := by
unfold SlicedEntities.asPartial at h_find₂
rw [h_find₂] at h_find
simp [Option.or] at h_find
exact h_find.symm
rw [h_eq]
exact h2 a e₂' h_case

exact h1 a e₁'.asPartial h_find₂
| none =>
have h_find1 : m1.find? a = some e₂ := byMaybeEntityData.asPartial
rw [h_case] at h_find
simp only [Option.none_or] at h_fMaybeEntityData.asPartial
rw [h_find]MaybeEntityData.asPartial
exact h1 a e₂ h_find1
have h_find₃ : m1.asPartial.find? a = none := by
unfold SlicedEntities.asPartial
exact Map.find?_mapOnValues_none MaybeEntityData.asPartial h_case
rw [h_find₃] at h_find
simp [Option.or] at h_find
exact h2 a e₂ h_find


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,
by rw [h_eq]; apply PartialIsValid.some; rfl,
by rw [h_eq]; apply PartialIsValid.some; rfl⟩


theorem batched_eval_loop_eq_evaluate
{x : Residual}
{req : Request}
(es : Entities)
{current_store : PartialEntities}
{current_store : SlicedEntities}
{env : TypeEnv} :
EntityLoader.WellBehaved es loader →
Residual.WellTyped env x →
RequestAndEntitiesRefine req es req.asPartialRequest current_store →
RequestAndEntitiesRefine req es req.asPartialRequest current_store.asPartial →
InstanceOfWellFormedEnvironment req es env →
(Residual.evaluate (batchedEvalLoop x req loader current_store iters) req es).toOption = (Residual.evaluate x req es).toOption := by
intro h₀ h₁ h₂ h₃
Expand All @@ -105,22 +119,23 @@ 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)
let newStore: SlicedEntities := newEntities ++ current_store

have h₀₂ := h₀
specialize h₀₂ toLoad
obtain ⟨h₄, h₅⟩ := h₀₂

have h₆ : RequestAndEntitiesRefine req es req.asPartialRequest newStore := by
have h₆ : RequestAndEntitiesRefine req es req.asPartialRequest newStore.asPartial := by
unfold RequestAndEntitiesRefine
constructor
· exact as_partial_request_refines
· apply entities_refine_append
· unfold RequestAndEntitiesRefine at h₂
exact h₂.right
· apply h₅
let newRes := SlicedEntitiesasPartialRequest newStore
· subst newStore
apply entities_refine_withMissing_asPartial_append
· exact h₅
· obtain ⟨_, h₂⟩ := h₂
exact h₂
let newRes := TPE.evaluate x req.asPartialRequest newStore.asPartial
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
Loading