TPE soundness proofs (#595)

Signed-off-by: Shaobo He <[email protected]>
Signed-off-by: Emina Torlak <[email protected]>
Co-authored-by: Emina Torlak <[email protected]>

Author: shaobo-he-aws

cedar-lean/Cedar/TPE/Evaluator.lean

@@ -70,7 +70,7 @@ def or : Residual → Residual → CedarType → Residual
   | .val false _, r, _ => r
   | .error _, _, ty    => .error ty
   | l, .val false _, _ => l
-  | l, r, ty           => .and l r ty
+  | l, r, ty           => .or l r ty
 
 def apply₁ (op₁ : UnaryOp) (r : Residual) (ty : CedarType) : Residual :=
   match r with
@@ -95,46 +95,52 @@ def getTag (uid : EntityUID) (tag : String) (es : PartialEntities) (ty : CedarTy
   | .none => .binaryApp .getTag uid tag ty
 
 def apply₂ (op₂ : BinaryOp) (r₁ r₂ : Residual) (es : PartialEntities) (ty : CedarType) : Residual :=
-  match op₂, r₁, r₂ with
-  | .eq, .val v₁ _, .val v₂ _ =>
-    .val (v₁ == v₂) ty
-  | .less, .val (.prim (.int i)) _, .val (.prim (.int j)) _ =>
-    .val (i < j : Bool) ty
-  | .less, .val (.ext (.datetime d₁)) _, .val (.ext (.datetime d₂)) _ =>
-    .val (d₁ < d₂: Bool) ty
-  | .less, .val (.ext (.duration d₁)) _, .val (.ext (.duration d₂)) _ =>
-    .val (d₁ < d₂: Bool) ty
-  | .lessEq, .val (.prim (.int i)) _, .val (.prim (.int j)) _ =>
-    .val (i ≤ j : Bool) ty
-  | .lessEq, .val (.ext (.datetime d₁)) _, .val (.ext (.datetime d₂)) _ =>
-    .val (d₁ ≤ d₂: Bool) ty
-  | .lessEq, .val (.ext (.duration d₁)) _, .val (.ext (.duration d₂)) _ =>
-    .val (d₁ ≤ d₂: Bool) ty
-  | .add, .val (.prim (.int i)) _, .val (.prim (.int j)) _ =>
-    someOrError (i.add? j) ty
-  | .sub, .val (.prim (.int i)) _, .val (.prim (.int j)) _ =>
-    someOrError (i.sub? j) ty
-  | .mul, .val (.prim (.int i)) _, .val (.prim (.int j)) _ =>
-    someOrError (i.mul? j) ty
-  | .contains, .val (.set vs₁) _, .val v₂ _ =>
-    .val (vs₁.contains v₂) ty
-  | .containsAll, .val (.set vs₁) _, .val (.set vs₂) _ =>
-    .val (vs₂.subset vs₁) ty
-  | .containsAny, .val (.set vs₁) _, .val (.set vs₂) _ =>
-    .val (vs₁.intersects vs₂) ty
-  | .mem, .val (.prim (.entityUID uid₁)) _, .val (.prim (.entityUID uid₂)) _ =>
-    someOrSelf (inₑ uid₁ uid₂ es) ty self
-  | .mem, .val (.prim (.entityUID uid₁)) _, .val (.set vs) _ =>
-    someOrSelf (inₛ uid₁ vs es) ty self
-  | .hasTag, .val (.prim (.entityUID uid₁)) _, .val (.prim (.string tag)) _ =>
-    someOrSelf (hasTag uid₁ tag es) ty self
-  | .getTag, .val (.prim (.entityUID uid₁)) _, .val (.prim (.string tag)) _ =>
-    getTag uid₁ tag es ty
-  | _, .error _, _ | _, _, .error _ => .error ty
-  | _, _, _ => self
-where
+  match r₁.asValue, r₂.asValue with
+  | .some v₁, .some v₂ =>
+    match op₂, v₁, v₂ with
+    | .eq, _, _ =>
+      .val (v₁ == v₂) ty
+    | .less, .prim (.int i), .prim (.int j) =>
+      .val (i < j : Bool) ty
+    | .less, .ext (.datetime d₁), .ext (.datetime d₂) =>
+      .val (d₁ < d₂: Bool) ty
+    | .less, .ext (.duration d₁), .ext (.duration d₂) =>
+      .val (d₁ < d₂: Bool) ty
+    | .lessEq, .prim (.int i), .prim (.int j) =>
+      .val (i ≤ j : Bool) ty
+    | .lessEq, .ext (.datetime d₁), .ext (.datetime d₂) =>
+      .val (d₁ ≤ d₂: Bool) ty
+    | .lessEq, .ext (.duration d₁), .ext (.duration d₂) =>
+      .val (d₁ ≤ d₂: Bool) ty
+    | .add, .prim (.int i), .prim (.int j) =>
+      someOrError (i.add? j) ty
+    | .sub, .prim (.int i), .prim (.int j) =>
+      someOrError (i.sub? j) ty
+    | .mul, .prim (.int i), .prim (.int j) =>
+      someOrError (i.mul? j) ty
+    | .contains, .set vs₁, _ =>
+      .val (vs₁.contains v₂) ty
+    | .containsAll, .set vs₁, .set vs₂ =>
+      .val (vs₂.subset vs₁) ty
+    | .containsAny, .set vs₁, .set vs₂ =>
+      .val (vs₁.intersects vs₂) ty
+    | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) =>
+      someOrSelf (inₑ uid₁ uid₂ es) ty self
+    | .mem, .prim (.entityUID uid₁), .set vs =>
+      someOrSelf (inₛ uid₁ vs es) ty self
+    | .hasTag, .prim (.entityUID uid₁), .prim (.string tag) =>
+      someOrSelf (hasTag uid₁ tag es) ty self
+    | .getTag, .prim (.entityUID uid₁), .prim (.string tag) =>
+      getTag uid₁ tag es ty
+    | _, _, _ => .error ty
+  | _, _ =>
+    match r₁, r₂ with
+    | .error _, _ | _, .error _ => .error ty
+    | _, _ => self
+  where
   self := .binaryApp op₂ r₁ r₂ ty
 
+
 def attrsOf (r : Residual) (lookup : EntityUID → Option (Map Attr Value)) : Option (Map Attr Value) :=
   match r with
   | .val (.record m) _              => .some m
@@ -210,6 +216,18 @@ decreasing_by
     try simp at h
     omega
 
+/-- Partially evaluating a policy.
+Note that this function actually evaluates a type-lifted version of `TypedExpr`
+produced by the type checker, as opposed to evaluating the expression directly.
+This design is to simplify proofs otherwise we need to prove theorems that
+state type-lifting (i.e, `TypedExpr.liftBoolTypes`) do not change the results
+of evaluating residuals. The soundness theorem still holds. That is,
+reauthorizing the residuals produces the same outcome as authorizing the input
+expressions with consistent requests/entities. It is just that the types in the
+residuals are all lifted. We essentially trade efficiency for ease of proofs,
+which I (Shaobo) think is fine because the Lean model is a reference model not
+used in production.
+-/
 def evaluatePolicy (schema : Schema)
   (p : Policy)
   (req : PartialRequest)
@@ -222,7 +240,7 @@ def evaluatePolicy (schema : Schema)
         do
           let expr := substituteAction env.reqty.action p.toExpr
           let (te, _) ← (typeOf expr ∅ env).mapError Error.invalidPolicy
-          .ok (evaluate te req es)
+          .ok (evaluate te.liftBoolTypes req es)
       else .error .invalidRequestOrEntities
     | .none => .error .invalidEnvironment
 

cedar-lean/Cedar/TPE/Input.lean

@@ -50,7 +50,7 @@ structure PartialEntityData where
 
 abbrev PartialEntities := Map EntityUID PartialEntityData
 
-private def PartialEntities.get (es : PartialEntities) (uid : EntityUID) (f : PartialEntityData → Option α) : Option α :=
+def PartialEntities.get (es : PartialEntities) (uid : EntityUID) (f : PartialEntityData → Option α) : Option α :=
   (es.find? uid).bind f
 
 def PartialEntities.ancestors (es : PartialEntities) (uid : EntityUID) : Option (Set EntityUID) := es.get uid PartialEntityData.ancestors
@@ -62,13 +62,12 @@ def PartialEntities.attrs (es : PartialEntities) (uid : EntityUID) : Option (Map
 def partialIsValid {α} (o : Option α) (f : α → Bool) : Bool :=
   (o.map f).getD true
 
--- We do not check if `req`'s action is valid (i.e, if it's contained in `env`)
--- because this function is called after validation, which already ensures it
 def requestIsValid (env : Environment) (req : PartialRequest) : Bool :=
   (partialIsValid req.principal.asEntityUID λ principal =>
-    instanceOfEntityType principal principal.ty env.ets.entityTypeMembers?) &&
+    instanceOfEntityType principal env.reqty.principal env.ets.entityTypeMembers?) &&
+  req.action == env.reqty.action &&
   (partialIsValid req.resource.asEntityUID λ resource =>
-    instanceOfEntityType resource resource.ty env.ets.entityTypeMembers?) &&
+    instanceOfEntityType resource env.reqty.resource env.ets.entityTypeMembers?) &&
   (partialIsValid req.context λ m =>
     instanceOfType (.record m) (.record env.reqty.context) env.ets)
 
