Prove type checker soundness. (#171)

Co-authored-by: Emina Torlak <[email protected]>

cedar-lean/Cedar/Data/List.lean

@@ -64,22 +64,27 @@ inductive Sorted [LT α] : List α → Prop where
       Sorted (y :: ys) →
       Sorted (x :: y :: ys)
 
+
+theorem sizeOf_snd_lt_sizeOf_list {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} :
+  x ∈ xs → sizeOf x.snd < 1 + sizeOf xs
+:= by
+  intro h
+  rw [Nat.add_comm]
+  apply Nat.lt_add_right
+  apply @Nat.lt_trans (sizeOf x.snd) (sizeOf x) (sizeOf xs)
+  {
+    simp [Prod._sizeOf_inst, Prod._sizeOf_1]
+    rw [Nat.add_comm]
+    apply Nat.lt_add_of_pos_right
+    apply Nat.add_pos_left
+    apply Nat.one_pos
+  }
+  { apply List.sizeOf_lt_of_mem; exact h }
+
 def attach₂ {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] (xs : List (α × β)) :
 List { x : α × β // sizeOf x.snd < 1 + sizeOf xs } :=
   xs.pmap Subtype.mk
-  (λ x => by
-    intro h
-    rw [Nat.add_comm]
-    apply Nat.lt_add_right
-    apply @Nat.lt_trans (sizeOf x.snd) (sizeOf x) (sizeOf xs)
-    {
-      simp [Prod._sizeOf_inst, Prod._sizeOf_1]
-      rw [Nat.add_comm]
-      apply Nat.lt_add_of_pos_right
-      apply Nat.add_pos_left
-      apply Nat.one_pos
-    }
-    { apply List.sizeOf_lt_of_mem; exact h })
+  (λ x => by exact sizeOf_snd_lt_sizeOf_list)
 
 def mapM₁ {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u}
   (xs : List α) (f : {x : α // x ∈ xs} → m β) : m (List β) :=
@@ -466,4 +471,67 @@ theorem if_equiv_strictLT_then_canonical [LT α] [StrictLT α] [DecidableLT α]
   apply Equiv.symm
   exact h₁
 
+def Forallᵥ {α β γ} (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : Prop :=
+  List.Forall₂ (fun kv₁ kv₂ => kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) kvs₁ kvs₂
+
+theorem insertCanonical_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] {p : β → γ → Prop}
+  {kv₁ : α × β} {kv₂ : α × γ} {kvs₁ : List (α × β)} {kvs₂ : List (α × γ)}
+  (h₁ : kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd)
+  (h₂ : Forallᵥ p kvs₁ kvs₂) :
+  Forallᵥ p (insertCanonical Prod.fst kv₁ kvs₁) (insertCanonical Prod.fst kv₂ kvs₂)
+:= by
+  simp [Forallᵥ] at *
+  cases h₂
+  case nil =>
+    simp [insertCanonical_singleton]
+    apply Forall₂.cons (by exact h₁) (by simp only [Forall₂.nil])
+  case cons hd₁ hd₂ tl₁ tl₂ h₃ h₄ =>
+    simp [insertCanonical]
+    split <;> split
+    case inl.inl =>
+      apply Forall₂.cons (by exact h₁)
+      apply Forall₂.cons (by exact h₃) (by exact h₄)
+    case inl.inr h₅ h₆ =>
+      simp [h₁, h₃] at h₅
+      rcases (StrictLT.asymmetric kv₂.fst hd₂.fst h₅) with _
+      split <;> contradiction
+    case inr.inl h₅ h₆ =>
+      simp [h₁, h₃] at h₅ h₆
+      split
+      case inl => contradiction
+      case inr =>
+        apply Forall₂.cons (by exact h₃)
+        apply insertCanonical_preserves_forallᵥ h₁ h₄
+    case inr.inr h₅ h₆ =>
+      simp [h₁, h₃] at h₅ h₆
+      split
+      case inl => contradiction
+      case inr => apply Forall₂.cons (by exact h₁) (by exact h₄)
+
+theorem canonicalize_preserves_forallᵥ {α β γ} [LT α] [StrictLT α] [DecidableLT α] (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) :
+  List.Forallᵥ p kvs₁ kvs₂ →
+  List.Forallᵥ p (List.canonicalize Prod.fst kvs₁) (List.canonicalize Prod.fst kvs₂)
+:= by
+  simp [Forallᵥ]
+  intro h₁
+  cases h₁
+  case nil =>
+    simp [canonicalize_nil]
+  case cons hd₁ hd₂ tl₁ tl₂ h₂ h₃ =>
+    simp [canonicalize]
+    rcases (canonicalize_preserves_forallᵥ p tl₁ tl₂ h₃) with h₄
+    apply insertCanonical_preserves_forallᵥ h₂ h₄
+
+theorem any_of_mem {f : α → Bool} {x : α} {xs : List α}
+  (h₁ : x ∈ xs)
+  (h₂ : f x) :
+  any xs f = true
+:= by
+  cases xs <;> simp at h₁
+  case cons hd tl =>
+    simp [List.any_cons]
+    rcases h₁ with h₁ | h₁
+    case inl => subst h₁ ; simp [h₂]
+    case inr => apply Or.inr ; exists x
+
 end List

cedar-lean/Cedar/Data/Set.lean

@@ -115,7 +115,7 @@ instance decLt [LT α] [DecidableLT α] : (n m : Set α) -> Decidable (n < m)
   | .mk nelts, .mk melts => List.hasDecidableLt nelts melts
 
 instance : Membership α (Set α) where -- enables ∈ notation
-  mem v s := s.elts.Mem v
+  mem v s := v ∈ s.elts
 
 theorem contains_prop_bool_equiv [DecidableEq α] {v : α} {s : Set α} :
   s.contains v = true ↔ v ∈ s
@@ -134,6 +134,25 @@ theorem in_list_in_set {α : Type u} (v : α) (s : Set α) :
   intro h0
   apply h0
 
+theorem in_set_in_list {α : Type u} (v : α) (s : Set α) :
+  v ∈ s → v ∈ s.elts
+:= by
+  simp [elts, Membership.mem]
+
+
+theorem mem_cons_self {α : Type u} (hd : α) (tl : List α) :
+  hd ∈ Set.mk (hd :: tl)
+:= by
+  simp [Membership.mem, elts]
+  apply List.mem_cons_self hd tl
+
+theorem mem_cons_of_mem {α : Type u} (a : α) (hd : α) (tl : List α) :
+  a ∈ Set.mk tl → a ∈ Set.mk (hd :: tl)
+:= by
+  simp [Membership.mem, elts] ; intro h₁
+  apply List.mem_cons_of_mem hd h₁
+
+
 theorem in_set_means_list_non_empty {α : Type u} (v : α) (s : Set α) :
   v ∈ s.elts → ¬(s.elts = [])
 := by
@@ -155,6 +174,14 @@ theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α)
   intro h; unfold make; simp
   apply List.if_equiv_strictLT_then_canonical _ _ h
 
+theorem make_eqv [LT α] [DecidableLT α] [StrictLT α] {xs ys : List α} :
+  Set.make xs = Set.mk ys → xs ≡ ys
+:= by
+  simp [make] ; intro h₁
+  rcases (List.canonicalize_equiv xs) with h₂
+  subst h₁
+  exact h₂
+
 theorem make_mem [LT α] [DecidableLT α] [StrictLT α] (x : α) (xs : List α) :
   x ∈ xs ↔ x ∈ Set.make xs
 := by
@@ -166,6 +193,26 @@ theorem make_mem [LT α] [DecidableLT α] [StrictLT α] (x : α) (xs : List α)
   case mp => apply h₁ h₃
   case mpr => apply h₂ h₃
 
+theorem make_any_iff_any [LT α] [DecidableLT α] [StrictLT α] (f : α → Bool) (xs : List α) :
+  (Set.make xs).any f = xs.any f
+:= by
+  simp [make, any, elts]
+  rcases (List.canonicalize_equiv xs) with h₁
+  simp [List.Equiv, List.subset_def] at h₁
+  rcases h₁ with ⟨hl₁, hr₁⟩
+  cases h₃ : List.any xs f
+  case false =>
+    by_contra h₄
+    simp only [Bool.not_eq_false, List.any_eq_true] at h₄
+    rcases h₄ with ⟨x, h₄, h₅⟩
+    specialize hr₁ h₄
+    simp [List.any_of_mem hr₁ h₅] at h₃
+  case true =>
+    simp [List.any_eq_true] at *
+    rcases h₃ with ⟨x, h₃, h₄⟩
+    exists x ; simp [h₄]
+    apply hl₁ h₃
+
 end Set
 
 end Cedar.Data

cedar-lean/Cedar/Thm.lean

@@ -14,6 +14,6 @@
  limitations under the License.
 -/
 
-import Cedar.Thm.Basic
+import Cedar.Thm.Authorization
 import Cedar.Thm.Slicing
-import Cedar.Thm.Soundness
+import Cedar.Thm.Typechecking

cedar-lean/Cedar/Thm/Basic.lean → cedar-lean/Cedar/Thm/Authorization.lean

@@ -15,7 +15,7 @@
 -/
 
 import Cedar.Spec
-import Cedar.Thm.Lemmas.Authorizer
+import Cedar.Thm.Authorization.Authorizer
 
 /-! This file contains basic theorems about Cedar's authorizer. -/
 
@@ -101,4 +101,4 @@ theorem order_and_dup_independent (request : Request) (entities : Entities) (pol
   unfold isAuthorized
   simp [hf, hp]
 
-end Cedar.Thm
+end Cedar.Thm

cedar-lean/Cedar/Thm/Lemmas/Authorizer.lean → cedar-lean/Cedar/Thm/Authorization/Authorizer.lean

@@ -15,7 +15,7 @@
 -/
 
 import Cedar.Spec
-import Cedar.Thm.Lemmas.Evaluator
+import Cedar.Thm.Authorization.Evaluator
 
 /-!
 This file contains useful lemmas about the `Authorizer` functions.
@@ -168,4 +168,4 @@ theorem satisfied_implies_resource_scope {policy : Policy} {request : Request} {
     exact h₅
 
 
-end Cedar.Thm
+end Cedar.Thm

cedar-lean/Cedar/Thm/Lemmas/Evaluator.lean → cedar-lean/Cedar/Thm/Authorization/Evaluator.lean

@@ -15,7 +15,7 @@
 -/
 
 import Cedar.Spec
-import Cedar.Thm.Lemmas.Std
+import Cedar.Thm.Core.Std
 
 /-!
 This file contains useful lemmas about the `Evaluator` functions.
@@ -66,4 +66,4 @@ theorem and_true_implies_right_true {e₁ e₂ : Expr} {request : Request} {enti
         cases b <;> simp at h₁
         rfl
 
-end Cedar.Thm
+end Cedar.Thm