Update symcc opt path to use pre-compiled schema

[john-h-kastner-aws]

Draft PR since we'll also want to make the change to the Rust, and I need to fix up some FFI/CLI parts here. The main change to the Lean model is done and can be reviewed.

Makes the API change proposed here cedar-policy/cedar#2467 (comment)

This PR adds the CompiledSchema structure to Lean, and changes the CompiledPolicy to use it in its constructor.

-def CompiledPolicy.compile (p : Policy) (Γ : Validation.TypeEnv) : Except CompiledPolicyError CompiledPolicy := do
+def CompiledPolicy.compile (p : Policy) (s : CompiledSchema) (reqty : Validation.RequestType) : Except CompiledPolicyError CompiledPolicy := do
+  let Γ := s.typeEnv reqty
   let policy ← wellTypedPolicy p Γ |>.mapError .validationError
-  let εnv := SymEnv.ofEnv Γ
+  let εnv := s.symEnv reqty
   let { term, footprint } ← Opt.compile policy.toExpr εnv |>.mapError .symCCError
   let acyclicity := footprint.map (SymCC.acyclicity · εnv.entities)
   .ok { term, εnv, policy, footprint, acyclicity }

Proof are updated to show we can reuse this the compiled schema

theorem checkEquivalentOpt_eqv_checkEquivalent {ps₁ ps₂ : Policies} {Γ : Validation.TypeEnv} :
  Γ.WellFormed →
  (do
    let s := CompiledSchema.compile ⟨Γ.ets, Γ.acts⟩
    let cpset₁ ← CompiledPolicySet.compile ps₁ s Γ.reqty
    let cpset₂ ← CompiledPolicySet.compile ps₂ s Γ.reqty
    pure $ checkEquivalentOpt cpset₁ cpset₂
  ) =
  (do
    let wps₁ ← wellTypedPolicies ps₁ Γ |>.mapError .validationError
    let wps₂ ← wellTypedPolicies ps₂ Γ |>.mapError .validationError
    pure $ checkEquivalent wps₁ wps₂ (SymEnv.ofTypeEnv Γ)
  )

[Copilot]

Pull request overview

This PR refactors the Lean SymCCOpt compilation API to take a pre-compiled schema (CompiledSchema) plus a request type, so symbolic entities can be reused across multiple policy/policyset compilations. It also updates the corresponding SymCCOpt correctness theorems to use the new API shape.

Changes:

• Introduces Cedar.SymCC.CompiledSchema (schema + precomputed SymEntities) with helpers to derive SymEnv/TypeEnv for a RequestType.
• Updates CompiledPolicy.compile / CompiledPolicySet.compile to accept (s : CompiledSchema) and (reqty : RequestType) and reuse s.entities.
• Adjusts SymCCOpt proof layers and theorems to thread CompiledSchema/reqty instead of a raw TypeEnv.

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
cedar-lean/Cedar/Validation/Types.lean	Derives Inhabited for Schema to support new compiled-schema structures.
cedar-lean/Cedar/Thm/SymCC/Opt/Verifier.lean	Updates verifier equivalence theorems to use CompiledSchema + reqty.
cedar-lean/Cedar/Thm/SymCC/Opt/Extractor.lean	Updates extractor theorem hypotheses for new compile signatures.
cedar-lean/Cedar/Thm/SymCC/Opt/Enforcer.lean	Updates enforcer equivalence theorems to use s.typeEnv reqty / s.symEnv reqty.
cedar-lean/Cedar/Thm/SymCC/Opt/CompiledPolicies.lean	Updates compiled-policy correctness theorems for new compile API.
cedar-lean/Cedar/Thm/SymCC/Opt.lean	Bridges old Γ-based theorems to new compiled-schema API; updates many lemmas accordingly.
cedar-lean/Cedar/SymCCOpt/CompiledSchema.lean	Adds CompiledSchema and its compile, symEnv, and typeEnv helpers.
cedar-lean/Cedar/SymCCOpt/CompiledPolicies.lean	Changes public compilation API to accept pre-compiled schema + request type, reusing symbolic entities.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.