@@ -103,11 +102,14 @@ inductive ConcretizationError
   | typeError
   | requestsDoNotMatch
   | entitiesDoNotMatch
+  | invalidEnvironment
 
-def isConsistent (env : Environment) (req₁ : Request) (es₁ : Entities) (req₂ : PartialRequest) (es₂ : PartialEntities) : Except ConcretizationError Unit :=
-  do requestIsConsistent; entitiesIsConsistent
+def isValidAndConsistent (schema : Schema) (req₁ : Request) (es₁ : Entities) (req₂ : PartialRequest) (es₂ : PartialEntities) : Except ConcretizationError Unit :=
+  match schema.environment? req₂.principal.ty req₂.resource.ty req₂.action with
+  | .some env => do requestIsConsistent env; entitiesIsConsistent env
+  | .none => .error .invalidEnvironment
 where
-  requestIsConsistent :=
+  requestIsConsistent env :=
   if !requestIsValid env req₂ || !requestMatchesEnvironment env req₁
   then
     .error .typeError
@@ -122,7 +124,7 @@ where
       .ok ()
     else
       .error .requestsDoNotMatch
-  entitiesIsConsistent : Except ConcretizationError Unit :=
+  entitiesIsConsistent env : Except ConcretizationError Unit :=
     if !entitiesIsValid env es₂ || !(entitiesMatchEnvironment env es₁).isOk
     then
       .error .typeError

