Project-declaredLean 4.31.0 · null

Partial authorize allow determining policies is sound

Cedar.Thm.partial_authorize_allow_determining_policies_is_sound

authorization program verification semantics tpe

Plain-language statement

If the result of concrete authorization is allow, then all permit policies satisfied after partial authorization are determining policies.

Exact Lean statement

theorem partial_authorize_allow_determining_policies_is_sound
  {schema : Schema}
  {policies : List Policy}
  {req : Request}
  {es : Entities}
  {preq : PartialRequest}
  {pes : PartialEntities}
  {response : TPE.Response} :
  TPE.isAuthorized schema policies preq pes = Except.ok response →
  isValidAndConsistent schema req es preq pes = Except.ok () →
  (Spec.isAuthorized req es policies).decision = .allow →
  response.satisfiedPermits ⊆ (Spec.isAuthorized req es policies).determiningPolicies

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem partial_authorize_allow_determining_policies_is_sound  {schema : Schema}  {policies : List Policy}  {req : Request}  {es : Entities}  {preq : PartialRequest}  {pes : PartialEntities}  {response : TPE.Response} :  TPE.isAuthorized schema policies preq pes = Except.ok response →  isValidAndConsistent schema req es preq pes = Except.ok () →  (Spec.isAuthorized req es policies).decision = .allow →  response.satisfiedPermits ⊆ (Spec.isAuthorized req es policies).determiningPolicies:= by  intro h₁ h₂ h_allow  simp only [TPE.isAuthorized] at h₁   replace h_allow' : (satisfiedPolicies Effect.forbid policies req es).isEmpty ∧ ¬ (satisfiedPolicies Effect.permit policies req es).isEmpty := by    grind [Spec.isAuthorized]  simp only [Spec.isAuthorized, h_allow', Bool.not_false, Bool.and_self, ↓reduceIte]   cases h₃ : isAuthorized.evaluatePolicies schema policies preq pes <;>    simp [h₃] at h₁  subst h₁  have h_equiv := evaluatePolicies_residuals_equiv h₂ h₃  exact Set.subset_trans    (partial_authorize_satisfied_policies_is_sound .permit h_equiv)    (by simp [Set.subset_def])

Project: Cedar Specification
License: Apache-2.0
Commit: 3f093947b8ae
Source: cedar-lean/Cedar/Thm/TPE.lean:148-174

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.31.0

Find? ext

Cedar.Data.Map.find?_ext

Plain-language statement

Two well-formed maps are equal if they have the same find? for every key.

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Find? notmem keys

Cedar.Data.Map.find?_notmem_keys

Plain-language statement

Inverse of find?_mem_toList, except that this requires wf

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record

Project-declaredLean 4.31.0

Find? some iff in values

Cedar.Data.Map.find?_some_iff_in_values

Plain-language statement

The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above

authorizationprogram verificationsemantics

Source project: Cedar Specification

Person-level attribution pending.

View proof record