Cleanup in validator spec (#159)

cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean

@@ -84,18 +84,18 @@ For every entity in the store,
 -/
 def InstanceOfEntityTypeStore (entities : Entities) (ets: EntityTypeStore) : Prop :=
   ∀ uid data, entities.find? uid = some data →
-    ∃ attrTys ancestorTys, ets.find? uid.ty = some (attrTys, ancestorTys) ∧
-      InstanceOfType data.attrs (.record attrTys) ∧
-      ∀ ancestor, ancestor ∈ data.ancestors → ancestor.ty ∈ ancestorTys
+    ∃ entry, ets.find? uid.ty = some entry ∧
+      InstanceOfType data.attrs (.record entry.attrs) ∧
+      ∀ ancestor, ancestor ∈ data.ancestors → ancestor.ty ∈ entry.ancestors
 
 /--
 For every action in the entity store, the action's ancestors are consistent
 with the ancestor information in the action store.
 -/
 def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop :=
   ∀ uid data, entities.find? uid = some data → as.contains uid →
-    ∃ ancestors, as.find? uid = some ancestors →
-      ∀ ancestor, ancestor ∈ data.ancestors → ancestor ∈ ancestors
+    ∃ entry, as.find? uid = some entry →
+      ∀ ancestor, ancestor ∈ data.ancestors → ancestor ∈ entry.ancestors
 
 def RequestAndEntitiesMatchEnvironment (env : Environment) (request : Request) (entities : Entities) : Prop :=
   InstanceOfRequestType request env.reqty ∧

cedar-lean/Cedar/Thm/Soundness.lean

@@ -19,7 +19,7 @@ import Cedar.Thm.Lemmas.Typechecker
 import Mathlib.Data.List.Basic
 
 /-!
-This file defines the top-level soundness property for the valdator.
+This file defines the top-level soundness property for the validator.
 
 todo: fill in `sorry`s. Some invariants may need to be adjusted. The current
 definitions are an informed guess based on the corresponding Dafny proof.
@@ -46,50 +46,20 @@ theorem typecheck_policy_is_sound (policy : Policy) (env : Environment) (t : Ced
   typecheckPolicy policy env = .ok t →
   EvaluatesToBool policy request entities
 := by
-  intro h₀ h₁
-  unfold typecheckPolicy at h₁
-  cases h₂ : (typeOf (Policy.toExpr policy) ∅ env) <;>
-  rw [h₂] at h₁ <;>
-  simp at h₁
-  case ok res =>
-    cases h₃ : (res.fst ⊑ CedarType.bool BoolType.anyBool) <;>
-    rw [h₃] at h₁ <;>
-    simp at h₁
-    clear h₁ t
-    have h₁ : GuardedCapabilitiesInvariant policy.toExpr res.2 request entities ∧ ∃ (v : Value), EvaluatesTo policy.toExpr request entities v ∧ InstanceOfType v res.1 := by
-      apply type_of_is_sound (env:=env) (c₁:=∅)
-      apply empty_capabilities_invariant
-      apply h₀
-      apply h₂
-    cases h₁ with
-    | intro _ h₁ =>
-      cases h₁ with
-      | intro v h₁ =>
-        cases h₁ with
-        | intro h₁ h₄ =>
-          have h₅ : ∃ b, v = .prim (.bool b) := by
-            apply instance_of_type_bool_is_bool
-            apply h₄
-            apply h₃
-          cases h₅ with
-          | intro b h₅ =>
-            unfold EvaluatesToBool
-            exists b
-            rewrite [← h₅]
-            apply h₁
+  sorry
 
 def RequestMatchesSchema (schema : Schema) (request : Request) : Prop :=
   match schema.acts.find? request.action with
   | some entry =>
-      request.principal.ty ∈ entry.appliesToPricipal ∧
+      request.principal.ty ∈ entry.appliesToPrincipal ∧
       request.resource.ty ∈ entry.appliesToResource ∧
       InstanceOfType request.context (.record entry.context)
   | _ => False
 
 def RequestAndEntitiesMatchSchema (schema : Schema) (request : Request) (entities : Entities) : Prop :=
   RequestMatchesSchema schema request ∧
   InstanceOfEntityTypeStore entities schema.ets ∧
-  InstanceOfActionStore entities (schema.acts.mapOnValues (fun entry => entry.descendants))
+  InstanceOfActionStore entities (schema.acts.mapOnValues (fun entry => { ancestors := entry.ancestors }))
 
 /--
 Top-level soundness theorem: If validation succeeds, then for any request

cedar-lean/Cedar/Validation/Subtyping.lean

@@ -54,7 +54,7 @@ mutual
     | .record (.mk r₁), .record (.mk r₂) => do
       let lub ← lubRecordType r₁ r₂
       .some (.record (Map.mk lub))
-    | _, _ => .none
+    | _, _ => if ty₁ = ty₂ then .some ty₁ else  .none
 end
 
 def subty (ty₁ ty₂ : CedarType) : Bool :=
@@ -65,4 +65,4 @@ def subty (ty₁ ty₂ : CedarType) : Bool :=
 infix:50 " ⊔ " => lub?
 infix:50 " ⊑ " => subty
 
-end Cedar.Validation
+end Cedar.Validation

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -64,7 +64,7 @@ def typeOfIf (r₁ : CedarType × Capabilities) (r₂ r₃ : ResultType) : Resul
   match r₁ with
   | (.bool .tt, c₁) => do
     let (ty₂, c₂) ← r₂
-    ok ty₂ (c₁.union c₂)
+    ok ty₂ (c₁ ∪ c₂)
   | (.bool .ff, _) => r₃
   | (.bool .anyBool, c₁) => do
     let (ty₂, c₂) ← r₂
@@ -89,12 +89,16 @@ def typeOfAnd (r₁ : CedarType × Capabilities) (r₂ : ResultType) : ResultTyp
 def typeOfOr (r₁ : CedarType × Capabilities) (r₂ : ResultType) : ResultType :=
   match r₁ with
   | (.bool .tt, _)  => ok (.bool .tt)
-  | (.bool .ff, _)  => r₂
-  | (.bool ty₁, c₁) => do
+  | (.bool .ff, _)  => do
+    let (ty₂, c₂) ← r₂
+    match ty₂ with
+    | .bool _       => ok ty₂ c₂
+    | _             => err (.unexpectedType ty₂)
+  | (.bool _, c₁)   => do
     let (ty₂, c₂) ← r₂
     match ty₂ with
     | .bool .tt     => ok (.bool .tt)
-    | .bool .ff     => ok (.bool ty₁) c₁
+    | .bool .ff     => ok (.bool .anyBool) c₁
     | .bool _       => ok (.bool .anyBool) (c₁ ∩ c₂)
     | _             => err (.unexpectedType ty₂)
   | (ty₁, _)        => err (.unexpectedType ty₁)
@@ -174,21 +178,20 @@ def typeOfBinaryApp (op₂ : BinaryOp) (ty₁ ty₂ : CedarType) (x₁ x₂ : Ex
   | .containsAny, .set ty₃, .set ty₄        => ifLubThenBool ty₃ ty₄
   | _, _, _                                 => err (.unexpectedType ty₁)
 
-def hasAttrInRecord (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType :=
+def hasAttrInRecord (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) (knownToExist : Bool) : ResultType :=
   match rty.find? a with
-  | .some (.required _) => ok (.bool .tt)
-  | .some (.optional _) =>
-    if (x, a) ∈ c
+  | .some qty =>
+    if (x, a) ∈ c || (qty.isRequired && knownToExist)
     then ok (.bool .tt)
     else ok (.bool .anyBool) (Capabilities.singleton x a)
-  | .none               => ok (.bool .ff)
+  | .none     => ok (.bool .ff)
 
 def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env : Environment) : ResultType :=
   match ty with
-  | .record rty => hasAttrInRecord rty x a c
+  | .record rty => hasAttrInRecord rty x a c true
   | .entity ety =>
     match env.ets.attrs? ety with
-    | .some rty => hasAttrInRecord rty x a c
+    | .some rty => hasAttrInRecord rty x a c false
     | .none     => err (.unknownEntity ety)
   | _           => err (.unexpectedType ty)
 

cedar-lean/Cedar/Validation/Types.lean

@@ -74,22 +74,29 @@ inductive TypeError where
   | emptySetErr
   | incompatibleSetTypes (ty : List CedarType)
 
-abbrev EntityTypeStore := Map EntityType (RecordType × (Cedar.Data.Set EntityType))
+structure EntityTypeStoreEntry where
+  ancestors : Cedar.Data.Set EntityType
+  attrs : RecordType
+
+abbrev EntityTypeStore := Map EntityType EntityTypeStoreEntry
 
 def EntityTypeStore.contains (ets : EntityTypeStore) (ety : EntityType) : Bool :=
   (ets.find? ety).isSome
 
 def EntityTypeStore.attrs? (ets : EntityTypeStore) (ety : EntityType) : Option RecordType :=
-  (ets.find? ety).map Prod.fst
+  (ets.find? ety).map EntityTypeStoreEntry.attrs
 
 def EntityTypeStore.descendentOf (ets : EntityTypeStore) (ety₁ ety₂ : EntityType) : Bool :=
   if ety₁ = ety₂
   then true
   else match ets.find? ety₁ with
-    | .some (_, ancs) => ancs.contains ety₂
+    | .some entry => entry.ancestors.contains ety₂
     | .none => false
 
-abbrev ActionStore := Map EntityUID (Cedar.Data.Set EntityUID)
+structure ActionStoreEntry where
+  ancestors : Cedar.Data.Set EntityUID
+
+abbrev ActionStore := Map EntityUID ActionStoreEntry
 
 def ActionStore.contains (as : ActionStore) (uid : EntityUID) : Bool :=
   (as.find? uid).isSome
@@ -98,7 +105,7 @@ def ActionStore.descendentOf (as : ActionStore)  (uid₁ uid₂ : EntityUID) : B
   if uid₁ == uid₂
   then true
   else match as.find? uid₁ with
-    | .some ancs => ancs.contains uid₂
+    | .some entry => entry.ancestors.contains uid₂
     | .none => false
 
 ----- Derivations -----

cedar-lean/Cedar/Validation/Validator.lean

@@ -26,9 +26,9 @@ open Cedar.Data
 ----- Definitions -----
 
 structure SchemaActionEntry where
-  appliesToPricipal : Set EntityType
+  appliesToPrincipal : Set EntityType
   appliesToResource : Set EntityType
-  descendants : Set EntityUID
+  ancestors : Set EntityUID
   context : RecordType
 
 abbrev SchemaActionStore := Map EntityUID SchemaActionEntry
@@ -42,7 +42,7 @@ For a given action, compute the cross-product of the applicable principal and
 resource types.
 -/
 def SchemaActionEntry.toRequestTypes (action : EntityUID) (entry : SchemaActionEntry) : List RequestType :=
-  entry.appliesToPricipal.toList.foldl (fun acc principal =>
+  entry.appliesToPrincipal.toList.foldl (fun acc principal =>
     let reqtys : List RequestType :=
       entry.appliesToResource.toList.map (fun resource =>
         {
@@ -59,7 +59,7 @@ def Schema.toEnvironments (schema : Schema) : List Environment :=
     schema.acts.toList.foldl (fun acc (action,entry) => entry.toRequestTypes action ++ acc) ∅
   requestTypes.map ({
     ets := schema.ets,
-    acts := schema.acts.mapOnValues (fun entry => entry.descendants),
+    acts := schema.acts.mapOnValues (fun entry => { ancestors := entry.ancestors }),
     reqty := ·
   })
 
@@ -69,9 +69,58 @@ inductive ValidationError where
 
 abbrev ValidationResult := Except ValidationError Unit
 
+-- TODO: prove termination and get rid of `partial`
+partial def mapOnVars (f : Var → Expr) : Expr → Expr
+  | .lit l => .lit l
+  | .var var => f var
+  | .ite x₁ x₂ x₃ =>
+    let x₁ := mapOnVars f x₁
+    let x₂ := mapOnVars f x₂
+    let x₃ := mapOnVars f x₃
+    .ite x₁ x₂ x₃
+  | .and x₁ x₂ =>
+    let x₁ := mapOnVars f x₁
+    let x₂ := mapOnVars f x₂
+    .and x₁ x₂
+  | .or x₁ x₂ =>
+    let x₁ := mapOnVars f x₁
+    let x₂ := mapOnVars f x₂
+    .or x₁ x₂
+  | .unaryApp op₁ x₁ =>
+    let x₁ := mapOnVars f x₁
+    .unaryApp op₁ x₁
+  | .binaryApp op₂ x₁ x₂ =>
+    let x₁ := mapOnVars f x₁
+    let x₂ := mapOnVars f x₂
+    .binaryApp op₂ x₁ x₂
+  | .hasAttr x₁ a =>
+    let x₁ := mapOnVars f x₁
+    .hasAttr x₁ a
+  | .getAttr x₁ a =>
+    let x₁ := mapOnVars f x₁
+    .getAttr x₁ a
+  | .set xs =>
+    let xs := xs.map (mapOnVars f)
+    .set xs
+  | .record axs =>
+    let axs := axs.map (λ (k,v) => (k, mapOnVars f v))
+    .record axs
+  | .call xfn xs =>
+    let xs := xs.map (mapOnVars f)
+    .call xfn xs
+
+/- Substitute `action` variable for a literal EUID to improve typechecking precision. -/
+def substituteAction (uid : EntityUID) (expr : Expr) : Expr :=
+  let f (var : Var) : Expr :=
+    match var with
+    | .action => .lit (.entityUID uid)
+    | _ => .var var
+  mapOnVars f expr
+
 /-- Check that a policy is Boolean-typed. -/
 def typecheckPolicy (policy : Policy) (env : Environment) : Except ValidationError CedarType :=
-  match typeOf policy.toExpr ∅ env with
+  let expr := substituteAction env.reqty.action policy.toExpr
+  match typeOf expr ∅ env with
   | .ok (ty, _) =>
     if ty ⊑ .bool .anyBool
     then .ok ty