cedar-lean/Cedar/TPE/Residual.lean

@@ -96,7 +96,7 @@ def Residual.evaluate (x : Residual) (req : Request) (es: Entities) : Result Val
     Cedar.Spec.hasAttr v a es
   | .getAttr e a _ => do
     let v ← e.evaluate req es
-    Cedar.Spec.hasAttr v a es
+    Cedar.Spec.getAttr v a es
   | .set xs _ => do
     let vs ← xs.mapM₁ (fun ⟨x₁, _⟩ => evaluate x₁ req es)
     .ok (Set.make vs)

cedar-lean/Cedar/Thm.lean

@@ -20,3 +20,4 @@ import Cedar.Thm.PolicySlice
 import Cedar.Thm.Typechecking
 import Cedar.Thm.Validation
 import Cedar.Thm.WellTyped
+import Cedar.Thm.TPE

cedar-lean/Cedar/Thm/Data/Control.lean

@@ -57,7 +57,96 @@ theorem do_error {res : Except ε α} {e : ε} {f : α → β} :
   res = .error e
 := by cases res <;> simp
 
-theorem do_ok {res : Except ε α} {f : α → β} :
+theorem do_ok_eq_ok {res : Except ε α} {f : α → β} :
   (do let v ← res ; .ok (f v)) = .ok b ↔
   ∃ a, res = .ok a ∧ f a = b
 := by cases res <;> simp
