add proofs for implies?, equivalent?, disjoint?, alwaysAllows?, and alwaysDenies? (#796)

Signed-off-by: Craig Disselkoen <[email protected]>

Author: cdisselkoen

cedar-lean/Cedar/Spec/Policy.lean

@@ -136,6 +136,16 @@ def Scope.bound : Scope → Option EntityUID
   | .isMem _ uid => .some uid
   | _            => .none
 
+/-- The trivial allow-all policy -/
+def Policy.allowAll : Policy := {
+    id             := "allowAll",
+    effect         := .permit,
+    principalScope := .principalScope .any,
+    actionScope    := .actionScope .any,
+    resourceScope  := .resourceScope .any,
+    condition      := []
+}
+
 ----- Derivations -----
 
 deriving instance Repr, DecidableEq, Inhabited for Effect

cedar-lean/Cedar/SymCC/Enforcer.lean

@@ -130,9 +130,9 @@ where
 Returns the ground acyclicity and transitivity assumptions for xs and env.
 -/
 def enforce (xs : List Expr) (εnv : SymEnv) : Set Term :=
-  let (Set.mk ts) := footprints xs εnv
-  let ac := ts.map (acyclicity · εnv.entities)
-  let tr := ts.mapUnion (λ t => ts.map (transitivity t · εnv.entities))
+  let ts := footprints xs εnv
+  let ac := ts.elts.map (acyclicity · εnv.entities)
+  let tr := ts.elts.mapUnion (λ t => ts.elts.map (transitivity t · εnv.entities))
   Set.make (ac ∪ tr)
 
 namespace Cedar.SymCC

cedar-lean/Cedar/SymCC/Verifier.lean

@@ -75,13 +75,24 @@ Returns asserts that are unsatisfiable iff `ps` allows all inputs in `εnv`.
 def verifyAlwaysAllows (ps : Policies) (εnv : SymEnv) : Result Asserts := do
   verifyImplies [allowAll] ps εnv
 where
+  -- This policy chosen not because it's readable or optimized, but because it
+  -- is the policy produced by `wellTypedPolicy Policy.allowAll Γ`
   allowAll : Policy := {
     id             := "allowAll",
     effect         := .permit,
     principalScope := .principalScope .any,
     actionScope    := .actionScope .any,
     resourceScope  := .resourceScope .any,
-    condition      := []
+    condition      := [{
+      kind := .when,
+      body := Expr.and
+        (.lit (.bool true))
+        (Expr.and
+          (.lit (.bool true))
+          (Expr.and
+            (.lit (.bool true))
+            (.lit (.bool true))))
+    }]
   }
 
 /--

cedar-lean/Cedar/SymCCOpt/CompiledPolicies.lean

@@ -101,19 +101,11 @@ A `CompiledPolicies` that represents the policyset that allows all requests in
 the `εnv`.
 -/
 def CompiledPolicies.allowAll (εnv : SymEnv) : CompiledPolicies :=
-  let allowAll : Policy := {
-    id := "allowAll",
-    effect := .permit,
-    principalScope := .principalScope .any,
-    actionScope := .actionScope .any,
-    resourceScope := .resourceScope .any,
-    condition := [],
-  }
-  let footprint := SymCC.footprint allowAll.toExpr εnv
+  let footprint := SymCC.footprint verifyAlwaysAllows.allowAll.toExpr εnv
   {
     term := .bool true
     εnv
-    policies := [allowAll]
+    policies := [verifyAlwaysAllows.allowAll]
     footprint
     acyclicity := footprint.map (SymCC.acyclicity · εnv.entities)
   }

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

@@ -92,6 +92,37 @@ theorem mapUnion_wf {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → S
     simp only [List.foldl_cons]
     exact ih _ (Set.union_wf _ _)
 
+theorem mapUnion_empty {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → Set α} :
+  [].mapUnion f = ∅
+:= by
+  simp only [List.mapUnion, EmptyCollection.emptyCollection, List.foldl_nil]
+
+private theorem foldl_union_init {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → Set α} {xs : List β} {a b : Set α} :
+  List.foldl (λ acc x => acc ∪ f x) (a ∪ b) xs = a ∪ List.foldl (λ acc x => acc ∪ f x) b xs
+:= by
+  induction xs generalizing a b
+  case nil =>
+    simp only [List.foldl_nil]
+  case cons hd tl ih =>
+    simp only [List.foldl_cons]
+    rw [Set.union_assoc]
+    rw [ih (a := a) (b := b ∪ f hd)]
+
+theorem mapUnion_cons {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → Set α} {hd : β} {tl : List β} :
+  (∀ b, (f b).WellFormed) →
+  (hd :: tl).mapUnion f = f hd ∪ tl.mapUnion f
+:= by
+  intro hwf
+  simp only [List.mapUnion, EmptyCollection.emptyCollection, List.foldl_cons]
+  rw [Set.union_empty_left (hwf hd)]
+  rw [← Set.union_empty_left (hwf hd)]
+  rw [foldl_union_init (a := Set.empty) (b := f hd)]
+  rw [← foldl_union_init (a := Set.empty ∪ f hd) (b := Set.empty)]
+  have h : Set.empty ∪ f hd ∪ Set.empty = Set.empty ∪ f hd := by
+    rw [Set.union_empty_right (Set.union_wf _ _)]
+  rw [h]
+  rw [foldl_union_init (a := Set.empty) (b := f hd)]
+
 private theorem mem_foldl_union_iff_mem_or_exists {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → Set α} {xs : List β} {init : Set α} {a : α} :
   a ∈ List.foldl (λ as b => as ∪ f b) init xs ↔ (a ∈ init ∨ ∃ s ∈ xs, a ∈ f s)
 := by
@@ -192,6 +223,35 @@ theorem mapUnion_eq_mapUnion_id_map {α β} [LT α] [StrictLT α] [DecidableLT 
     simp only [List.foldl_cons, id_eq, List.map_cons]
     apply ih
 
+private theorem foldl_union_append {α β} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] {g : β → Set α} {xs ys : List β} {a : Set α} :
+  List.foldl (λ acc b => acc ∪ g b) a (xs.append ys) = List.foldl (λ acc b => acc ∪ g b) (List.foldl (λ acc b => acc ∪ g b) a xs) ys
+:= by
+  induction xs generalizing a
+  case nil =>
+    simp only [List.foldl_nil]
+    rfl
+  case cons xhd xtl ih =>
+    simp only [List.append, List.foldl_cons]
+    rw [ih]
+
+theorem mapUnion_append {α β} [LT α] [StrictLT α] [DecidableLT α] {f : β → Set α} {xs ys : List β} :
+  (∀ b, (f b).WellFormed) →
+  (xs ++ ys).mapUnion f = xs.mapUnion f ++ ys.mapUnion f
+:= by
+  intro hwf
+  induction xs
+  case nil =>
+    simp only [List.nil_append, mapUnion_empty]
+    change _ = Set.empty ∪ ys.mapUnion f
+    rw [Set.union_empty_left]
+    exact mapUnion_wf
+  case cons hd tl ih =>
+    simp only [List.cons_append]
+    rw [mapUnion_cons hwf, mapUnion_cons hwf, ih]
+    change _ ∪ (_ ∪ _) = (_ ∪ _) ∪ _
+    symm
+    apply Set.union_assoc
+
 private theorem foldl_union_swap_front {α} [LT α] [StrictLT α] [DecidableLT α] [DecidableEq α] (x₁ x₂ : Set α) {xs : List (Set α)} {a : Set α}:
   (x₁ :: x₂ :: xs).foldl (· ∪ ·) a = (x₂ :: x₁ :: xs).foldl (· ∪ ·) a
 := by

cedar-lean/Cedar/Thm/SymCC/Enforcer/Footprint.lean

@@ -15,6 +15,7 @@
 -/
 
 import Cedar.SymCC.Enforcer
+import Cedar.Thm.Data.LT
 import Cedar.Thm.Data.MapUnion
 import Cedar.Thm.SymCC.Env.SWF
 import Cedar.Thm.SymCC.Enforcer.Asserts
@@ -28,6 +29,29 @@ namespace Cedar.SymCC
 
 open Data Spec SymCC Factory
 
+def footprint_ofEntity_wf :
+  (footprint.ofEntity x εnv).WellFormed
+:= by
+  simp [footprint.ofEntity]
+  split
+  · split <;> simp [Set.singleton_wf, Set.empty_wf]
+  · exact Set.empty_wf
+
+def footprint_ofBranch_wf :
+  ft₂.WellFormed →
+  ft₃.WellFormed →
+  (footprint.ofBranch εnv x ft₁ ft₂ ft₃).WellFormed
+:= by
+  intro h₂ h₃
+  simp [footprint.ofBranch]
+  split <;> simp [h₂, h₃, Set.empty_wf, Set.union_wf]
+
+def footprint_wf (x : Expr) (εnv : SymEnv) :
+  (footprint x εnv).WellFormed
+:= by
+  cases x
+  all_goals simp [footprint, footprint_ofEntity_wf, footprint_ofBranch_wf, footprint_wf, Set.empty_wf, Set.mapUnion_wf, Set.union_wf]
+
 def SymEntities.SameOn (εs : SymEntities) (ft : Set Term) (I₁ I₂ : Interpretation) : Prop :=
   ∀ ety δ,
     εs.find? ety = some δ →
@@ -274,6 +298,24 @@ theorem mem_footprints_wf {xs : List Expr} {t : Term} {εnv : SymEnv}
   replace ⟨x, hinₓ, hin⟩ := hin
   exact mem_footprint_wf (And.intro hwε (hvr x hinₓ)) hin
 
+theorem footprints_empty {εnv : SymEnv} :
+  footprints [] εnv = ∅
+:= by
+  simp [footprints, Set.mapUnion_empty]
+
+theorem footprints_singleton {x : Expr} {εnv : SymEnv} :
+  footprints [x] εnv = footprint x εnv
+:= by
+  simp [SymCC.footprints, List.mapUnion, EmptyCollection.emptyCollection]
+  rw [Data.Set.union_empty_left (footprint_wf x εnv)]
+
+theorem footprints_append {xs₁ xs₂ : List Expr} {εnv : SymEnv} :
+  footprints (xs₁ ++ xs₂) εnv = footprints xs₁ εnv ++ footprints xs₂ εnv
+:= by
+  simp [footprints]
+  apply Data.Set.mapUnion_append
+  intro x ; apply footprint_wf
+
 theorem footprint_subset_footprints {x : Expr} {xs : List Expr} {εnv : SymEnv} :
   x ∈ xs → footprint x εnv ⊆ footprints xs εnv
 := by