+
+theorem do_eq_ok {res : Except ε α} {f : α → Except ε β} :
+  (do let v ← res ; f v) = .ok b ↔
+  ∃ a, res = .ok a ∧ f a = .ok b
+:= by cases res <;> simp
+
+theorem do_eq_ok₂ {res₁ res₂: Except ε PUnit} :
+  (do res₁ ; res₂) = .ok () → res₁ = .ok () ∧ res₂ = .ok ()
+:= by
+  cases res₁ <;> cases res₂ <;> simp
+
+theorem to_option_some {v : α} {res: Except ε α} :
+  res.toOption = .some v ↔ res = .ok v
+:= by
+  constructor
+  case mp =>
+    intro h
+    simp [Except.toOption] at h
+    split at h <;> simp at h
+    subst h
+    rfl
+  case mpr =>
+    intro h
+    simp only [Except.toOption, h]
+
+theorem to_option_none {res: Except ε α} :
+  res.toOption = .none → (∃ err, res = .error err)
+:= by
+  intro h
+  simp [Except.toOption] at h
+  split at h <;> simp at h
+  rename_i err
+  exists err
+
+theorem to_option_left_ok {α ε₁ ε₂} {v : α} {res₁ : Except ε₁ α} {res₂ : Except ε₂ α} :
+  res₁.toOption = res₂.toOption → res₁ = .ok v → res₂ = .ok v
+:= by
+  intro h₀ h₁
+  simp [Except.toOption] at h₀
+  repeat split at h₀
+  · simp only [Except.ok.injEq]
+    simp only [Option.some.injEq] at h₀
+    simp only [Except.ok.injEq] at h₁
+    simp only [← h₀]; exact h₁
+  · cases h₀
+  · cases h₁
+
+theorem to_option_right_ok {α ε₁ ε₂} {v : α} {res₁ : Except ε₁ α} {res₂ : Except ε₂ α} :
+  res₁.toOption = res₂.toOption → res₂ = .ok v → res₁ = .ok v
+:= by
+  intro h
+  symm at h
+  exact to_option_left_ok h
+
+theorem to_option_right_ok' {α ε₁ ε₂} {v : α} {res₁ : Except ε₁ α} :
+  res₁.toOption = ((.ok v) : Except ε₂ α).toOption → res₁ = Except.ok v
+:= by
+  generalize h : ((.ok v) : Except ε₂ α) = res₂
+  symm at h
+  intro h₁
+  exact to_option_right_ok h₁ h
+
+theorem to_option_left_ok' {α ε₁ ε₂} {v : α} {res₂ : Except ε₂ α} :
+  ((.ok v) : Except ε₁ α).toOption = res₂.toOption → res₂ = Except.ok v
+:= by
+  intro h
+  symm at h
+  exact to_option_right_ok' h
+
+theorem to_option_left_err {ε₁ ε₂ α} {err₁: ε₁} {res₂ : Except ε₂ α} :
+  (Except.error err₁).toOption = res₂.toOption → ∃ err₂, res₂ = .error err₂
+:= by
+  intro h
+  simp [Except.toOption] at h
+  repeat split at h
+  · cases h
+  · simp only [Except.error.injEq, exists_eq']
+
+theorem to_option_right_err {ε₂ ε₁ α} {err₂: ε₂} {res₁ : Except ε₁ α} :
+  res₁.toOption = (Except.error err₂).toOption → ∃ err₁, res₁ = .error err₁
+:= by
+  intro h
+  symm at h
+  exact to_option_left_err h
+
+theorem do_error_to_option {res : Except ε α} {e : ε} :
+  (do let (_ : α) ← res ; (.error e : Except ε α)).toOption = .none
+:= by
+  cases res <;> simp [Except.toOption]

cedar-lean/Cedar/Thm/Data/List/Lemmas.lean

@@ -437,7 +437,7 @@ theorem mapM'_ok_iff_forall₂ {α β γ} {f : α → Except γ β} {xs : List 
       · simp only [reduceCtorEq] at h₁
       · simp only [reduceCtorEq] at h₁
       · rename_i yhd
-        replace ⟨ytl, h₁, h₃⟩ := do_ok.mp h₁
+        replace ⟨ytl, h₁, h₃⟩ := do_ok_eq_ok.mp h₁
         subst h₃
         exact List.Forall₂.cons h₂ (ih h₁)
   case mpr =>
@@ -852,6 +852,17 @@ theorem mapM_some_subset {f : α → Option β} {xs xs' : List α} {ys : List β
   simp only [← mapM'_eq_mapM]
   exact mapM'_some_subset
 
+theorem forall₂_implies_mapM_eq {α₁ α₂ β ε} {xs : List α₁} {ys : List α₂} (f : α₁ → Except ε β) (g : α₂ → Except ε β):
+  List.Forall₂ (fun x y => f x = g y) xs ys →
+  List.mapM f xs =
+  List.mapM g ys
+:= by
+  intro h
+  cases h
+  case nil => simp only [List.mapM_nil]
+  case cons h₁ h₂ =>
+    simp only [List.mapM_cons, h₁, forall₂_implies_mapM_eq f g h₂, bind_pure_comp]
+
 /--
   our own variant of map_congr, for mapM'
 -/