diff --git a/README.md b/README.md index dadbadffb..d3f7c8a31 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,7 @@ This repository contains the Dafny formalization of Cedar and infrastructure for ## Repository Structure +* [`cedar-lean`](./cedar-lean) contains the Lean formalization of, and proofs about, Cedar. * [`cedar-dafny`](./cedar-dafny) contains the Dafny formalization of, and proofs about, Cedar. * [`cedar-dafny-java-wrapper`](./cedar-dafny-java-wrapper) contains the Java interface for DRT. * [`cedar-drt`](./cedar-drt) contains code for fuzzing, property-based testing, and differential testing of Cedar. diff --git a/cedar-lean/.gitignore b/cedar-lean/.gitignore new file mode 100644 index 000000000..f1d686650 --- /dev/null +++ b/cedar-lean/.gitignore @@ -0,0 +1,7 @@ +.DS_Store +/build +/lake-packages/* +*.json +!lake-manifest.json +*.olean + diff --git a/cedar-lean/Cedar.lean b/cedar-lean/Cedar.lean new file mode 100644 index 000000000..f79829fb3 --- /dev/null +++ b/cedar-lean/Cedar.lean @@ -0,0 +1,20 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data +import Cedar.Spec +import Cedar.Thm +import Cedar.Validation \ No newline at end of file diff --git a/cedar-lean/Cedar/Data.lean b/cedar-lean/Cedar/Data.lean new file mode 100644 index 000000000..9ee23729e --- /dev/null +++ b/cedar-lean/Cedar/Data.lean @@ -0,0 +1,18 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data.Set +import Cedar.Data.Map diff --git a/cedar-lean/Cedar/Data/LT.lean b/cedar-lean/Cedar/Data/LT.lean new file mode 100644 index 000000000..902e91c90 --- /dev/null +++ b/cedar-lean/Cedar/Data/LT.lean @@ -0,0 +1,219 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Init.Classical +import Std + +/-! +This file contains utilities for working with strict and decidable LT relations. +-/ + +namespace Cedar.Data + +class StrictLT (α) [LT α] : Prop where + asymmetric : ∀ (a b : α), a < b → ¬ b < a + transitive : ∀ (a b c : α), a < b → b < c → a < c + connected : ∀ (a b : α), a ≠ b → (a < b ∨ b < a) + +theorem StrictLT.irreflexive [LT α] [StrictLT α] (x : α) : + ¬ x < x +:= by + by_contra h₁ + rcases (StrictLT.asymmetric x x h₁) with h₂ + contradiction + +theorem StrictLT.if_not_lt_gt_then_eq [LT α] [StrictLT α] (x y : α) : + ¬ x < y → ¬ y < x → x = y +:= by + intro h₁ h₂ + by_contra h₃ + rcases (StrictLT.connected x y h₃) with h₄ + simp [h₁, h₂] at h₄ + +abbrev DecidableLT (α) [LT α] := DecidableRel (α := α) (· < ·) + +end Cedar.Data + +----- Theorems and instances ----- + +open Cedar.Data + +theorem List.lt_cons_cases [LT α] {x y : α} {xs ys : List α} : + x :: xs < y :: ys → + (x < y ∨ (¬ x < y ∧ ¬ y < x ∧ xs < ys)) +:= by + intro h₁ + cases h₁ + case head _ h₁ => simp [h₁] + case tail _ h₁ h₂ h₃ => simp [h₁, h₂]; assumption + +theorem List.cons_lt_cons [LT α] [StrictLT α] (x : α) (xs ys : List α) : + xs < ys → x :: xs < x :: ys +:= by + intro h₁ + apply List.lt.tail (StrictLT.irreflexive x) (StrictLT.irreflexive x) h₁ + +theorem List.lt_irrefl [LT α] [StrictLT α] (xs : List α) : + ¬ xs < xs +:= by + induction xs + case nil => by_contra; contradiction + case cons _ _ hd tl ih => + by_contra h₁ + rcases (StrictLT.irreflexive hd) with h₂ + cases tl + case nil => + rcases (List.lt_cons_cases h₁) with h₃ + simp [h₂] at h₃ + contradiction + case cons _ _ hd' tl' => + rcases (List.lt_cons_cases h₁) with h₃ + simp [h₂] at h₃ + contradiction + +theorem List.lt_trans [LT α] [StrictLT α] {xs ys zs : List α} : + xs < ys → ys < zs → xs < zs +:= by + intro h₁ h₂ + cases h₁ + case nil => cases h₂ <;> apply List.lt.nil + case head _ _ xhd xtl yhd ytl h₃ => + cases h₂ + case head _ _ zhd ztl h₄ => + apply List.lt.head + apply StrictLT.transitive _ _ _ h₃ h₄ + case tail _ _ zhd ztl h₄ h₅ h₆ => + rcases (StrictLT.if_not_lt_gt_then_eq yhd zhd h₄ h₅) with h₇ + subst h₇ + apply List.lt.head + exact h₃ + case tail _ _ xhd xtl yhd ytl h₃ h₄ h₅ => + cases h₂ + case head _ _ zhd ztl h₆ => + rcases (StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄) with h₇ + subst h₇ + apply List.lt.head + exact h₆ + case tail _ _ zhd ztl h₆ h₇ h₈ => + rcases (StrictLT.if_not_lt_gt_then_eq xhd yhd h₃ h₄) with h₉ + subst h₉ + apply List.lt.tail h₆ h₇ + apply List.lt_trans h₅ h₈ + +theorem List.lt_asymm [LT α] [StrictLT α] {xs ys : List α} : + xs < ys → ¬ ys < xs +:= by + intro h₁ + cases xs + case nil => + by_contra h₂ + contradiction + case cons _ _ hd tl => + cases ys + case nil => contradiction + case cons _ _ hd' tl' => + by_contra h₂ + rcases (List.lt_trans h₁ h₂) with h₃ + rcases (List.lt_irrefl (hd :: tl)) with h₄ + contradiction + +theorem List.lt_conn [LT α] [StrictLT α] {xs ys : List α} : + xs ≠ ys → (xs < ys ∨ ys < xs) +:= by + intro h₁ + by_contra h₂ + simp [not_or] at h₂ + rcases h₂ with ⟨h₂, h₃⟩ + cases xs <;> cases ys + case intro.nil.nil => contradiction + case intro.nil.cons _ _ xhd xtl => + rcases (List.lt.nil xhd xtl) with h₄ + contradiction + case intro.cons.nil _ _ yhd ytl => + rcases (List.lt.nil yhd ytl) with h₄ + contradiction + case intro.cons.cons _ _ xhd xtl yhd ytl => + by_cases (xhd < yhd) + case pos h₄ => + rcases (List.lt.head xtl ytl h₄) with h₅ + contradiction + case neg h₄ => + by_cases (yhd < xhd) + case pos h₅ => + rcases (List.lt.head ytl xtl h₅) with h₆ + contradiction + case neg h₅ => + rcases (StrictLT.if_not_lt_gt_then_eq xhd yhd h₄ h₅) with h₆ + subst h₆ + simp at h₁ + rcases (List.lt_conn h₁) with h₆ + cases h₆ + case inl _ _ h₆ => + rcases (List.cons_lt_cons xhd xtl ytl h₆) with h₇ + contradiction + case inr _ _ h₆ => + rcases (List.cons_lt_cons xhd ytl xtl h₆) with h₇ + contradiction + +instance List.strictLT (α) [LT α] [StrictLT α] : StrictLT (List α) where + asymmetric _ _ := List.lt_asymm + transitive _ _ _ := List.lt_trans + connected _ _ := List.lt_conn + +instance Nat.strictLT : StrictLT Nat where + asymmetric a b := Nat.lt_asymm + transitive a b c := Nat.lt_trans + connected a b := by + intro h₁ + rcases (Nat.lt_trichotomy a b) with h₂ + simp [h₁] at h₂ + exact h₂ + +instance UInt32.strictLT : StrictLT UInt32 where + asymmetric a b := by apply Nat.strictLT.asymmetric + transitive a b c := by apply Nat.strictLT.transitive + connected a b := by + intro h₁ + apply Nat.strictLT.connected + by_contra h₂ + have h₃ : a.val = b.val := by apply Fin.eq_of_val_eq; exact h₂ + have h₄ : a = b := by apply congrArg mk h₃ + contradiction + +instance Char.strictLT : StrictLT Char where + asymmetric a b := by apply UInt32.strictLT.asymmetric + transitive a b c := by apply UInt32.strictLT.transitive + connected a b := by + intro h₁ + apply UInt32.strictLT.connected + by_contra h₂ + have h₄ : a = b := by apply Char.eq_of_val_eq h₂ + contradiction + +instance String.strictLT : StrictLT String where + asymmetric a b := by + simp [String.lt_iff] + have h : StrictLT (List Char) := by apply List.strictLT + apply h.asymmetric + transitive a b c := by + simp [String.lt_iff] + have h : StrictLT (List Char) := by apply List.strictLT + apply h.transitive + connected a b := by + simp [String.lt_iff, String.ext_iff] + have h : StrictLT (List Char) := by apply List.strictLT + apply h.connected + diff --git a/cedar-lean/Cedar/Data/List.lean b/cedar-lean/Cedar/Data/List.lean new file mode 100644 index 000000000..d6288b35b --- /dev/null +++ b/cedar-lean/Cedar/Data/List.lean @@ -0,0 +1,449 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data.LT +import Std.Data.List.Basic +import Std.Data.List.Lemmas + +/-! +This file contains utilities for working with lists that are canonical or +equivalent modulo ordering and duplicates. A canonical list is sorted and +duplicate-free according to a strict total order <. +-/ + +namespace List + +open Cedar.Data + +----- Definitions ----- + +def insertCanonical [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α := + match xs with + | [] => [x] + | hd :: tl => + let fh := f hd + let fx := f x + if fx < fh + then x :: xs + else if fx > fh + then hd :: insertCanonical f x tl + else x :: tl + +/-- +If the ordering relation < on β is strict, then `canonicalize` returns a +canonical representation of the input list, which is sorted and free of +duplicates. +-/ +def canonicalize [LT β] [DecidableLT β] (f : α → β) : List α → List α + | [] => [] + | hd :: tl => insertCanonical f hd (canonicalize f tl) + +def Equiv {α} (a b : List α) : Prop := + a ⊆ b ∧ b ⊆ a + +infix:50 " ≡ " => Equiv + +inductive Sorted [LT α] : List α → Prop where + | nil : Sorted [] + | cons_nil {x} : Sorted (x :: nil) + | cons_cons {x y ys} : + x < y → + Sorted (y :: ys) → + Sorted (x :: y :: ys) + +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 }) + +def mapM₁ {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} + (xs : List α) (f : {x : α // x ∈ xs} → m β) : m (List β) := + xs.attach.mapM f + +def mapM₂ {m : Type u → Type v} [Monad m] {γ : Type u} [SizeOf α] [SizeOf β] + (xs : List (α × β)) (f : {x : α × β // sizeOf x.snd < 1 + sizeOf xs} → m γ) : m (List γ) := + xs.attach₂.mapM f + +----- Theorems ----- + +theorem Equiv.refl {a : List α} : + a ≡ a +:= by unfold List.Equiv; simp + +theorem Equiv.symm {a b : List α} : + a ≡ b → b ≡ a +:= by unfold List.Equiv; simp; intro h₁ h₂; simp [h₁, h₂] + +theorem Equiv.trans {a b c : List α} : + a ≡ b → b ≡ c → a ≡ c +:= by + unfold List.Equiv + simp + intro h₁ h₂ h₃ h₄ + apply And.intro + case _ => apply List.Subset.trans h₁ h₃ + case _ => apply List.Subset.trans h₄ h₂ + +theorem cons_equiv_cons (x : α) (xs ys : List α) : + xs ≡ ys → x :: xs ≡ x :: ys +:= by + unfold List.Equiv + intro h₁ + rcases h₁ with ⟨h₁, h₂⟩ + apply And.intro + all_goals { + apply List.cons_subset_cons; assumption + } + +theorem dup_head_equiv (x : α) (xs : List α) : + x :: x :: xs ≡ x :: xs +:= by unfold List.Equiv; simp [List.subset_def] + +theorem swap_cons_cons_equiv (x₁ x₂ : α) (xs : List α) : + x₁ :: x₂ :: xs ≡ x₂ :: x₁ :: xs +:= by + unfold List.Equiv + simp [List.subset_def] + apply And.intro + all_goals { intro a h₁; simp [h₁] } + +theorem filterMap_equiv (f : α → Option β) (xs ys : List α) : + xs ≡ ys → xs.filterMap f ≡ ys.filterMap f +:= by + simp [List.Equiv, List.subset_def] + intros h₁ h₂ + apply And.intro <;> + intro b a h₃ h₄ <;> + apply Exists.intro a <;> + simp [h₄] + apply h₁ h₃ + apply h₂ h₃ + +theorem tail_of_sorted_is_sorted {x : α} {xs : List α} [LT α] : + Sorted (x :: xs) → Sorted xs +:= by + intro h₁; cases h₁ + case cons_nil => exact Sorted.nil + case cons_cons => assumption + +theorem if_strictly_sorted_then_head_lt_tail [LT α] [StrictLT α] (x : α) (xs : List α) : + Sorted (x :: xs) → ∀ y, y ∈ xs → x < y +:= by + intro h₁ y h₂ + induction xs generalizing y + case nil => contradiction + case cons _ _ hd tl ih => + cases h₂ + case head => cases h₁; assumption + case tail h₂ => + apply ih + case _ => + cases h₁ + case cons_cons h₃ h₄ => + cases h₄ + case _ => exact Sorted.cons_nil + case cons_cons _ _ hd' tl' h₅ h₆ => + apply Sorted.cons_cons _ h₅ + apply StrictLT.transitive x hd hd' h₃ h₆ + case _ => assumption + +theorem if_strictly_sorted_equiv_then_head_eq [LT α] [StrictLT α] (x y : α) (xs ys : List α) : + Sorted (x :: xs) → + Sorted (y :: ys) → + (x :: xs) ≡ (y :: ys) → + x = y +:= by + intro h₁ h₂ + unfold List.Equiv; intro h₃ + rcases h₃ with ⟨h₃, h₄⟩ + simp at h₃; simp at h₄ + rcases h₃ with ⟨h₃, _⟩ + rcases h₄ with ⟨h₄, _⟩ + cases h₃ <;> cases h₄ <;> try { assumption } + case intro _ h₅ => simp [h₅] + case intro h₅ h₆ => + rcases (if_strictly_sorted_then_head_lt_tail x xs h₁ y h₆) with hc₁ + rcases (if_strictly_sorted_then_head_lt_tail y ys h₂ x h₅) with hc₂ + rcases (StrictLT.asymmetric x y hc₁) with hc₃ + contradiction + +theorem if_strictly_sorted_equiv_then_tail_subset [LT α] [StrictLT α] (x : α) (xs ys : List α) : + Sorted (x :: xs) → + Sorted (x :: ys) → + (x :: xs) ⊆ (x :: ys) → + xs ⊆ ys +:= by + intro h₁ h₂ h₃ + simp at h₃ + simp [List.subset_def] + intro y h₄ + simp [List.subset_def] at h₃ + specialize h₃ h₄ + cases h₃ + case inr => assumption + case inl _ h₅ => + subst h₅ + rcases (if_strictly_sorted_then_head_lt_tail y xs h₁ y h₄) with h₆ + rcases (StrictLT.irreflexive y) with h₇ + contradiction + +theorem if_strictly_sorted_equiv_then_tail_equiv [LT α] [StrictLT α] (x : α) (xs ys : List α) : + Sorted (x :: xs) → + Sorted (x :: ys) → + (x :: xs) ≡ (x :: ys) → + xs ≡ ys +:= by + unfold List.Equiv + intro h₁ h₂ h₃ + rcases h₃ with ⟨h₃, h₄⟩ + apply And.intro + exact if_strictly_sorted_equiv_then_tail_subset x xs ys h₁ h₂ h₃ + exact if_strictly_sorted_equiv_then_tail_subset x ys xs h₂ h₁ h₄ + +theorem if_strictly_sorted_equiv_then_eq [LT α] [StrictLT α] (xs ys : List α) : + Sorted xs → Sorted ys → xs ≡ ys → xs = ys +:= by + intro h₁ h₂ h₃ + induction xs generalizing ys + case nil => + apply Eq.symm + rw [←List.subset_nil] + unfold List.Equiv at h₃ + exact h₃.right + case cons xhd xtl ih => + cases ys + case nil => + unfold List.Equiv at h₃ + rw [←List.subset_nil] + exact h₃.left + case cons yhd ytl => + simp + have h₅ : xhd = yhd := if_strictly_sorted_equiv_then_head_eq xhd yhd xtl ytl h₁ h₂ h₃ + simp [h₅] + subst h₅ + apply ih + exact (tail_of_sorted_is_sorted h₁) + exact (tail_of_sorted_is_sorted h₂) + exact (if_strictly_sorted_equiv_then_tail_equiv xhd xtl ytl h₁ h₂ h₃) + +theorem insertCanonical_singleton [LT β] [DecidableLT β] (f : α → β) (x : α) : + insertCanonical f x [] = [x] +:= by unfold insertCanonical; rfl + +theorem insertCanonical_not_nil [DecidableEq β] [LT β] [DecidableRel (α := β) (· < ·)] (f : α → β) (x : α) (xs : List α) : + insertCanonical f x xs ≠ [] +:= by + unfold insertCanonical + cases xs with + | nil => simp + | cons hd tl => + simp + by_cases h₁ : (f x) < (f hd) <;> simp [h₁] + by_cases h₂ : (f x) > (f hd) <;> simp [h₂] + +theorem insertCanonical_cases [LT α] [DecidableLT α] (x y : α) (ys : List α) : + (x < y ∧ insertCanonical id x (y :: ys) = x :: y :: ys) ∨ + (¬ x < y ∧ x > y ∧ insertCanonical id x (y :: ys) = y :: insertCanonical id x ys) ∨ + (¬ x < y ∧ ¬ x > y ∧ insertCanonical id x (y :: ys) = x :: ys) +:= by + generalize h₁ : insertCanonical id x ys = xys + unfold insertCanonical; simp + by_cases (x < y) + case pos _ _ h₂ => simp [h₂] + case neg _ _ h₂ => + simp [h₂] + by_cases (x > y) + case pos _ _ h₃ => simp [h₃, h₁] + case neg _ _ h₃ => simp [h₃] + +theorem insertCanonical_sorted [LT α] [StrictLT α] [DecidableLT α] (x : α) (xs : List α) : + Sorted xs → Sorted (insertCanonical id x xs) +:= by + intro h₁ + unfold insertCanonical + induction xs <;> simp + case nil => exact Sorted.cons_nil + case cons _ _ hd tl ih => + specialize ih (tail_of_sorted_is_sorted h₁) + split + case inl _ _ h₂ => exact Sorted.cons_cons h₂ h₁ + case inr _ _ h₂ => + by_cases (x > hd) + case neg _ _ h₃ => + simp [h₃] + unfold GT.gt at h₃ + rcases (StrictLT.if_not_lt_gt_then_eq x hd h₂ h₃) with h₄ + subst h₄ + exact h₁ + case pos _ _ h₃ => + simp [h₃] + cases tl + case nil => + rcases (insertCanonical_singleton id x) with h₄ + simp [h₄] + apply Sorted.cons_cons (by apply h₃) Sorted.cons_nil + case cons _ _ hd' tl' => + simp at ih + rcases (insertCanonical_cases x hd' tl') with h₄ + cases h₄ + case inl _ _ _ h₄ => + rcases h₄ with ⟨h₄, h₅⟩ + simp [h₅] + apply Sorted.cons_cons (by apply h₃) + apply Sorted.cons_cons h₄ (tail_of_sorted_is_sorted h₁) + case inr _ _ _ h₄ => + cases h₄ + case inl _ _ _ h₄ => + rcases h₄ with ⟨h₄, h₅, h₆⟩ + simp [h₆] + simp [h₄, h₅] at ih + apply Sorted.cons_cons _ ih + apply if_strictly_sorted_then_head_lt_tail hd (hd' :: tl') h₁ + simp only [find?, mem_cons, true_or] + case inr _ _ _ h₄ => + rcases h₄ with ⟨h₄, h₅, h₆⟩ + simp [h₆] + unfold GT.gt at h₅ + rcases (StrictLT.if_not_lt_gt_then_eq x hd' h₄ h₅) with h₇ + subst h₇ + exact h₁ + +theorem insertCanonical_equiv [LT α] [StrictLT α] [DecidableLT α] (x : α) (xs : List α) : + x :: xs ≡ insertCanonical id x xs +:= by + unfold insertCanonical + induction xs + case nil => simp; exact Equiv.refl + case cons _ _ hd tl ih => + simp + split + case inl => exact Equiv.refl + case inr _ _ h₁ => + split + case inr _ _ h₂ => + rcases (StrictLT.if_not_lt_gt_then_eq x hd h₁ h₂) with h₃ + subst h₃ + exact dup_head_equiv x tl + case inl _ _ h₂ => + cases tl + case nil => + rcases (insertCanonical_singleton id x) with h₃ + simp [h₃] + apply swap_cons_cons_equiv + case cons _ _ _ hd' tl' => + simp at ih + rcases (insertCanonical_cases x hd' tl') with h₃ + cases h₃ + case inl _ _ _ h₃ => + simp [h₃] + unfold List.Equiv + simp only [cons_subset, mem_cons, true_or, or_true, true_and] + apply And.intro + all_goals { + simp [List.subset_def] + intro a h₄; simp [h₄] + } + case inr _ _ _ h₃ => + cases h₃ + case inr _ _ _ h₃ => + rcases h₃ with ⟨h₃, h₄, h₅⟩ + simp [h₅] + unfold GT.gt at h₄ + rcases (StrictLT.if_not_lt_gt_then_eq x hd' h₃ h₄) with h₆ + subst h₆ + unfold List.Equiv + simp only [cons_subset, mem_cons, true_or, or_true, Subset.refl, and_self, subset_cons] + case inl _ _ _ h₃ => + rcases h₃ with ⟨h₃, h₄, h₅⟩ + simp [h₅] + simp [h₃, h₄] at ih + rcases (swap_cons_cons_equiv x hd (hd' :: tl')) with h₆ + apply Equiv.trans h₆ + apply cons_equiv_cons + exact ih + +theorem canonicalize_nil [LT β] [DecidableLT β] (f : α → β) : + canonicalize f [] = [] +:= by unfold canonicalize; rfl + +theorem canonicalize_not_nil [DecidableEq β] [LT β] [DecidableLT β] (f : α → β) (xs : List α) : + xs ≠ [] ↔ (canonicalize f xs) ≠ [] +:= by + apply Iff.intro + case _ => + intro h0 + cases xs with + | nil => contradiction + | cons hd tl => + unfold canonicalize + apply insertCanonical_not_nil + case _ => + unfold canonicalize + intro h0 + cases xs <;> simp at h0; simp + +theorem canonicalize_equiv [LT α] [StrictLT α] [DecidableLT α] (xs : List α) : + xs ≡ canonicalize id xs +:= by + induction xs + case nil => simp [canonicalize_nil, Equiv.refl] + case cons _ _ hd tl ih => + unfold canonicalize + generalize h₁ : canonicalize id tl = ys + simp [h₁] at ih + rcases (insertCanonical_equiv hd ys) with h₂ + apply Equiv.trans _ h₂ + apply cons_equiv_cons + exact ih + +theorem canonicalize_sorted [LT α] [StrictLT α] [DecidableLT α] (xs : List α) : + Sorted (canonicalize id xs) +:= by + induction xs + case nil => simp [canonicalize_nil, Sorted.nil] + case cons _ _ hd tl ih => + unfold canonicalize + apply insertCanonical_sorted + exact ih + +theorem if_equiv_strictLT_then_canonical [LT α] [StrictLT α] [DecidableLT α] (xs ys : List α) : + xs ≡ ys → (canonicalize id xs) = (canonicalize id ys) +:= by + intro h₁ + apply if_strictly_sorted_equiv_then_eq + exact (canonicalize_sorted xs) + exact (canonicalize_sorted ys) + rcases (Equiv.symm (canonicalize_equiv xs)) with h₂ + rcases (Equiv.symm (canonicalize_equiv ys)) with h₃ + apply Equiv.trans h₂ + apply Equiv.symm + apply Equiv.trans h₃ + apply Equiv.symm + exact h₁ + +end List \ No newline at end of file diff --git a/cedar-lean/Cedar/Data/Map.lean b/cedar-lean/Cedar/Data/Map.lean new file mode 100644 index 000000000..1fb915cd9 --- /dev/null +++ b/cedar-lean/Cedar/Data/Map.lean @@ -0,0 +1,114 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data.Set +/-! + +This file defines a simple map data types, backed by a sorted duplicate-free +list of key-value. Functions maps assume but don't require that their inputs are +well-formed (sorted and duplicate-free). Separate theorems show that these +functions produce well-formed outputs when given well-formed inputs. + +Use Map.make to construct well-formed maps from lists of key-value pairs. +-/ + +namespace Cedar.Data + +inductive Map (α : Type u) (β : Type v) where +| mk : List (α × β) -> Map α β +deriving Repr +deriving instance DecidableEq, Repr, Inhabited for Map + +namespace Map + +private def kvs {α : Type u} {β : Type v} : Map α β -> List (Prod α β) +| .mk kvs => kvs + + +open Except + +----- Definitions ----- + +-- produces an ordered and duplicate free list provided the given map is well formed +def toList {α : Type u} {β : Type v} (m : Map α β) : List (Prod α β) := m.kvs + +/- Creates a well-formed map from the given list of pairs. -/ +def make {α β} [LT α] [DecidableLT α] (kvs : List (α × β)) : Map α β := + Map.mk (kvs.canonicalize Prod.fst) + +/-- Empty map -/ +def empty {α β} : Map α β := .mk [] + +/-- Returns the keys of `m` as a set. -/ +def keys {α β} (m : Map α β) : Set α := + Set.mk (m.kvs.map Prod.fst) -- well-formed by construction + +def values {α β} (m : Map α β) : Set β := + Set.mk (m.kvs.map Prod.snd) + +/-- Returns true if `m` contains a mapping for the key `k`. -/ +def contains {α β} [BEq α] (m : Map α β) (k : α) : Bool := + (m.kvs.find? (fun ⟨k', _⟩ => k' == k)).isSome + +/-- Returns the binding for `k` in `m`, if any. -/ +def find? {α β} [BEq α] (m : Map α β) (k : α) : Option β := + match m.kvs.find? (fun ⟨k', _⟩ => k' == k) with + | some (_, v) => some v + | _ => none + +/-- Returns the binding for `k` in `m` or `err` if none is found. -/ +def findOrErr {α β ε} [BEq α] (m : Map α β) (k : α) (err: ε) : Except ε β := + match m.find? k with + | some v => ok v + | _ => error err + +/-- Filters `m` using `f`. -/ +def filter {α β} (f : α → β → Bool) (m : Map α β) : Map α β := + Map.mk (m.kvs.filter (fun ⟨k, v⟩ => f k v)) + +def size {α β} (m : Map α β) : Nat := + m.kvs.length + +def mapOnValues {α β γ} [LT α] [DecidableLT α] (f : β → γ) (m : Map α β) : Map α γ := + Map.make (m.kvs.map (λ (k,v) => (k, f v ))) + +def mapOnKeys {α β γ} [LT γ] [DecidableLT γ] (f : α → γ) (m : Map α β) : Map γ β := + Map.make (m.kvs.map (λ (k,v) => (f k, v) )) + +----- Props and Theorems ----- + +instance [LT (Prod α β)] : LT (Map α β) where +lt a b := a.kvs < b.kvs + +instance decLt [LT (Prod α β)] [DecidableRel (α:=(Prod α β)) (·<·)] : (n m : Map α β) -> Decidable (n < m) + | .mk nkvs, .mk mkvs => List.hasDecidableLt nkvs mkvs + +instance : Membership α (Map α β) where + mem a m := List.Mem a (m.kvs.map Prod.fst) + +theorem in_list_in_map {α : Type u} (k : α) (v : β) (m : Map α β) : + (k, v) ∈ m.kvs → k ∈ m +:= by + intro h0 + have h1 : k ∈ (List.map Prod.fst m.kvs) := by + simp + apply Exists.intro (k, v) + simp [h0] + apply h1 + +end Map + +end Cedar.Data \ No newline at end of file diff --git a/cedar-lean/Cedar/Data/Set.lean b/cedar-lean/Cedar/Data/Set.lean new file mode 100644 index 000000000..e81e35bce --- /dev/null +++ b/cedar-lean/Cedar/Data/Set.lean @@ -0,0 +1,160 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data.List +import Std.Data.List.Basic +import Std.Data.List.Lemmas +/-! +This file defines a simple set data type, backed by a sorted duplicate-free +list. Functions on sets assume but don't require their inputs to be well-formed +(sorted and duplicate-free). Separate theorems show that these functions produce +well-formed outputs when given well-formed inputs. + +Use Set.make to construct well-formed sets from lists. +-/ + +namespace Cedar.Data + +inductive Set (α : Type u) where +| mk (l : List α) +deriving Repr +deriving instance DecidableEq, Repr, Inhabited, Lean.ToJson for Set + +namespace Set + +private def elts {α : Type u} : (Set α) -> (List α) +| .mk elts => elts + +open Except + +----- Definitions ----- + +-- Creates an ordered/duplicate free list froma set provided the underlying set is well formed. +def toList {α : Type u} (s : Set α) : List α := s.elts + +/- Creates a well-formed set from the given list. -/ +def make [LT α] [DecidableLT α] (elts : List α) : Set α := + Set.mk (elts.canonicalize (·)) + +/-- Empty set ∅ -/ +def empty {α} : Set α := .mk [] + +/-- s == ∅ -/ +def isEmpty {α} [DecidableEq α] (s : Set α) : Bool := + s == empty + +/-- elt ∈ s -/ +def contains {α} [BEq α] (s : Set α) (elt : α) : Bool := + s.elts.elem elt -- can use binary search instead + +/-- s₁ ⊆ s₂ -/ +def subset {α} [BEq α] (s₁ s₂ : Set α) : Bool := + s₁.elts.all s₂.contains + +/-- s₁ ∩ s₂ ≠ ∅ -/ +def intersects {α} [BEq α] (s₁ s₂ : Set α) : Bool := + s₁.elts.any s₂.contains + +/-- s₁ ∩ s₂ -/ +def intersect {α} [BEq α] (s₁ s₂ : Set α) : Set α := + Set.mk (s₁.elts.filter s₂.contains) -- well-formed by construction + +/-- s₁ ∪ s₂ -/ +def union {α} [LT α] [DecidableLT α] (s₁ s₂ : Set α) : Set α := + make (s₁.elts ++ s₂.elts) -- enforce well-formedness + +/-- Filters `s` using `f`. -/ +def filter {α} (f : α → Bool) (s : Set α) : Set α := + Set.mk (s.elts.filter f) -- well-formed by construction + +/-- Maps `f` to `s`.-/ +def map {α β} [LT β] [DecidableLT β] (f : α → β) (s : Set α) : Set β := + make (s.elts.map f) -- enforce well-formedness + +/-- Maps `f` to `s` and returns the result of `err` if any error is encounterd. -/ +def mapOrErr {α β ε} [DecidableEq β] [LT β] [DecidableRel (α := β) (· < ·)] (f : α → Except ε β) (s : Set α) (err : ε) : Except ε (Set β) := + match s.elts.mapM f with + | .ok elts => ok (make elts) -- enforce well-formedness + | _ => error err -- return fixed error to be order-independent + +/-- Returns true if all elements of `s` satisfy `f`. -/ +def all {α} (f : α → Bool) (s : Set α) : Bool := + s.elts.all f + +/-- Returns true if some element of `s` satisfies `f`. -/ +def any {α} (f : α → Bool) (s : Set α) : Bool := + s.elts.any f + +def size {α} (s : Set α) : Nat := + s.elts.length + +def singleton {α} (a : α) : Set α := + Set.mk [a] + +def foldl {α β} (f : α → β → α) (init : α) (s : Set β) : α := + s.elts.foldl f init +----- Props and Theorems ----- + +instance [LT α] : LT (Set α) where +lt a b := a.elts < b.elts + +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 + +theorem contains_prop_bool_equiv [DecidableEq α] {v : α} {s : Set α} : + s.contains v = true ↔ v ∈ s +:= by + apply Iff.intro + intro h0 + apply List.mem_of_elem_eq_true + assumption + intro h0 + apply List.elem_eq_true_of_mem + assumption + +theorem in_list_in_set {α : Type u} (v : α) (s : Set α) : + v ∈ s.elts → v ∈ s +:= by + intro h0 + apply h0 + +theorem in_set_means_list_non_empty {α : Type u} (v : α) (s : Set α) : + v ∈ s.elts → ¬(s.elts = []) +:= by + intros h0 h1 + rw [List.eq_nil_iff_forall_not_mem] at h1 + specialize h1 v + contradiction + +theorem make_non_empty [DecidableEq α] [LT α] [DecidableLT α] (xs : List α) : + xs ≠ [] ↔ (Set.make xs).isEmpty = false +:= by + unfold isEmpty; unfold empty; unfold make + simp only [beq_eq_false_iff_ne, ne_eq, mk.injEq] + apply List.canonicalize_not_nil + +theorem make_eq_if_eqv [LT α] [DecidableLT α] [StrictLT α] (xs ys : List α) : + xs ≡ ys → Set.make xs = Set.make ys +:= by + intro h; unfold make; simp + apply List.if_equiv_strictLT_then_canonical _ _ h + +end Set + +end Cedar.Data \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec.lean b/cedar-lean/Cedar/Spec.lean new file mode 100644 index 000000000..d60873b34 --- /dev/null +++ b/cedar-lean/Cedar/Spec.lean @@ -0,0 +1,26 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Authorizer +import Cedar.Spec.Entities +import Cedar.Spec.Evaluator +import Cedar.Spec.Expr +import Cedar.Spec.Ext +import Cedar.Spec.Policy +import Cedar.Spec.Request +import Cedar.Spec.Response +import Cedar.Spec.Value +import Cedar.Spec.Wildcard \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Authorizer.lean b/cedar-lean/Cedar/Spec/Authorizer.lean new file mode 100644 index 000000000..f56118343 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Authorizer.lean @@ -0,0 +1,45 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Evaluator +import Cedar.Spec.Response + +/-! This file defines the Cedar authorizer. -/ + +namespace Cedar.Spec + +open Cedar.Data +open Effect + +def satisfied (policy : Policy) (req : Request) (entities : Entities) : Bool := + (evaluate policy.toExpr req entities) = .ok true + +def satisfiedWithEffect (effect : Effect) (policy : Policy) (req : Request) (entities : Entities) : Option PolicyID := + if policy.effect == effect && satisfied policy req entities + then some policy.id + else none + +def satisfiedPolicies (effect : Effect) (policies : Policies) (req : Request) (entities : Entities) : Set PolicyID := + Set.make (policies.filterMap (satisfiedWithEffect effect · req entities)) + +def isAuthorized (req : Request) (entities : Entities) (policies : Policies) : Response := + let forbids := satisfiedPolicies .forbid policies req entities + let permits := satisfiedPolicies .permit policies req entities + if forbids.isEmpty && !permits.isEmpty + then { decision := .allow, policies := permits } + else { decision := .deny, policies := forbids } + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Entities.lean b/cedar-lean/Cedar/Spec/Entities.lean new file mode 100644 index 000000000..3ef3da14d --- /dev/null +++ b/cedar-lean/Cedar/Spec/Entities.lean @@ -0,0 +1,60 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Value + +/-! +This file defines Cedar entities. +-/ + +namespace Cedar.Spec + +open Except +open Cedar.Data + +----- Definitions ----- + +structure EntityData where + attrs : Map Attr Value + ancestors : Set EntityUID + +abbrev Entities := Map EntityUID EntityData + +def Entities.ancestors (es : Entities) (uid : EntityUID) : Result (Set EntityUID) := do + let d ← es.findOrErr uid .entityDoesNotExist + ok d.ancestors + +def Entities.ancestorsOrEmpty (es : Entities) (uid : EntityUID) : Set EntityUID := + match es.find? uid with + | some d => d.ancestors + | none => Set.empty + +def Entities.attrs (es : Entities) (uid : EntityUID) : Result (Map Attr Value) := do + let d ← es.findOrErr uid .entityDoesNotExist + ok d.attrs + +def Entities.attrsOrEmpty (es : Entities) (uid : EntityUID) : Map Attr Value := + match es.find? uid with + | some d => d.attrs + | none => Map.empty + +----- Derivations ----- + +deriving instance Repr for EntityData +deriving instance DecidableEq for EntityData +deriving instance Inhabited for EntityData + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Evaluator.lean b/cedar-lean/Cedar/Spec/Evaluator.lean new file mode 100644 index 000000000..f989b0bff --- /dev/null +++ b/cedar-lean/Cedar/Spec/Evaluator.lean @@ -0,0 +1,117 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Entities +import Cedar.Spec.Expr +import Cedar.Spec.Request + +/-! This file defines the semantics of Cedar operators and expressions. -/ + +namespace Cedar.Spec + +open Cedar.Data +open Except +open Error + +def apply₁ : UnaryOp → Value → Result Value + | .not, .prim (.bool b) => ok !b + | .neg, .prim (.int i) => ok ((- i) : Int) + | .mulBy c, .prim (.int i) => ok (c * i) + | .like p, .prim (.string s) => ok (wildcardMatch s p) + | .is ety, .prim (.entityUID uid) => ok (ety == uid.ty) + | _, _ => error .typeError + +def inₑ (uid₁ uid₂ : EntityUID) (es : Entities) : Bool := + uid₁ == uid₂ || (es.ancestorsOrEmpty uid₁).contains uid₂ + +def inₛ (uid : EntityUID) (vs : Set Value) (es : Entities) : Result Value := do + let uids ← vs.mapOrErr Value.asEntityUID .typeError + ok (uids.any (inₑ uid · es)) + +def apply₂ (op₂ : BinaryOp) (v₁ v₂ : Value) (es : Entities) : Result Value := + match op₂, v₁, v₂ with + | .eq, _, _ => ok (v₁ == v₂) + | .less, .prim (.int i), .prim (.int j) => ok ((i < j): Bool) + | .lessEq, .prim (.int i), .prim (.int j) => ok ((i ≤ j): Bool) + | .add, .prim (.int i), .prim (.int j) => ok (i + j) + | .sub, .prim (.int i), .prim (.int j) => ok (i - j) + | .contains, .set vs₁, _ => ok (vs₁.contains v₂) + | .containsAll, .set vs₁, .set vs₂ => ok (vs₂.subset vs₁) + | .containsAny, .set vs₁, .set vs₂ => ok (vs₁.intersects vs₂) + | .mem, .prim (.entityUID uid₁), .prim (.entityUID uid₂) => ok (inₑ uid₁ uid₂ es) + | .mem, .prim (.entityUID uid₁), .set (vs) => inₛ uid₁ vs es + | _, _, _ => error .typeError + +def attrsOf (v : Value) (lookup : EntityUID → Result (Map Attr Value)) : Result (Map Attr Value) := + match v with + | .record r => ok r + | .prim (.entityUID uid) => lookup uid + | _ => error typeError + +def hasAttr (v : Value) (a : Attr) (es : Entities) : Result Value := do + let r ← attrsOf v (fun uid => ok (es.attrsOrEmpty uid)) + ok (r.contains a) + +def getAttr (v : Value) (a : Attr) (es : Entities) : Result Value := do + let r ← attrsOf v es.attrs + r.findOrErr a attrDoesNotExist + +def bindAttr (a : Attr) (res : Result Value) : Result (Attr × Value) := do + let v ← res + ok (a, v) + +def evaluate (x : Expr) (req : Request) (es : Entities) : Result Value := + match x with + | .lit l => ok l + | .var var => + match var with + | .principal => ok req.principal + | .action => ok req.action + | .resource => ok req.resource + | .context => ok req.context + | .ite x₁ x₂ x₃ => do + let b ← (evaluate x₁ req es).as Bool + if b then evaluate x₂ req es else evaluate x₃ req es + | .and x₁ x₂ => do + let b ← (evaluate x₁ req es).as Bool + if !b then ok b else (evaluate x₂ req es).as Bool + | .or x₁ x₂ => do + let b ← (evaluate x₁ req es).as Bool + if b then ok b else (evaluate x₂ req es).as Bool + | .unaryApp op₁ x₁ => do + let v₁ ← evaluate x₁ req es + apply₁ op₁ v₁ + | .binaryApp op₂ x₁ x₂ => do + let v₁ ← evaluate x₁ req es + let v₂ ← evaluate x₂ req es + apply₂ op₂ v₁ v₂ es + | .hasAttr x₁ a => do + let v₁ ← evaluate x₁ req es + hasAttr v₁ a es + | .getAttr x₁ a => do + let v₁ ← evaluate x₁ req es + getAttr v₁ a es + | .set xs => do + let vs ← xs.mapM₁ (fun ⟨x₁, _⟩ => evaluate x₁ req es) + ok (Set.make vs) + | .record axs => do + let avs ← axs.mapM₂ (fun ⟨(a₁, x₁), _⟩ => bindAttr a₁ (evaluate x₁ req es)) + ok (Map.make avs) + | .call xfn xs => do + let vs ← xs.mapM₁ (fun ⟨x₁, _⟩ => evaluate x₁ req es) + call xfn vs + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Expr.lean b/cedar-lean/Cedar/Spec/Expr.lean new file mode 100644 index 000000000..1e5f7e7fa --- /dev/null +++ b/cedar-lean/Cedar/Spec/Expr.lean @@ -0,0 +1,176 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.ExtFun +import Cedar.Spec.Wildcard + +/-! This file defines abstract syntax for Cedar expressions. -/ + +namespace Cedar.Spec + +----- Definitions ----- + +inductive Var where + | principal + | action + | resource + | context + +inductive UnaryOp where + | not + | neg + | mulBy (i : Int) + | like (p : Pattern) + | is (ety : EntityType) + +inductive BinaryOp where + | eq + | mem -- represents Cedar's in operator + | less + | lessEq + | add + | sub + | contains + | containsAll + | containsAny + +inductive Expr where + | lit (p : Prim) + | var (v : Var) + | ite (cond : Expr) (thenExpr : Expr) (elseExpr : Expr) + | and (a : Expr) (b : Expr) + | or (a : Expr) (b : Expr) + | unaryApp (op : UnaryOp) (expr : Expr) + | binaryApp (op : BinaryOp) (a : Expr) (b : Expr) + | getAttr (expr : Expr) (attr : Attr) + | hasAttr (expr : Expr) (attr : Attr) + | set (ls : List Expr) + | record (map : List (Prod Attr Expr)) + | call (xfn : ExtFun) (args : List Expr) + +----- Derivations ----- + +deriving instance Repr for Var +deriving instance Repr for UnaryOp +deriving instance Repr for BinaryOp +deriving instance Repr for Expr + +deriving instance Inhabited for Expr + +deriving instance DecidableEq for Var +deriving instance DecidableEq for UnaryOp +deriving instance DecidableEq for BinaryOp + +mutual + +-- We should be able to get rid of this manual deriviation eventually. +-- There is work in progress on making these mutual derivations automatic. + +def decExpr (a b : Expr) : Decidable (a = b) := by + cases a <;> cases b + case lit.lit pa pb => exact match decEq pa pb with + | isTrue h₁ => isTrue (by rw [h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case var.var va vb => exact match decEq va vb with + | isTrue h₁ => isTrue (by rw [h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case ite.ite c1 t1 e1 c2 t2 e2 => exact match decExpr c1 c2 with + | isTrue h₁ => match decExpr t1 t2 with + | isTrue h₂ => match decExpr e1 e2 with + | isTrue h₃ => isTrue (by rw [h₁, h₂, h₃]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case and.and a1 a2 b1 b2 => exact match decExpr a1 b1 with + | isTrue h₁ => match decExpr a2 b2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case or.or a1 a2 b1 b2 => exact match decExpr a1 b1 with + | isTrue h₁ => match decExpr a2 b2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case unaryApp.unaryApp op1 e1 op2 e2 => exact match decEq op1 op2 with + | isTrue h₁ => match decExpr e1 e2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case binaryApp.binaryApp op1 a1 b1 op2 a2 b2 => exact match decEq op1 op2 with + | isTrue h₁ => match decExpr a1 a2 with + | isTrue h₂ => match decExpr b1 b2 with + | isTrue h₃ => isTrue (by rw [h₁, h₂, h₃]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case getAttr.getAttr e1 a1 e2 a2 => exact match decExpr e1 e2 with + | isTrue h₁ => match decEq a1 a2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case hasAttr.hasAttr e1 a1 e2 a2 => exact match decExpr e1 e2 with + | isTrue h₁ => match decEq a1 a2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case set.set l1 l2 => exact match decExprList l1 l2 with + | isTrue h₁ => isTrue (by rw [h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case record.record r1 r2 => exact match decProdAttrExprList r1 r2 with + | isTrue h₁ => isTrue (by rw [h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case call.call n1 a1 n2 a2 => exact match decEq n1 n2 with + | isTrue h₁ => match decExprList a1 a2 with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + all_goals apply isFalse; intro h; injection h + +def decProdAttrExpr (a b : Prod Attr Expr) : Decidable (a = b) := + match a, b with + | (aa, ae), (ba,be) => match decEq aa ba with + | isTrue h₁ => match decExpr ae be with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decProdAttrExprList (as bs : List (Prod Attr Expr)) : Decidable (as = bs) := + match as, bs with + | [], [] => isTrue rfl + | _::_, [] => isFalse (by intro; contradiction) + | [], _::_ => isFalse (by intro; contradiction) + | a::as, b::bs => match decProdAttrExpr a b with + | isTrue h₁ => match decProdAttrExprList as bs with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decExprList (as bs : List Expr) : Decidable (as = bs) := + match as, bs with + | [], [] => isTrue rfl + | _::_, [] => isFalse (by intro; contradiction) + | [], _::_ => isFalse (by intro; contradiction) + | a::as, b::bs => + match decExpr a b with + | isTrue h₁ => match decExprList as bs with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) +end + +instance : DecidableEq Expr := decExpr + +end Cedar.Spec diff --git a/cedar-lean/Cedar/Spec/Ext.lean b/cedar-lean/Cedar/Spec/Ext.lean new file mode 100644 index 000000000..108249b7d --- /dev/null +++ b/cedar-lean/Cedar/Spec/Ext.lean @@ -0,0 +1,57 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Ext.Decimal +import Cedar.Spec.Ext.IPAddr + +/-! This file defines Cedar extension values. -/ + +namespace Cedar.Spec + +open Cedar.Spec.Ext + +----- Definitions ----- + +abbrev IPAddr := IPAddr.IPNet + +inductive Ext where + | decimal (d : Decimal) + | ipaddr (ip : IPAddr) + +def Ext.lt : Ext → Ext → Bool + | .decimal d₁, .decimal d₂ => d₁ < d₂ + | .ipaddr ip₁, .ipaddr ip₂ => ip₁ < ip₂ + | .decimal _, .ipaddr _ => true + | .ipaddr _, .decimal _ => false + +----- Derivations ----- + +deriving instance Repr for Ext +deriving instance DecidableEq for Ext + +instance : LT Ext where +lt := fun x y => Ext.lt x y + +instance Ext.decLt (x y : Ext) : Decidable (x < y) := +if h : Ext.lt x y then isTrue h else isFalse h + +instance : Coe Decimal Ext where + coe d := .decimal d + +instance : Coe IPAddr Ext where + coe a := .ipaddr a + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Ext/Decimal.lean b/cedar-lean/Cedar/Spec/Ext/Decimal.lean new file mode 100644 index 000000000..a29d6d7a5 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Ext/Decimal.lean @@ -0,0 +1,82 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +/-! This file defines Cedar decimal values and functions. -/ + +namespace Cedar.Spec.Ext + +/-- +A decimal number consists of an integer part and a fractional part. +The former is the integer number before the decimal point. +The latter is the decimal number minus its integer part. +For instance, 10.234 is a decimal number. Its integer part is 10 and its fractional part is 0.234 +We restrict the number of the digits after the decimal point to 4. +-/ + +def DECIMAL_DIGITS : Nat := 4 +def DECIMAL_MIN : Int := -9223372036854775808 +def DECIMAL_MAX : Int := 9223372036854775807 + +abbrev Decimal := { i : Int // DECIMAL_MIN ≤ i ∧ i ≤ DECIMAL_MAX } + +namespace Decimal + +----- Definitions ----- + +def decimal? (i : Int) : Option Decimal := + if h : DECIMAL_MIN ≤ i ∧ i ≤ DECIMAL_MAX + then .some (Subtype.mk i h) + else .none + +def parse (str : String) : Option Decimal := + match str.split (· = '.') with + | [left, right] => + let rlen := right.length + if 0 < rlen ∧ rlen ≤ DECIMAL_DIGITS + then + match String.toInt? left, String.toNat? right with + | .some l, .some r => + let l' := l * (Int.pow 10 DECIMAL_DIGITS) + let r' := r * (Int.pow 10 (DECIMAL_DIGITS - rlen)) + let i := if l ≥ 0 then l' + r' else l' - r' + decimal? i + | _, _ => .none + else .none + | _ => .none + +abbrev decimal := parse + +def lt (d₁ d₂ : Decimal) : Bool := d₁.1 < d₂.1 + +def le (d₁ d₂ : Decimal) : Bool := d₁.1 ≤ d₂.1 + +----- Derivations ----- + +instance : LT Decimal where + lt := fun d₁ d₂ => Decimal.lt d₁ d₂ + +instance : LE Decimal where + le := fun d₁ d₂ => Decimal.le d₁ d₂ + +instance decLt (d₁ d₂ : Decimal) : Decidable (d₁ < d₂) := +if h : Decimal.lt d₁ d₂ then isTrue h else isFalse h + +instance decLe (d₁ d₂ : Decimal) : Decidable (d₁ ≤ d₂) := +if h : Decimal.le d₁ d₂ then isTrue h else isFalse h + +end Decimal + +end Cedar.Spec.Ext \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Ext/IPAddr.lean b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean new file mode 100644 index 000000000..873c2bb18 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Ext/IPAddr.lean @@ -0,0 +1,270 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +/-! This file defines Cedar IpAddr values and functions. -/ + +namespace Cedar.Spec.Ext + +namespace IPAddr + +----- UInt128 ----- + +-- Type of 128-bit unsigned numbers: 0 <= n < 2^128. +abbrev UInt128 := Fin 0x100000000000000000000000000000000 + +def UInt128.ofNat (n : Nat) : UInt128 := Fin.ofNat n + +instance : Coe UInt128 Nat where + coe n := n.1 + +instance : Coe Nat UInt128 where + coe n := Fin.ofNat n + +instance : Coe UInt8 Nat where + coe n := n.toNat + +instance : Coe UInt16 Nat where + coe n := n.toNat + +instance : Coe UInt32 Nat where + coe n := n.toNat + +instance : Coe Nat UInt32 where + coe n := UInt32.ofNat n + +----- IPv4Addr and IPv6Addr ----- + +/-- +IPv4 address: a 32 bit number partitioned into 4 groups. a0 is most signifcant +and a3 is the least significant. In other words, the number represented is +a0++a1++a2++a3 +--/ +abbrev IPv4Addr := UInt32 + +def IPv4Addr.toUInt128 (ip4 : IPv4Addr) : UInt128 := UInt128.ofNat ip4.toNat + +def UInt128.toIPv4Addr (bits : UInt128) : IPv4Addr := UInt32.ofNat bits + +def IPv4Addr.mk (a₀ a₁ a₂ a₃ : UInt8) : IPv4Addr := + (a₀ : Nat) <<< 24 ||| + (a₁ : Nat) <<< 16 ||| + (a₂ : Nat) <<< 8 ||| + (a₃ : Nat) + +/-- +IPv6 address: a 128 bit number partitioned into 8 groups. a0 is most signifcant +and a7 is the least significant. In other words, the number represented is +a0++a1++a2++a3++a4++a5++a6++a7 +--/ +abbrev IPv6Addr := UInt128 + +def IPv6Addr.toUInt128 (ip6 : IPv6Addr) : UInt128 := ip6 + +def UInt128.toIPv6Addr (bits : UInt128) : IPv6Addr := bits + +def IPv6Addr.mk (a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : UInt16) : IPv6Addr := + (a₀ : Nat) <<< 112 ||| + (a₁ : Nat) <<< 96 ||| + (a₂ : Nat) <<< 80 ||| + (a₃ : Nat) <<< 64 ||| + (a₄ : Nat) <<< 48 ||| + (a₅ : Nat) <<< 32 ||| + (a₆ : Nat) <<< 16 ||| + (a₇ : Nat) + +----- IPNet ----- + +def V4_SIZE := 32 +abbrev Prefix4 := Fin (V4_SIZE + 1) + +def V6_SIZE := 128 +abbrev Prefix6 := Fin (V6_SIZE + 1) + +inductive IPNet where + | V4 (v4 : IPv4Addr) (prefix4 : Prefix4) + | V6 (v6 : IPv6Addr) (prefix6 : Prefix6) + +def IPNet.isV4 : IPNet → Bool + | .V4 _ _ => true + | _ => false + +def IPNet.isV6 : IPNet → Bool + | .V6 _ _ => true + | _ => false + +def IPNet.toUInt128 : IPNet → UInt128 + | .V4 v4 _ => v4.toUInt128 + | .V6 v6 _ => v6.toUInt128 + +def IPNet.subnetWidth : IPNet → UInt128 + | .V4 _ p4 => V4_SIZE - p4 + | .V6 _ p6 => V6_SIZE - p6 + +def IPNet.applySubnetMask (ip : IPNet) : UInt128 := + let width := ip.subnetWidth + (ip.toUInt128 >>> width) <<< width + +def IPNet.range (ip : IPNet) : UInt128 × UInt128 := + let lo := ip.applySubnetMask + let hi := lo + (1 <<< ip.subnetWidth) - 1 + (lo, hi) + +def IPNet.inRange : IPNet → IPNet → Bool + | .V4 _ _, .V6 _ _ => false + | .V6 _ _, .V4 _ _ => false + | ip₁ , ip₂ => + let r₁ := ip₁.range + let r₂ := ip₂.range + r₂.2 ≥ r₁.2 && r₁.1 ≥ r₂.1 + +def LOOP_BACK_ADDRESS_V4 := IPv4Addr.mk 127 0 0 0 +def LOOP_BACK_ADDRESS_V6 := IPv6Addr.mk 0 0 0 0 0 0 0 1 +def LOOP_BACK_NET_V4 := IPNet.V4 LOOP_BACK_ADDRESS_V4 8 +def LOOP_BACK_NET_V6 := IPNet.V6 LOOP_BACK_ADDRESS_V6 128 + +def MULTICAST_ADDRESS_V4 := IPv4Addr.mk 224 0 0 0 +def MULTICAST_ADDRESS_V6 := IPv6Addr.mk 65280 0 0 0 0 0 0 0 +def MULTICAST_NET_V4 := IPNet.V4 MULTICAST_ADDRESS_V4 4 +def MULTICAST_NET_V6 := IPNet.V6 MULTICAST_ADDRESS_V6 8 + +def IPNet.isLoopback (ip : IPNet) : Bool := + ip.inRange (if ip.isV4 then LOOP_BACK_NET_V4 else LOOP_BACK_NET_V6) + +def IPNet.isMulticast (ip : IPNet) : Bool := + ip.inRange (if ip.isV4 then MULTICAST_NET_V4 else MULTICAST_NET_V6) + +def parseCIDR (str : String) (digits : Nat) (size : Nat) : Option (Fin (size + 1)) := + let len := str.length + if 0 < len && len ≤ digits + then do + let n ← str.toNat? + if n ≤ size then .some (Fin.ofNat n) else .none + else .none + +def parseCIDRV4 (str : String) : Option Prefix4 := parseCIDR str 2 V4_SIZE + +def parseCIDRV6 (str : String) : Option Prefix6 := parseCIDR str 3 V6_SIZE + +def parseNumV4 (str : String) : Option UInt8 := + let len := str.length + if 0 < len && len ≤ 3 && (str.startsWith "0" → str = "0") + then do + let n ← str.toNat? + if n ≤ 0xff then .some (UInt8.ofNat n) else .none + else .none + +def parseSegsV4 (str : String) : Option IPv4Addr := + match str.split (· = '.') with + | [s₀, s₁, s₂, s₃] => do + let a₀ ← parseNumV4 s₀ + let a₁ ← parseNumV4 s₁ + let a₂ ← parseNumV4 s₂ + let a₃ ← parseNumV4 s₃ + .some (IPv4Addr.mk a₀ a₁ a₂ a₃) + | _ => .none + +def parseIPv4Net (str : String) : Option IPNet := + match str.split (· = '/') with + | strV4 :: rest => do + let pre ← + match rest with + | [] => .some (Fin.ofNat V4_SIZE) + | [strPre] => parseCIDRV4 strPre + | _ => .none + let v4 ← parseSegsV4 strV4 + .some (IPNet.V4 v4 pre) + | _ => .none + +private def isHexDigit (c : Char) : Bool := + c.isDigit || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F') + +private def toHexNat (c : Char) : Nat := + if c.isDigit + then c.toNat - '0'.toNat + else if 'a' ≤ c && c ≤ 'f' + then c.toNat - 'a'.toNat + 10 + else if 'A' ≤ c && c ≤ 'F' + then c.toNat - 'A'.toNat + 10 + else c.toNat + +def parseNumV6 (str : String) : Option UInt16 := + let len := str.length + if 0 < len && len ≤ 4 && str.all isHexDigit + then + let n := str.foldl (fun n c => n * 16 + toHexNat c) 0 + if n ≤ 0xffff then .some (UInt16.ofNat n) else .none + else .none + +def parseNumSegsV6 (str : String) : Option (List UInt16) := + if str.isEmpty + then .some [] + else (str.split (· = ':')).mapM parseNumV6 + +def parseSegsV6 (str : String) : Option IPv6Addr := do + let segs ← + match str.splitOn "::" with + | [s₁] => parseNumSegsV6 s₁ + | [s₁, s₂] => do + let ns₁ ← parseNumSegsV6 s₁ + let ns₂ ← parseNumSegsV6 s₂ + let len := ns₁.length + ns₂.length + if len < 8 + then .some (ns₁ ++ (List.replicate (8 - len) 0) ++ ns₂) + else .none + | _ => .none + match segs with + | [a₀, a₁, a₂, a₃, a₄, a₅, a₆, a₇] => + .some (IPv6Addr.mk a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇) + | _ => .none + +def parseIPv6Net (str : String) : Option IPNet := + match str.split (· = '/') with + | strV6 :: rest => do + let pre ← + match rest with + | [] => .some (Fin.ofNat V6_SIZE) + | [strPre] => parseCIDRV6 strPre + | _ => .none + let v6 ← parseSegsV6 strV6 + .some (IPNet.V6 v6 pre) + | _ => .none + +def parse (str : String) : Option IPNet := + let ip := parseIPv4Net str + if ip.isSome then ip else parseIPv6Net str + +def ip (str : String) : Option IPNet := parse str + +def IPNet.lt : IPNet → IPNet → Bool + | .V4 _ _, .V6 _ _ => true + | .V6 _ _, .V4 _ _ => false + | .V4 v₁ p₁, .V4 v₂ p₂ => v₁ < v₂ || (v₁ = v₂ && p₁ < p₂) + | .V6 v₁ p₁, .V6 v₂ p₂ => v₁ < v₂ || (v₁ = v₂ && p₁ < p₂) + +----- IPNet deriviations ----- + +deriving instance Repr for IPNet +deriving instance DecidableEq for IPNet + +instance : LT IPNet where + lt := fun d₁ d₂ => IPNet.lt d₁ d₂ + +instance IPNet.decLt (d₁ d₂ : IPNet) : Decidable (d₁ < d₂) := +if h : IPNet.lt d₁ d₂ then isTrue h else isFalse h + +end IPAddr + +end Cedar.Spec.Ext diff --git a/cedar-lean/Cedar/Spec/ExtFun.lean b/cedar-lean/Cedar/Spec/ExtFun.lean new file mode 100644 index 000000000..2ecef1a08 --- /dev/null +++ b/cedar-lean/Cedar/Spec/ExtFun.lean @@ -0,0 +1,70 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Value + +/-! This file defines Cedar extension functions. -/ + +namespace Cedar.Spec + +open Cedar.Spec.Ext +open Option +open Except + +----- Definitions ----- + +inductive ExtFun where + | decimal ----- Decimal functions ----- + | lessThan + | lessThanOrEqual + | greaterThan + | greaterThanOrEqual + | ip ----- IpAddr functions ----- + | isIpv4 + | isIpv6 + | isLoopback + | isMulticast + | isInRange + +private def res {α} [Coe α Ext] : Option α → Result Value + | some v => ok v + | none => error .extensionError + +def call : ExtFun → List Value → Result Value + | .decimal, [.prim (.string s)] => res (Decimal.decimal s) + | .lessThan, + [.ext (.decimal d₁), .ext (.decimal d₂)] => ok (d₁ < d₂ : Bool) + | .lessThanOrEqual, + [.ext (.decimal d₁), .ext (.decimal d₂)] => ok (d₁ ≤ d₂ : Bool) + | .greaterThan, + [.ext (.decimal d₁), .ext (.decimal d₂)] => ok (d₁ > d₂ : Bool) + | .greaterThanOrEqual, + [.ext (.decimal d₁), .ext (.decimal d₂)] => ok (d₁ ≥ d₂ : Bool) + | .ip, [.prim (.string s)] => res (IPAddr.ip s) + | .isIpv4, [.ext (.ipaddr a)] => ok a.isV4 + | .isIpv6, [.ext (.ipaddr a)] => ok a.isV6 + | .isLoopback, [.ext (.ipaddr a)] => ok a.isLoopback + | .isMulticast, [.ext (.ipaddr a)] => ok a.isMulticast + | .isInRange, + [.ext (.ipaddr a₁), .ext (.ipaddr a₂)] => ok (a₁.inRange a₂) + | _, _ => error .typeError + +----- Derivations ----- + +deriving instance Repr for ExtFun +deriving instance DecidableEq for ExtFun + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Policy.lean b/cedar-lean/Cedar/Spec/Policy.lean new file mode 100644 index 000000000..b2ecd0f44 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Policy.lean @@ -0,0 +1,142 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Expr + +/-! This file defines abstract syntax for Cedar policies. -/ + +namespace Cedar.Spec + +----- Definitions ----- + +inductive Effect where + | permit + | forbid + +inductive Scope where + | any + | eq (entity : EntityUID) + | mem (entity : EntityUID) + | is (ety : EntityType) + | isMem (ety : EntityType) (entity : EntityUID) + +inductive PrincipalScope where + | principalScope (scope : Scope) + +inductive ResourceScope where + | resourceScope (scope : Scope) + +/-- +This definition of the ActionScope is more liberal than what is allowed by +Cedar's concrete grammar. In particular, the concrete grammar doesn't allow `is` +constraints in action scopes (e.g., `action is ety`), while our abstract grammar +does. Restricting action scopes in this way is not necessary for proving any +properties of Cedar; it is done in the concrete grammar for usability (since +`is` constraints on actions can be expressed using groups instead). We're +choosing the more liberal modeling here for uniformity and simplicity. +-/ +inductive ActionScope where + | actionScope (scope : Scope) + | actionInAny (ls : List EntityUID) + +abbrev PolicyID := String + +structure Policy where + id : PolicyID + effect : Effect + principalScope : PrincipalScope + actionScope : ActionScope + resourceScope : ResourceScope + condition : Expr + +abbrev Policies := List Policy + +def PrincipalScope.scope : PrincipalScope → Scope + | .principalScope s => s + +def ResourceScope.scope : ResourceScope → Scope + | .resourceScope s => s + +def Var.eqEntityUID (v : Var) (uid : EntityUID) : Expr := + .binaryApp .eq (.var v) (.lit (.entityUID uid)) + +def Var.inEntityUID (v : Var) (uid : EntityUID) : Expr := + .binaryApp .mem (.var v) (.lit (.entityUID uid)) + +def Var.isEntityType (v : Var) (ety : EntityType) : Expr := + .unaryApp (.is ety) (.var v) + +def Scope.toExpr (s : Scope) (v : Var) : Expr := + match s with + | .any => .lit (.bool true) + | .eq uid => v.eqEntityUID uid + | .mem uid => v.inEntityUID uid + | .is ety => v.isEntityType ety + | .isMem ety uid => .and (v.isEntityType ety) (v.inEntityUID uid) + +def PrincipalScope.toExpr : PrincipalScope → Expr + | .principalScope s => s.toExpr .principal + +def ResourceScope.toExpr : ResourceScope → Expr + | .resourceScope s => s.toExpr .resource + +def ActionScope.toExpr : ActionScope → Expr + | .actionScope s => s.toExpr .action + | .actionInAny es => + let exprs := es.map (fun e => .lit (.entityUID e)) + .binaryApp (.mem) (.var .action) (.set exprs) + +def Policy.toExpr (p : Policy) : Expr := + .and + p.principalScope.toExpr + (.and + p.actionScope.toExpr + (.and + p.resourceScope.toExpr + p.condition)) + +def Scope.bound : Scope → Option EntityUID + | .eq uid => .some uid + | .mem uid => .some uid + | .isMem _ uid => .some uid + | _ => .none + +----- Derivations ----- + +deriving instance Repr for Effect +deriving instance Repr for Scope +deriving instance Repr for PrincipalScope +deriving instance Repr for ResourceScope +deriving instance Repr for ActionScope +deriving instance Repr for Policy + +deriving instance DecidableEq for Effect +deriving instance DecidableEq for Scope +deriving instance DecidableEq for PrincipalScope +deriving instance DecidableEq for ResourceScope +deriving instance DecidableEq for ActionScope +deriving instance DecidableEq for Policy + +deriving instance Inhabited for Effect +deriving instance Inhabited for Scope +deriving instance Inhabited for PrincipalScope +deriving instance Inhabited for ResourceScope +deriving instance Inhabited for ActionScope +deriving instance Inhabited for Policy + +deriving instance Lean.ToJson for PolicyID + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Request.lean b/cedar-lean/Cedar/Spec/Request.lean new file mode 100644 index 000000000..06af6cb8a --- /dev/null +++ b/cedar-lean/Cedar/Spec/Request.lean @@ -0,0 +1,38 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Value + +/-! +This file defines Cedar requests. +-/ + +namespace Cedar.Spec + +open Except +open Cedar.Data + +structure Request where + principal : EntityUID + action : EntityUID + resource : EntityUID + context : Map Attr Value + +deriving instance Repr for Request +deriving instance DecidableEq for Request +deriving instance Inhabited for Request + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Response.lean b/cedar-lean/Cedar/Spec/Response.lean new file mode 100644 index 000000000..1e38495e9 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Response.lean @@ -0,0 +1,47 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Policy +import Lean.Data.Json.FromToJson +/-! +This file defines Cedar responses. +-/ + +namespace Cedar.Spec + +open Cedar.Data + +----- Definitions ----- + +inductive Decision where + | allow + | deny + +structure Response where + decision : Decision + policies : Set PolicyID + +----- Derivations ----- + +deriving instance Repr for Decision, Response + +deriving instance DecidableEq for Decision +deriving instance DecidableEq for Response + +deriving instance Lean.ToJson for Decision +deriving instance Lean.ToJson for Response + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Value.lean b/cedar-lean/Cedar/Spec/Value.lean new file mode 100644 index 000000000..87bc5d3be --- /dev/null +++ b/cedar-lean/Cedar/Spec/Value.lean @@ -0,0 +1,326 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Data +import Cedar.Spec.Ext + +/-! This file defines Cedar values and results. -/ + +namespace Cedar.Spec + +open Cedar.Data +open Cedar.Spec.Ext +open Except + +----- Definitions ----- + +inductive Error where + | entityDoesNotExist + | attrDoesNotExist + | typeError + | extensionError + +abbrev Result (α) := Except Error α + +abbrev Id := String + +structure Name where + id : Id + path : List Id + +abbrev EntityType := Name + +structure EntityUID where + ty : EntityType + eid : String + +inductive Prim where + | bool (b : Bool) + | int (i : Int) + | string (s : String) + | entityUID (uid : EntityUID) + +abbrev Attr := String + +inductive Value where + | prim (p : Prim) + | set (s : Set Value) + | record (m : Map Attr Value) + | ext (x : Ext) + +----- Coercions ----- + +def Value.asEntityUID : Value → Result EntityUID + | .prim (.entityUID uid) => ok uid + | _ => error Error.typeError + +def Value.asSet : Value → Result (Data.Set Value) + | .set s => ok s + | _ => error Error.typeError + +def Value.asBool : Value → Result Bool + | .prim (.bool b) => ok b + | _ => error Error.typeError + +def Value.asString : Value → Result String + | .prim (.string s) => ok s + | _ => error Error.typeError + +def Value.asInt : Value → Result Int + | .prim (.int i) => ok i + | _ => error Error.typeError + +def Result.as {α} (β) [Coe α (Result β)] : Result α → Result β + | ok v => v + | error e => error e + +instance : Coe Bool Value where + coe b := .prim (.bool b) + +instance : Coe Int Value where + coe i := .prim (.int i) + +instance : Coe String Value where + coe s := .prim (.string s) + +instance : Coe EntityUID Value where + coe e := .prim (.entityUID e) + +instance : Coe Prim Value where + coe p := .prim p + +instance : Coe Ext Value where + coe x := .ext x + +instance : Coe (Data.Set Value) Value where + coe s := .set s + +instance : Coe (Map Attr Value) Value where + coe r := .record r + +instance : Coe Value (Result Bool) where + coe v := v.asBool + +instance : Coe Value (Result Int) where + coe v := v.asInt + +instance : Coe Value (Result String) where + coe v := v.asString + +instance : Coe Value (Result EntityUID) where + coe v := v.asEntityUID + +instance : Coe Value (Result (Data.Set Value)) where + coe v := v.asSet + +----- Derivations ----- + +deriving instance Repr for Except +deriving instance Repr for Error +deriving instance Repr for Name +deriving instance Repr for EntityType +deriving instance Repr for EntityUID +deriving instance Repr for Prim +deriving instance Repr for Value + +deriving instance DecidableEq for Except +deriving instance DecidableEq for Error +deriving instance DecidableEq for Name +deriving instance DecidableEq for EntityType +deriving instance DecidableEq for EntityUID +deriving instance DecidableEq for Prim + +deriving instance Inhabited for Name +deriving instance Inhabited for EntityType +deriving instance Inhabited for EntityUID +deriving instance Inhabited for Prim + +deriving instance BEq for Except + +mutual + +def decValue (a b : Value) : Decidable (a = b) := by + cases a <;> cases b + case prim.prim pa pb => exact match decEq pa pb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case set.set sa sb => exact match decValueSet sa sb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case record.record ra rb => exact match decValueRecord ra rb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case ext.ext xa xb => exact match decEq xa xb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + all_goals { + apply isFalse + intro h + injection h + } + +def decValueList (as bs : List Value) : Decidable (as = bs) := + match as, bs with + | [], [] => isTrue rfl + | _::_, [] => isFalse (by intro; contradiction) + | [], _::_ => isFalse (by intro; contradiction) + | a::as, b::bs => + match decValue a b with + | isTrue h₁ => match decValueList as bs with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decProdAttrValue (as bs : Prod Attr Value) : Decidable (as = bs) := + match as, bs with + | (a1, a2), (b1, b2) => match decEq a1 b1 with + | isTrue h₀ => match decValue a2 b2 with + | isTrue h₁ => isTrue (by rw [h₀, h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decProdAttrValueList (as bs : List (Prod Attr Value)) : Decidable (as = bs) := + match as, bs with + | [], [] => isTrue rfl + | _::_, [] => isFalse (by intro; contradiction) + | [], _::_ => isFalse (by intro; contradiction) + | a::as, b::bs => + match decProdAttrValue a b with + | isTrue h₁ => match decProdAttrValueList as bs with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decValueSet (a b : Set Value) : Decidable (a = b) := by + match a, b with + | .mk la, .mk lb => exact match decValueList la lb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + done + +def decValueRecord (as bs : Map Attr Value) : Decidable (as = bs) := by + match as, bs with + | .mk ma, .mk mb => exact match decProdAttrValueList ma mb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) +end + +instance : DecidableEq Value := + decValue + +def Name.lt (a b : Name) : Bool := + (a.id < b.id) ∨ (a.id = b.id ∧ a.path < b.path) + +instance : LT Name where + lt a b := Name.lt a b + +instance Name.decLt (n m : Name) : Decidable (n < m) := + if h : Name.lt n m then isTrue h else isFalse h + +-- lol for some reason eta reduction breaks this (can't handle the implicit arguments) +instance : Ord EntityType where + compare a b := compareOfLessAndEq a b + +def EntityUID.lt (a b : EntityUID) : Bool := + (a.ty < b.ty) ∨ (a.ty = b.ty ∧ a.eid < b.eid) + +instance : LT EntityUID where + lt a b := EntityUID.lt a b + +instance EntityUID.decLt (n m : EntityUID) : Decidable (n < m) := + if h : EntityUID.lt n m then isTrue h else isFalse h + +instance : Ord EntityUID where + compare a b := compareOfLessAndEq a b + +def Bool.lt (a b : Bool) : Bool := match a,b with +| false, true => true +| _, _ => false + +instance : LT Bool where + lt a b := Bool.lt a b + +instance Bool.decLt (n m : Bool) : Decidable (n < m) := + if h : Bool.lt n m then isTrue h else isFalse h + +def Prim.lt (n m : Prim) : Bool := match n,m with + | .bool nb, .bool mb => nb < mb + | .int ni, .int mi => ni < mi + | .string ns, .string ms => ns < ms + | .entityUID nuid, .entityUID muid => nuid < muid + | .bool _, .int _ => True + | .bool _, .string _ => True + | .bool _, .entityUID _ => True + | .int _, .string _ => True + | .int _, .entityUID _ => True + | .string _, .entityUID _ => True + | _,_ => False + +instance : LT Prim where +lt := fun x y => Prim.lt x y + +instance Prim.decLt (n m : Prim) : Decidable (n < m) := +if h : Prim.lt n m then isTrue h else isFalse h + +mutual +def Value.lt (n m : Value) : Bool := match n,m with + | .prim x, .prim y => x < y + | .set (.mk lx), .set (.mk ly) => Values.lt lx ly lx.length + | .record (.mk lx), .record (.mk ly) => ValueAttrs.lt lx ly lx.length + | .ext x, .ext y => x < y + | .prim _, .set _ => True + | .prim _, .record _ => True + | .prim _, .ext _ => True + | .set _, .record _ => True + | .set _, .ext _ => True + | .set _, .prim _ => False + | .record _, .ext _ => True + | .record _, .prim _ => False + | .record _, .set _ => False + | .ext _, .prim _ => False + | .ext _, .set _ => False + | .ext _, .record _ => False + +def Values.lt (n m : List Value) (i : Nat): Bool := match n, m with + | [], [] => False + | [], _ => True + | _, [] => False + | n::ns, m::ms => Value.lt n m && Values.lt ns ms (i-1) + +def ValueAttrs.lt (n m : List (Prod String Value)) (i : Nat) : _root_.Bool := match n, m with + | [], [] => False + | [], _ => True + | _, [] => False + | (na, nv)::ns, (ma, mv)::ms => Value.lt nv mv && na < ma && ValueAttrs.lt ns ms (i-1) +end +termination_by +Value.lt as₁ as₂ => (sizeOf as₁, 0) +Values.lt as₁ as₂ i => (sizeOf as₁, as₁.length - i) +ValueAttrs.lt as₁ as₂ i => (sizeOf as₁, as₁.length - i) + +instance : LT Value where + lt := fun x y => Value.lt x y + +instance Value.decLt (n m : Value) : Decidable (n < m) := +if h : Value.lt n m then isTrue h else isFalse h + +instance : Ord Value where + compare a b := compareOfLessAndEq a b + + +deriving instance Inhabited for Value + +end Cedar.Spec \ No newline at end of file diff --git a/cedar-lean/Cedar/Spec/Wildcard.lean b/cedar-lean/Cedar/Spec/Wildcard.lean new file mode 100644 index 000000000..7b00e5006 --- /dev/null +++ b/cedar-lean/Cedar/Spec/Wildcard.lean @@ -0,0 +1,51 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +namespace Cedar.Spec + +inductive PatElem where + | star + | justChar (c : Char) +deriving Repr +deriving instance DecidableEq for PatElem +deriving instance Inhabited for PatElem + +abbrev Pattern := List PatElem + +def charMatch (textChar : Char) (patternChar : PatElem) : Bool := + match patternChar with + | .justChar c => textChar == c + | _ => false + +def wildcard (patternChar : PatElem) : Bool := + match patternChar with + | .star => true + | _ => false + +def wildcardMatch (text : String) (pattern : Pattern) : Bool := + match pattern with + | [] => match text with + | .mk [] => true + | _ => false + | p::ps => match text with + | .mk [] => wildcard p && wildcardMatch (.mk []) ps + | .mk (c::cs) => match wildcard p with + | true => wildcardMatch (.mk (c::cs)) ps || wildcardMatch (.mk cs) (p::ps) + | false => charMatch c p && wildcardMatch (.mk cs) ps + termination_by + wildcardMatch text pattern => sizeOf text + sizeOf pattern + +end Cedar.Spec diff --git a/cedar-lean/Cedar/Thm.lean b/cedar-lean/Cedar/Thm.lean new file mode 100644 index 000000000..e5cfe4bda --- /dev/null +++ b/cedar-lean/Cedar/Thm.lean @@ -0,0 +1,18 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Thm.Basic +import Cedar.Thm.Slicing diff --git a/cedar-lean/Cedar/Thm/Basic.lean b/cedar-lean/Cedar/Thm/Basic.lean new file mode 100644 index 000000000..243ff4051 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Basic.lean @@ -0,0 +1,104 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Thm.Lemmas.Authorizer + +/-! This file contains basic theorems about Cedar's authorizer. -/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec + +open Decision +open Effect +open Option + +/-- +Forbid trumps permit: if a `forbid` policy is satisfied, the request is denied. +-/ +theorem forbid_trumps_permit (request : Request) (entities : Entities) (policies : Policies) : + (∃ (policy : Policy), + policy ∈ policies ∧ + policy.effect = forbid ∧ + satisfied policy request entities) → + (isAuthorized request entities policies).decision = deny +:= by + intro h0 + unfold isAuthorized + generalize hf : (satisfiedPolicies forbid policies request entities) = forbids + generalize (satisfiedPolicies permit policies request entities) = permits + rcases (if_satisfied_then_satisfiedPolicies_non_empty forbid policies request entities h0) with h1 + rw [hf] at h1 + simp [h1] + +/-- +A request is explicitly permitted when there is at least one satisfied permit policy. +-/ +def IsExplicitlyPermitted (request : Request) (entities : Entities) (policies : Policies) : Prop := + ∃ (policy : Policy), + policy ∈ policies ∧ + policy.effect = permit ∧ + satisfied policy request entities + +/-- A request is allowed only if it is explicitly permitted. -/ +theorem allowed_if_explicitly_permitted (request : Request) (entities : Entities) (policies : Policies) : + (isAuthorized request entities policies).decision = allow → + IsExplicitlyPermitted request entities policies +:= by + unfold isAuthorized + generalize (satisfiedPolicies forbid policies request entities) = forbids + generalize hp : (satisfiedPolicies permit policies request entities) = permits + simp + cases forbids.isEmpty <;> simp + cases h0 : permits.isEmpty <;> simp + unfold IsExplicitlyPermitted + apply if_satisfiedPolicies_non_empty_then_satisfied permit policies + simp [hp, h0] + +/-- +Default deny: if not explicitly permitted, the request is denied. +This is contrapositive of allowed_if_explicitly_permitted. +-/ +theorem default_deny (request : Request) (entities : Entities) (policies : Policies) : + ¬ IsExplicitlyPermitted request entities policies → + (isAuthorized request entities policies).decision = deny +:= by + intro h0 + generalize h1 : (isAuthorized request entities policies).decision = dec + by_contra h2 + cases dec + case allow => + rcases (allowed_if_explicitly_permitted request entities policies h1) with h3 + contradiction + case deny => contradiction + +/-- +Order and duplicate independence: isAuthorized produces the same result +regardless of policy order or duplicates. +-/ +theorem order_and_dup_independent (request : Request) (entities : Entities) (policies₁ policies₂ : Policies) : + policies₁ ≡ policies₂ → + isAuthorized request entities policies₁ = isAuthorized request entities policies₂ +:= by + intro h + rcases (satisfiedPolicies_order_and_dup_independent forbid request entities policies₁ policies₂ h) with hf + rcases (satisfiedPolicies_order_and_dup_independent permit request entities policies₁ policies₂ h) with hp + unfold isAuthorized + simp [hf, hp] + +end Cedar.Thm \ No newline at end of file diff --git a/cedar-lean/Cedar/Thm/Lemmas/Authorizer.lean b/cedar-lean/Cedar/Thm/Lemmas/Authorizer.lean new file mode 100644 index 000000000..539377810 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Lemmas/Authorizer.lean @@ -0,0 +1,171 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Thm.Lemmas.Evaluator + +/-! +This file contains useful lemmas about the `Authorizer` functions. +-/ + +namespace Cedar.Thm + +open Cedar.Spec +open Cedar.Data + +theorem if_satisfied_then_satisfiedPolicies_non_empty (effect : Effect) (policies : Policies) (request : Request) (entities : Entities) : + (∃ policy, + policy ∈ policies ∧ + policy.effect = effect ∧ + satisfied policy request entities) → + (satisfiedPolicies effect policies request entities).isEmpty = false +:= by + intro h0 + cases h0 + case intro policy h1 => + rcases h1 with ⟨ha, hb, hc⟩ + unfold satisfiedPolicies + rw [←Set.make_non_empty] + apply @List.ne_nil_of_mem _ policy.id + simp [List.mem_filterMap] + apply Exists.intro policy + unfold satisfiedWithEffect + simp [ha, hb, hc] + + +theorem if_satisfiedPolicies_non_empty_then_satisfied (effect : Effect) (policies : Policies) (request : Request) (entities : Entities) : + (satisfiedPolicies effect policies request entities).isEmpty = false → + ∃ policy, + policy ∈ policies ∧ + policy.effect = effect ∧ + satisfied policy request entities +:= by + unfold satisfiedPolicies + intro h0 + rw [←Set.make_non_empty] at h0 + rcases List.exists_mem_of_ne_nil _ h0 with ⟨pid, h1⟩ + rw [List.mem_filterMap] at h1 + rcases h1 with ⟨policy, h1, h2⟩ + unfold satisfiedWithEffect at h2 + apply Exists.intro policy + simp [h1] + cases h3 : (policy.effect == effect) <;> simp at h3; simp [h3] at h2 + simp [h3] + cases h4 : (satisfied policy request entities) + case _ => simp [h3, h4] at h2 + case _ => rfl + +theorem satisfiedPolicies_order_and_dup_independent (effect : Effect) (request : Request) (entities : Entities) (policies₁ policies₂ : Policies) : + policies₁ ≡ policies₂ → + satisfiedPolicies effect policies₁ request entities = satisfiedPolicies effect policies₂ request entities +:= by + intro h₁ + unfold satisfiedPolicies + apply Set.make_eq_if_eqv + exact List.filterMap_equiv (satisfiedWithEffect effect · request entities) policies₁ policies₂ h₁ + +theorem sound_policy_slice_is_equisatisfied (effect : Effect) (request : Request) (entities : Entities) (slice policies : Policies) : + slice ⊆ policies → + (∀ policy, policy ∈ policies → policy ∉ slice → ¬ satisfied policy request entities) → + slice.filterMap (satisfiedWithEffect effect · request entities) ≡ + policies.filterMap (satisfiedWithEffect effect · request entities) +:= by + intros h₁ h₂ + simp [List.Equiv] + simp [List.subset_def] + apply And.intro <;> + intros pid policy h₃ h₄ <;> + apply Exists.intro policy <;> + simp [h₄] + case _ => + simp [List.subset_def] at h₁ + specialize h₁ h₃ + exact h₁ + case _ => + by_contra h₅ + specialize h₂ policy h₃ h₅ + unfold satisfiedWithEffect at h₄ + simp [h₂] at h₄ + +theorem satisfiedPolicies_eq_for_sound_policy_slice (effect : Effect) (request : Request) (entities : Entities) (slice policies : Policies) : + slice ⊆ policies → + (∀ policy, policy ∈ policies → policy ∉ slice → ¬ satisfied policy request entities) → + satisfiedPolicies effect slice request entities = satisfiedPolicies effect policies request entities +:= by + intro h₁ h₂ + unfold satisfiedPolicies + apply Set.make_eq_if_eqv + exact sound_policy_slice_is_equisatisfied effect request entities slice policies h₁ h₂ + +theorem satisfied_implies_principal_scope {policy : Policy} {request : Request} {entities : Entities} {uid : EntityUID} : + satisfied policy request entities = true → + policy.principalScope.scope.bound = .some uid → + inₑ request.principal uid entities = true +:= by + intro h₁ h₂ + simp [satisfied] at h₁ + unfold Policy.toExpr at h₁ + rcases (and_true_implies_left_true h₁) with h₃ + clear h₁ + simp [PrincipalScope.toExpr, Scope.toExpr] at h₃ + simp [Scope.bound, PrincipalScope.scope] at h₂ + generalize h₄ : policy.3.1 = x + simp only [h₄] at h₂ h₃ + cases x <;> simp at h₂ h₃ <;> + simp only [h₂] at h₃ + case eq => + simp [evaluate, Var.eqEntityUID, apply₂] at h₃ + simp [inₑ, h₃] + case mem => + simp [evaluate, Var.inEntityUID, apply₂] at h₃ + exact h₃ + case isMem => + rcases (and_true_implies_right_true h₃) with h₅ + simp [evaluate, Var.inEntityUID, apply₂] at h₅ + exact h₅ + +theorem satisfied_implies_resource_scope {policy : Policy} {request : Request} {entities : Entities} {uid : EntityUID} : + satisfied policy request entities = true → + policy.resourceScope.scope.bound = .some uid → + inₑ request.resource uid entities = true +:= by + intro h₁ h₂ + simp [satisfied] at h₁ + unfold Policy.toExpr at h₁ + rcases + (and_true_implies_left_true + (and_true_implies_right_true + (and_true_implies_right_true h₁))) with h₃ + clear h₁ + simp [ResourceScope.toExpr, Scope.toExpr] at h₃ + simp [Scope.bound, ResourceScope.scope] at h₂ + generalize h₄ : policy.5.1 = x + simp only [h₄] at h₂ h₃ + cases x <;> simp at h₂ h₃ <;> + simp only [h₂] at h₃ + case eq => + simp [evaluate, Var.eqEntityUID, apply₂] at h₃ + simp [inₑ, h₃] + case mem => + simp [evaluate, Var.inEntityUID, apply₂] at h₃ + exact h₃ + case isMem => + rcases (and_true_implies_right_true h₃) with h₅ + simp [evaluate, Var.inEntityUID, apply₂] at h₅ + exact h₅ + + +end Cedar.Thm \ No newline at end of file diff --git a/cedar-lean/Cedar/Thm/Lemmas/Evaluator.lean b/cedar-lean/Cedar/Thm/Lemmas/Evaluator.lean new file mode 100644 index 000000000..f9816df9f --- /dev/null +++ b/cedar-lean/Cedar/Thm/Lemmas/Evaluator.lean @@ -0,0 +1,69 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Thm.Lemmas.Std + +/-! +This file contains useful lemmas about the `Evaluator` functions. +-/ + +namespace Cedar.Thm + +open Cedar.Spec +open Cedar.Data + + +theorem and_true_implies_left_true {e₁ e₂ : Expr} {request : Request} {entities : Entities} : + evaluate (Expr.and e₁ e₂) request entities = .ok true → + evaluate e₁ request entities = .ok true +:= by + intro h₁ + simp [evaluate, Result.as] at h₁ + generalize h₂ : (evaluate e₁ request entities) = r₁ + simp [h₂] at h₁ + cases r₁ <;> simp at h₁ + case ok v₁ => + generalize h₃ : (Coe.coe v₁ : Result Bool) = rb + simp [h₃] at h₁ + cases rb <;> simp at h₁ + case ok b => + cases b <;> simp at h₁ + simp [Coe.coe, Value.asBool] at h₃ + cases v₁ <;> try simp at h₃ + case _ p₁ => + cases p₁ <;> simp at h₃ + simp [h₃] + +theorem and_true_implies_right_true {e₁ e₂ : Expr} {request : Request} {entities : Entities} : + evaluate (Expr.and e₁ e₂) request entities = .ok true → + evaluate e₂ request entities = .ok true +:= by + intro h₁ + rcases (and_true_implies_left_true h₁) with h₂ + simp [evaluate, h₂, Result.as, Coe.coe, Value.asBool] at h₁ + generalize h₃ : (evaluate e₂ request entities) = r₂ + simp [h₃] at h₁ + cases r₂ <;> simp [Lean.Internal.coeM] at h₁ + case ok v₂ => + cases v₂ <;> try simp at h₁ + case _ p₂ => + cases p₂ <;> simp at h₁ + case _ b => + cases b <;> simp at h₁ + rfl + +end Cedar.Thm \ No newline at end of file diff --git a/cedar-lean/Cedar/Thm/Lemmas/Std.lean b/cedar-lean/Cedar/Thm/Lemmas/Std.lean new file mode 100644 index 000000000..e09a7c5e2 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Lemmas/Std.lean @@ -0,0 +1,33 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +/-! +This file contains useful auxiliary lemmas about standard Lean datatypes and +functions. +-/ + +-- The `Except.bind_*` theorems let `simp` reduce terms that use the `do` notation. +@[simp] theorem Except.bind_ok_T (a : α) (f : α → ExceptT ε Id β) : + (bind (Except.ok a) f : ExceptT ε Id β) = f a +:= by rfl + +@[simp] theorem Except.bind_ok (a : α) (f : α → Except ε β) : + (bind (Except.ok a) f : Except ε β) = f a +:= by rfl + +@[simp] theorem Except.bind_err (e : ε) (f : α → Except ε β) : + (bind (Except.error e) f : Except ε β) = (Except.error e) +:= by rfl \ No newline at end of file diff --git a/cedar-lean/Cedar/Thm/Slicing.lean b/cedar-lean/Cedar/Thm/Slicing.lean new file mode 100644 index 000000000..bd23fc18e --- /dev/null +++ b/cedar-lean/Cedar/Thm/Slicing.lean @@ -0,0 +1,196 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Thm.Lemmas.Authorizer +import Mathlib.Data.List.Basic + +/-! +This file defines what it means for a policy slice to be sound. + +We prove two main theorems: + +* Authorization returns the same response for a sound policy slice as for the + original collection of policies (`isAuthorized_eq_for_sound_policy_slice`). +* It is sound to slice policies based on scope constraints (see + `isAuthorized_eq_for_scope_based_policy_slice`). The proof is based on a more + general lemma (`sound_bound_analysis_produces_sound_slices`) that covers all + forms of slicing that are based on identifying "bound" principal and resource + entities (if any) for a policy, such that the policy evaluates to true on an + input only if the request principal and resource are descendents of the + corresponding bound entities. Currently, we are extracting bounds only from + the scope constraints. The general lemma also covers more sophisticated + analyses that can extract bounds from policy conditions as well. +--/ + +namespace Cedar.Thm + +open Cedar.Spec + +/-- +A policy slice is a subset of a collection of policies. This slice is sound for +a given request and entities if every policy in the collection that is not in the slice is also +not satisfied with respect to the request and entities. +-/ +def IsSoundPolicySlice (req : Request) (entities : Entities) (slice policies : Policies) : Prop := + slice ⊆ policies ∧ + ∀ policy, + policy ∈ policies → + policy ∉ slice → + ¬ satisfied policy req entities + +/-- +Policy slicing soundness: `isAuthorized` produces the same result for a sound +slice (subset) of a collection of policies as it does for the original policies. +-/ +theorem isAuthorized_eq_for_sound_policy_slice (req : Request) (entities : Entities) (slice policies : Policies) : + IsSoundPolicySlice req entities slice policies → + isAuthorized req entities slice = isAuthorized req entities policies +:= by + intro h₀ + have hf : satisfiedPolicies .forbid slice req entities = satisfiedPolicies .forbid policies req entities := + satisfiedPolicies_eq_for_sound_policy_slice .forbid req entities slice policies h₀.left h₀.right + have hp : satisfiedPolicies .permit slice req entities = satisfiedPolicies .permit policies req entities := + satisfiedPolicies_eq_for_sound_policy_slice .permit req entities slice policies h₀.left h₀.right + unfold isAuthorized + simp [hf, hp] + +/-- +A policy bound consists of optional `principal` and `resource` entities. +-/ +structure PolicyBound where + principalBound : Option EntityUID + resourceBound : Option EntityUID + +def inSomeOrNone (uid : EntityUID) (opt : Option EntityUID) (entities : Entities) : Bool := + match opt with + | .some uid' => inₑ uid uid' entities + | .none => true + +/-- +A bound is satisfied by a request and store if the request principal and +resource fields are descendents of the corresponding bound fields (or if those +bound fields are `none`). +-/ +def satisfiedBound (bound : PolicyBound) (request : Request) (entities : Entities) : Bool := + inSomeOrNone request.principal bound.principalBound entities ∧ + inSomeOrNone request.resource bound.resourceBound entities + +/-- +A bound is sound for a given policy if the bound is satisfied for every +request and entities for which the policy is satisfied. +-/ +def IsSoundPolicyBound (bound : PolicyBound) (policy : Policy) : Prop := + ∀ (request : Request) (entities : Entities), + satisfied policy request entities → + satisfiedBound bound request entities + +/-- +A bound analysis takes as input a policy and returns a PolicyBound. +-/ +abbrev BoundAnalysis := Policy → PolicyBound + +def BoundAnalysis.slice (ba : BoundAnalysis) (request : Request) (entities : Entities) (policies : Policies) : Policies := + policies.filter (fun policy => satisfiedBound (ba policy) request entities) + +/-- +A bound analysis is sound if it produces sound bounds for all policies. +-/ +def IsSoundBoundAnalysis (ba : BoundAnalysis) : Prop := + ∀ (policy : Policy), IsSoundPolicyBound (ba policy) policy + +/-- +A sound bound analysis produces sound policy slices. +-/ +theorem sound_bound_analysis_produces_sound_slices (ba : BoundAnalysis) (request : Request) (entities : Entities) (policies : Policies) : + IsSoundBoundAnalysis ba → + IsSoundPolicySlice request entities (ba.slice request entities policies) policies +:= by + unfold IsSoundBoundAnalysis + unfold IsSoundPolicySlice + intro h₁ + unfold BoundAnalysis.slice + apply And.intro + case left => + apply List.filter_subset + case right => + intro policy + specialize h₁ policy + intro h₂ h₃ + rw [List.mem_filter] at h₃ + simp [h₂] at h₃ + by_contra h₄ + unfold IsSoundPolicyBound at h₁ + specialize h₁ request entities h₄ + simp [h₃] at h₁ + +/-- +Scope-based bound analysis extracts the bound from the policy scope. +-/ +def scopeAnalysis (policy : Policy) : PolicyBound := + { + principalBound := policy.principalScope.scope.bound, + resourceBound := policy.resourceScope.scope.bound, + } + +/-- +Scope-based bounds are sound. +-/ +theorem scope_bound_is_sound (policy : Policy) : + IsSoundPolicyBound (scopeAnalysis policy) policy +:= by + unfold IsSoundPolicyBound + intro request entities h₁ + unfold scopeAnalysis + unfold satisfiedBound + unfold Scope.bound + unfold inSomeOrNone + simp only [Bool.decide_and, Bool.decide_coe, Bool.and_eq_true] + apply And.intro + case left => + generalize h₂ : policy.principalScope.scope = s + cases s <;> simp <;> + apply satisfied_implies_principal_scope h₁ <;> + unfold Scope.bound <;> simp [h₂] + case right => + generalize h₂ : policy.resourceScope.scope = s + cases s <;> simp <;> + apply satisfied_implies_resource_scope h₁ <;> + unfold Scope.bound <;> simp [h₂] + +/-- +Scope-based bound analysis is sound. +-/ +theorem scope_analysis_is_sound : + IsSoundBoundAnalysis scopeAnalysis +:= by + unfold IsSoundBoundAnalysis + apply scope_bound_is_sound + +/-- +Scope-based slicing is sound: `isAuthorized` produces the same result for a +scope-based slice of a collection of policies as it does for the original +policies. +-/ +theorem isAuthorized_eq_for_scope_based_policy_slice (request : Request) (entities : Entities) (policies : Policies) : + isAuthorized request entities (BoundAnalysis.slice scopeAnalysis request entities policies) = + isAuthorized request entities policies +:= by + apply isAuthorized_eq_for_sound_policy_slice + apply sound_bound_analysis_produces_sound_slices + exact scope_analysis_is_sound + +end Cedar.Thm diff --git a/cedar-lean/Cedar/Validation.lean b/cedar-lean/Cedar/Validation.lean new file mode 100644 index 000000000..2f8780fb5 --- /dev/null +++ b/cedar-lean/Cedar/Validation.lean @@ -0,0 +1,19 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Validation.Types +import Cedar.Validation.Subtyping +import Cedar.Validation.Typechecker \ No newline at end of file diff --git a/cedar-lean/Cedar/Validation/Subtyping.lean b/cedar-lean/Cedar/Validation/Subtyping.lean new file mode 100644 index 000000000..ec1dc8498 --- /dev/null +++ b/cedar-lean/Cedar/Validation/Subtyping.lean @@ -0,0 +1,68 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Validation.Types +import Cedar.Spec + +namespace Cedar.Validation + +open Cedar.Data +open Cedar.Spec + +def lubBool (b₁ b₂ : BoolType) : BoolType := + if b₁ = b₂ then b₁ else .anyBool + +mutual + def lubQualifiedType (q₁ q₂ : QualifiedType) : Option QualifiedType := + match q₁, q₂ with + | .optional ty₁, .optional ty₂ => do let ty ← lub? ty₁ ty₂; .some (.optional ty) + | .required ty₁, .required ty₂ => do let ty ← lub? ty₁ ty₂; .some (.required ty) + | _, _ => .none + + def lubRecordType (ty₁ ty₂ : List (Attr × QualifiedType)) : Option (List (Attr × QualifiedType)) := + match ty₁, ty₂ with + | [], [] => .some [] + | (k₁, v₁)::r₁, (k₂, v₂)::r₂ => + if k₁ != k₂ + then .none + else do + let ty ← lubQualifiedType v₁ v₂ + let tys ← lubRecordType r₁ r₂ + .some ((k₁, ty) :: tys) + | _, _ => .none + + + def lub? (ty₁ ty₂ : CedarType) : Option CedarType := + match ty₁, ty₂ with + | .bool b₁, .bool b₂ => .some (.bool (lubBool b₁ b₂)) + | .set s₁, .set s₂ => do + let lub ← lub? s₁ s₂ + .some (.set lub) + | .record (.mk r₁), .record (.mk r₂) => do + let lub ← lubRecordType r₁ r₂ + .some (.record (Map.mk lub)) + | _, _ => .none +end + +def subty (ty₁ ty₂ : CedarType) : Bool := + match lub? ty₁ ty₂ with + | .some ty => ty = ty₂ + | .none => false + +infix:50 " ⊔ " => lub? +infix:50 " ⊑ " => subty + +end Cedar.Validation \ No newline at end of file diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean new file mode 100644 index 000000000..b83d68ae0 --- /dev/null +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -0,0 +1,287 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Validation.Types +import Cedar.Validation.Subtyping + +namespace Cedar.Validation + +open Cedar.Data +open Cedar.Spec + +abbrev Capabilities := List (Expr × Attr) + +def Capabilities.singleton (e : Expr) (a : Attr) : Capabilities := [(e, a)] + +abbrev ResultType := Except TypeError (CedarType × Capabilities) + +def ok (ty : CedarType) (c : Capabilities := ∅) : ResultType := .ok (ty, c) +def err (e : TypeError) : ResultType := .error e + +structure RequestType where + principal : EntityType + action : EntityUID + resource : EntityType + context : RecordType + +structure Environment where + ets : EntityTypeStore + acts : ActionStore + reqty : RequestType + +def typeOfLit (p : Prim) (env : Environment) : ResultType := + match p with + | .bool true => ok (.bool .tt) + | .bool false => ok (.bool .ff) + | .int _ => ok .int + | .string _ => ok .string + | .entityUID uid => + if env.ets.contains uid.ty || env.acts.contains uid + then ok (.entity uid.ty) + else err (.unknownEntity uid.ty) + +def typeOfVar (v : Var) (env : Environment) : ResultType := + match v with + | .principal => ok (.entity env.reqty.principal) + | .action => ok (.entity env.reqty.action.ty) + | .resource => ok (.entity env.reqty.resource) + | .context => ok (.record env.reqty.context) + +def typeOfIf (r₁ : CedarType × Capabilities) (r₂ r₃ : ResultType) : ResultType := + match r₁ with + | (.bool .tt, c₁) => do + let (ty₂, c₂) ← r₂ + ok ty₂ (c₁.union c₂) + | (.bool .ff, _) => r₃ + | (.bool .anyBool, c₁) => do + let (ty₂, c₂) ← r₂ + let (ty₃, c₃) ← r₃ + match ty₂ ⊔ ty₃ with + | .some ty => ok ty ((c₁ ∪ c₂) ∩ c₃) + | .none => err (.lubErr ty₂ ty₃) + | (ty₁, _) => err (.unexpectedType ty₁) + +def typeOfAnd (r₁ : CedarType × Capabilities) (r₂ : ResultType) : ResultType := + match r₁ with + | (.bool .ff, _) => ok (.bool .ff) + | (.bool ty₁, c₁) => do + let (ty₂, c₂) ← r₂ + match ty₂ with + | .bool .ff => ok (.bool .ff) + | .bool .tt => ok (.bool ty₁) (c₁ ∪ c₂) + | .bool _ => ok (.bool .anyBool) (c₁ ∪ c₂) + | _ => err (.unexpectedType ty₂) + | (ty₁, _) => err (.unexpectedType ty₁) + +def typeOfOr (r₁ : CedarType × Capabilities) (r₂ : ResultType) : ResultType := + match r₁ with + | (.bool .tt, _) => ok (.bool .tt) + | (.bool .ff, _) => r₂ + | (.bool ty₁, c₁) => do + let (ty₂, c₂) ← r₂ + match ty₂ with + | .bool .tt => ok (.bool .tt) + | .bool .ff => ok (.bool ty₁) c₁ + | .bool _ => ok (.bool .anyBool) (c₁ ∩ c₂) + | _ => err (.unexpectedType ty₂) + | (ty₁, _) => err (.unexpectedType ty₁) + +def typeOfUnaryApp (op : UnaryOp) (ty : CedarType) : ResultType := + match op, ty with + | .not, .bool x => ok (.bool x.not) + | .neg, .int => ok .int + | .mulBy _, .int => ok .int + | .like _, .string => ok (.bool .anyBool) + | .is ety₁, .entity ety₂ => ok (.bool (if ety₁ = ety₂ then .tt else .ff)) + | _, _ => err (.unexpectedType ty) + +def typeOfEq (ty₁ ty₂ : CedarType) (x₁ x₂ : Expr) : ResultType := + match x₁, x₂ with + | .lit p₁, .lit p₂ => if p₁ == p₂ then ok (.bool .tt) else ok (.bool .ff) + | _, _ => + match ty₁ ⊔ ty₂ with + | .some _ => ok (.bool .anyBool) + | .none => + if ty₁.isPrimType || ty₂.isPrimType + then ok (.bool .ff) + else err (.lubErr ty₁ ty₂) + +def entityUID? : Expr → Option EntityUID + | .lit (.entityUID uid) => .some uid + | _ => .none + +def entityUIDs? : Expr → Option (List EntityUID) + | .set xs => xs.mapM entityUID? + | _ => .none + +def actionUID? (x : Expr) (acts: ActionStore) : Option EntityUID := do + let uid ← entityUID? x + if acts.contains uid then .some uid else .none + +-- x₁ in x₂ where x₁ has type ety₁ and x₂ has type ety₂ +def typeOfInₑ (ety₁ ety₂ : EntityType) (x₁ x₂ : Expr) (env : Environment) : ResultType := + match actionUID? x₁ env.acts, entityUID? x₂ with + | .some uid₁, .some uid₂ => + if env.acts.descendentOf uid₁ uid₂ + then ok (.bool .tt) + else ok (.bool .ff) + | _, _ => + if env.ets.descendentOf ety₁ ety₂ + then ok (.bool .anyBool) + else ok (.bool .ff) + +-- x₁ in x₂ where x₁ has type ety₁ and x₂ has type (.set ety₂) +def typeOfInₛ (ety₁ ety₂ : EntityType) (x₁ x₂ : Expr) (env : Environment) : ResultType := + match actionUID? x₁ env.acts, entityUIDs? x₂ with + | .some uid₁, .some uids => + if uids.any (env.acts.descendentOf uid₁ ·) + then ok (.bool .tt) + else ok (.bool .ff) + | _, _ => + if env.ets.descendentOf ety₁ ety₂ + then ok (.bool .anyBool) + else ok (.bool .ff) + +def ifLubThenBool (ty₁ ty₂ : CedarType) : ResultType := + match ty₁ ⊔ ty₂ with + | some _ => ok (.bool .anyBool) + | none => err (.lubErr ty₁ ty₂) + +def typeOfBinaryApp (op₂ : BinaryOp) (ty₁ ty₂ : CedarType) (x₁ x₂ : Expr) (env : Environment) : ResultType := + match op₂, ty₁, ty₂ with + | .eq, _, _ => typeOfEq ty₁ ty₂ x₁ x₂ + | .mem, .entity ety₁, .entity ety₂ => typeOfInₑ ety₁ ety₂ x₁ x₂ env + | .mem, .entity ety₁, .set (.entity ety₂) => typeOfInₛ ety₁ ety₂ x₁ x₂ env + | .less, .int, .int => ok (.bool .anyBool) + | .lessEq, .int, .int => ok (.bool .anyBool) + | .add, .int, .int => ok .int + | .sub, .int, .int => ok .int + | .contains, .set ty₃, _ => ifLubThenBool ty₂ ty₃ + | .containsAll, .set ty₃, .set ty₄ => ifLubThenBool ty₃ ty₄ + | .containsAny, .set ty₃, .set ty₄ => ifLubThenBool ty₃ ty₄ + | _, _, _ => err (.unexpectedType ty₁) + +def hasAttrInRecord (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType := + match rty.find? a with + | .some (.required _) => ok (.bool .tt) + | .some (.optional _) => + if (x, a) ∈ c + then ok (.bool .tt) + else ok (.bool .anyBool) (Capabilities.singleton x a) + | .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 + | .entity ety => + match env.ets.attrs? ety with + | .some rty => hasAttrInRecord rty x a c + | .none => err (.unknownEntity ety) + | _ => err (.unexpectedType ty) + +def getAttrInRecord (ty : CedarType) (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType := + match rty.find? a with + | .some (.required aty) => ok aty + | .some (.optional aty) => if (x, a) ∈ c then ok aty else err (.attrNotFound ty a) + | .none => err (.attrNotFound ty a) + +def typeOfGetAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env : Environment) : ResultType := + match ty with + | .record rty => getAttrInRecord ty rty x a c + | .entity ety => + match env.ets.attrs? ety with + | .some rty => getAttrInRecord ty rty x a c + | .none => err (.unknownEntity ety) + | _ => err (.unexpectedType ty) + +def typeOfSet (tys : List CedarType) : ResultType := + match tys with + | [] => err .emptySetErr + | hd :: tl => + match tl.foldrM lub? hd with + | .some ty => ok (.set ty) + | .none => err (.incompatibleSetTypes tys) + +def justType (r : ResultType) : Except TypeError CedarType := + r.map Prod.fst + +def requiredAttr (a : Attr) (r : ResultType) : Except TypeError (Attr × QualifiedType) := + r.map λ (ty, _) => (a, .required ty) + +def typeOfConstructor (mk : String → Option α) (xs : List Expr) (ty : CedarType) : ResultType := + match xs with + | [.lit (.string s)] => + match (mk s) with + | .some _ => ok ty + | .none => err (.extensionErr xs) + | _ => err (.extensionErr xs) + +def typeOfCall (xfn : ExtFun) (tys : List CedarType) (xs : List Expr) : ResultType := + match xfn, tys with + | .decimal, _ => typeOfConstructor Cedar.Spec.Ext.Decimal.decimal xs (.ext .decimal) + | .ip, _ => typeOfConstructor Cedar.Spec.Ext.IPAddr.ip xs (.ext .ipAddr) + | .lessThan, [.ext .decimal, .ext .decimal] => ok (.bool .anyBool) + | .lessThanOrEqual, [.ext .decimal, .ext .decimal] => ok (.bool .anyBool) + | .greaterThan, [.ext .decimal, .ext .decimal] => ok (.bool .anyBool) + | .greaterThanOrEqual, [.ext .decimal, .ext .decimal] => ok (.bool .anyBool) + | .isIpv4, [.ext .ipAddr] => ok (.bool .anyBool) + | .isIpv6, [.ext .ipAddr] => ok (.bool .anyBool) + | .isLoopback, [.ext .ipAddr] => ok (.bool .anyBool) + | .isMulticast, [.ext .ipAddr] => ok (.bool .anyBool) + | .isInRange, [.ext .ipAddr, .ext .ipAddr] => ok (.bool .anyBool) + | _, _ => err (.extensionErr xs) + + +-- Note: if x types as .tt or .ff, it is okay to replace x with the literal +-- expression true or false if x can never throw an extension error at runtime. +-- This is true for the current version of Cedar. +def typeOf (x : Expr) (c : Capabilities) (env : Environment) : ResultType := + match x with + | .lit p => typeOfLit p env + | .var v => typeOfVar v env + | .ite x₁ x₂ x₃ => do + let (ty₁, c₁) ← typeOf x₁ c env + typeOfIf (ty₁, c₁) (typeOf x₂ (c ∪ c₁) env) (typeOf x₃ c env) + | .and x₁ x₂ => do + let (ty₁, c₁) ← typeOf x₁ c env + typeOfAnd (ty₁, c₁) (typeOf x₂ (c ∪ c₁) env) + | .or x₁ x₂ => do + let (ty₁, c₁) ← typeOf x₁ c env + typeOfOr (ty₁, c₁) (typeOf x₂ c env) + | .unaryApp op₁ x₁ => do + let (ty₁, _) ← typeOf x₁ c env + typeOfUnaryApp op₁ ty₁ + | .binaryApp op₂ x₁ x₂ => do + let (ty₁, _) ← typeOf x₁ c env + let (ty₂, _) ← typeOf x₂ c env + typeOfBinaryApp op₂ ty₁ ty₂ x₁ x₂ env + | .hasAttr x₁ a => do + let (ty₁, _) ← typeOf x₁ c env + typeOfHasAttr ty₁ x₁ a c env + | .getAttr x₁ a => do + let (ty₁, _) ← typeOf x₁ c env + typeOfGetAttr ty₁ x₁ a c env + | .set xs => do + let tys ← xs.mapM₁ (λ ⟨x₁, _⟩ => justType (typeOf x₁ c env)) + typeOfSet tys + | .record axs => do + let atys ← axs.mapM₂ (λ ⟨(a₁, x₁), _⟩ => requiredAttr a₁ (typeOf x₁ c env)) + ok (.record (Map.make atys)) + | .call xfn xs => do + let tys ← xs.mapM₁ (λ ⟨x₁, _⟩ => justType (typeOf x₁ c env)) + typeOfCall xfn tys xs + +end Cedar.Validation \ No newline at end of file diff --git a/cedar-lean/Cedar/Validation/Types.lean b/cedar-lean/Cedar/Validation/Types.lean new file mode 100644 index 000000000..3172923a1 --- /dev/null +++ b/cedar-lean/Cedar/Validation/Types.lean @@ -0,0 +1,177 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec + +namespace Cedar.Validation +open Cedar.Data +open Cedar.Spec + +----- Definitions ----- + +inductive BoolType where + | anyBool + | tt + | ff + +def BoolType.not : BoolType → BoolType + | .anyBool => .anyBool + | .tt => .ff + | .ff => .tt + +inductive ExtType where + | ipAddr + | decimal + +inductive Qualified (α : Type u) where + | optional (a : α) + | required (a : α) + +inductive CedarType where + | bool (bty : BoolType) + | int + | string + | entity (ety : EntityType) + | set (ty : CedarType) + | record (rty : Map Attr (Qualified CedarType)) + | ext (xty : ExtType) + +def CedarType.isPrimType : CedarType → Bool +| bool _ | int | string | entity _ => true +| _ => false + +abbrev QualifiedType := Qualified CedarType + +abbrev RecordType := Map Attr QualifiedType + +inductive TypeError where + | lubErr (ty₁ : CedarType) (ty₂ : CedarType) + | unexpectedType (ty : CedarType) + | attrNotFound (ty : CedarType) (attr : Attr) + | unknownEntity (ety : EntityType) + | extensionErr (xs : List Expr) + | emptySetErr + | incompatibleSetTypes (ty : List CedarType) + +abbrev EntityTypeStore := Map EntityType (RecordType × (Cedar.Data.Set EntityType)) + +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 + +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₂ + | .none => false + +abbrev ActionStore := Map EntityUID (Cedar.Data.Set EntityUID) + +def ActionStore.contains (as : ActionStore) (uid : EntityUID) : Bool := + (as.find? uid).isSome + +def ActionStore.descendentOf (as : ActionStore) (uid₁ uid₂ : EntityUID) : Bool := + if uid₁ == uid₂ + then true + else match as.find? uid₁ with + | .some ancs => ancs.contains uid₂ + | .none => false + +----- Derivations ----- + +deriving instance DecidableEq for BoolType +deriving instance DecidableEq for ExtType + +mutual + +def decCedarType (a b : CedarType) : Decidable (a = b) := by + cases a <;> cases b + case string.string => apply isTrue (by rfl) + case int.int => apply isTrue (by rfl) + case bool.bool b1 b2 => exact match decEq b1 b2 with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case set.set t1 t2 => exact match decCedarType t1 t2 with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case entity.entity lub1 lub2 => exact match decEq lub1 lub2 with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case record.record r1 r2 => exact match decAttrQualifiedCedarTypeMap r1 r2 with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case ext.ext n1 n2 => exact match decEq n1 n2 with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + all_goals { + apply isFalse + intro h + injection h + } + +def decQualifiedCedarType (a b : QualifiedType) : Decidable (a = b) := by + cases a <;> cases b + case optional.optional a' b' => exact match decCedarType a' b' with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + case required.required a' b' => exact match decCedarType a' b' with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + all_goals { + apply isFalse + intro h + injection h + } + +def decProdAttrQualifiedCedarType (a b : Prod Attr QualifiedType) : Decidable (a = b) := + match a, b with + | (a1, a2), (b1, b2) => match decEq a1 b1 with + | isTrue h₀ => match decQualifiedCedarType a2 b2 with + | isTrue h₁ => isTrue (by rw [h₀, h₁]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decProdAttrQualifiedCedarTypeList (as bs : List (Prod Attr QualifiedType)) : Decidable (as = bs) := + match as, bs with + | [], [] => isTrue rfl + | _::_, [] => isFalse (by intro; contradiction) + | [], _::_ => isFalse (by intro; contradiction) + | a::as, b::bs => + match decProdAttrQualifiedCedarType a b with + | isTrue h₁ => match decProdAttrQualifiedCedarTypeList as bs with + | isTrue h₂ => isTrue (by rw [h₁, h₂]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +def decAttrQualifiedCedarTypeMap (as bs : Map Attr QualifiedType) : Decidable (as = bs) := by + match as, bs with + | Map.mk ma, Map.mk mb => exact match decProdAttrQualifiedCedarTypeList ma mb with + | isTrue h => isTrue (by rw [h]) + | isFalse _ => isFalse (by intro h; injection h; contradiction) + +end + +instance : DecidableEq CedarType := decCedarType + +deriving instance DecidableEq for Qualified +deriving instance DecidableEq for TypeError + +deriving instance Inhabited for CedarType + +end Cedar.Validation \ No newline at end of file diff --git a/cedar-lean/GUIDE.md b/cedar-lean/GUIDE.md new file mode 100644 index 000000000..2bb74c9e5 --- /dev/null +++ b/cedar-lean/GUIDE.md @@ -0,0 +1,62 @@ +# Style guidelines for Cedar Lean + +The Cedar Lean formalization uses the following coding conventions, adapted from [Lean 4](https://leanprover.github.io/lean4/doc/lean3changes.html#style-changes) and [Mathlib 4](https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention). + +## Imports + +Sort `import` and `open` statements lexicographically. Keep imports to a minimum. + +## Casing + +* Type variables are lower-case Greek letters. +* Theorem names and `Prop` terms are in `lower_snake_case`. +* Inductive types, structures, typeclasses, modules, and namespaces use `UpperCamelCase`. +* Constructors of inductive types use `lowerCamelCase`. +* Function names are `lowerCamelCase` unless they return a `Prop`, in which case they are `UpperCamelCase`. +* Everything else (e.g., structure fields and local variables) is `lowerCamelCase`. + +## Indentation + +Declaration and theorem bodies should always be indented: + +``` +inductive Hello where + | world + | planet + +structure Point where + x : Nat + y : Nat + +def Point.addX : Point → Point → Nat := + fun { x := a, .. } { x := b, .. } => a + b +``` + +In structures and typeclass definitions, prefer `where` to `:=`. + +## Theorem statements + +Indent long theorem statements. + +Minimize the use of explicitly named hypotheses, and use implications instead. + +For example, prefer anonymous hypotheses, like this: +``` +theorem even_is_not_odd (n : Nat) : Even n -> ¬ Odd n +:= by ... +``` + +Over named hypotheses, like this: + +``` +theorem even_is_not_odd (n : Nat) (isEven : Even n) : ¬ Odd n +:= by ... +``` + +To break up implications across multiple lines: +* If there is only one hypothesis (e.g., `A -> B`), put the implication symbol at the end of the first line (e.g., `A ->\n B`). +* Otherwise, put the implication symbol at the start of the subsequent lines (e.g., `A \n-> B \n-> C`). + +## Comments + +Main theorems should have a docstring comment `/-- ... -/` explaining what is proven. See [here](https://leanprover-community.github.io/contribute/doc.html) for more information on the Mathlib documentation style. diff --git a/cedar-lean/README.md b/cedar-lean/README.md new file mode 100644 index 000000000..c8199a606 --- /dev/null +++ b/cedar-lean/README.md @@ -0,0 +1,67 @@ +# Cedar Lean + +This folder contains the Lean formalization of, and proofs about, Cedar. + +## Setup + +Follow [these instructions](https://leanprover.github.io/lean4/doc/setup.html) to set up Lean and install the VS Code plugin. + + +## Usage + +To use VS Code, open the `cedar-lean` folder as the root directory. + +To build code and proofs from the command line: +``` +$ cd cedar-lean +$ lake build Cedar +``` + +The the first build may take a while because it builds the `mathlib4` library that Cedar depends on. Subsequent builds will be fast. + +To run the unit tests: +``` +$ lake exe CedarUnitTests +``` + +## Updating the Lean toolchain + +Cedar depends on [`mathlib4`](https://github.com/leanprover-community/mathlib4), and it is configured to use the same version of Lean as `mathlib4`. + +Follow [these instructions](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4) to update to the latest version of `mathlib4` and Lean: + +``` +$ curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain +$ lake update +$ lake exe cache get +``` + +## Contributing + +To [contribute](../CONTRIBUTING.md) Lean code or proofs, follow these [style guidelines](GUIDE.md). + +## Key definitions + +Definitional engine ([`Cedar/Spec/`](Cedar/Spec/)) + +* [`evaluate`](Cedar/Spec/Evaluator.lean#L76) returns the result of evaluating an expression. +* [`satisfied`](Cedar/Spec/Authorizer.lean#L27) checks if a policy is satisfied for a given request and entities. +* [`isAuthorized`](Cedar/Spec/Authorizer.lean#L38) checks if a request is allowed or denied for a given policy store and entities. + +Definitional validator ([`Cedar/Validation/`](Cedar/Validation/)) + +* [`typeOf`](Cedar/Validation/Typechecker.lean#L235) returns the result of type checking an expression against a schema. + +## Verified properties + +Basic theorems ([`Cedar/Thm/Basic.lean`](Cedar/Thm/Basic.lean)) + +* If some forbid policy is satisfied, then the request is denied. +* A request is allowed only if it is explicitly permitted (i.e., there is at least one permit policy that is satisfied). +* If not explicitly permitted, a request is denied. +* Authorization produces the same result regardless of policy evaluation order or duplicates. + +Sound policy slicing ([`Cedar/Thm/Slicing.lean`](Cedar/Thm/Slicing.lean)) + +* Given a _sound policy slice_, the result of authorization is the same with the slice as it is with the full policy store. + diff --git a/cedar-lean/UnitTest.lean b/cedar-lean/UnitTest.lean new file mode 100644 index 000000000..b11206228 --- /dev/null +++ b/cedar-lean/UnitTest.lean @@ -0,0 +1,20 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import UnitTest.Decimal +import UnitTest.IPAddr +import UnitTest.Main +import UnitTest.Run \ No newline at end of file diff --git a/cedar-lean/UnitTest/Decimal.lean b/cedar-lean/UnitTest/Decimal.lean new file mode 100644 index 000000000..f714c53b0 --- /dev/null +++ b/cedar-lean/UnitTest/Decimal.lean @@ -0,0 +1,64 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Ext.Decimal +import UnitTest.Run + +/-! This file defines unit tests for Decimal functions. -/ + +namespace UnitTest.Decimal + +open Cedar.Spec.Ext.Decimal + +private def testValid (str : String) (rep : Int) : TestCase := + test str (checkEq (parse str) (decimal? rep)) + +def testsForValidStrings := + suite "Decimal.parse for valid strings" + [ + testValid "0.0" 0, + testValid "0.0000" 0, + testValid "12.34" 123400, + testValid "1.2345" 12345, + testValid "-1.0" (-10000), + testValid "-4.2" (-42000), + testValid "-9.876" (-98760), + testValid "-922337203685477.5808" (-9223372036854775808), + testValid "922337203685477.5807" 9223372036854775807 + ] + +private def testInvalid (str : String) (msg : String) : TestCase := + test s!"{str} [{msg}]" (checkEq (parse str) .none) + +def testsForInvalidStrings := + suite "Decimal.parse for invalid strings" + [ + testInvalid "1.x" "invalid characters", + testInvalid "1.-2" "invalid use of -", + testInvalid "12" "no decimal point", + testInvalid ".12" "no integer part", + testInvalid "12." "no fractional part", + testInvalid "1.23456" "too many fractional digits", + testInvalid "922337203685477.5808" "overflow", + testInvalid "-922337203685477.5809" "overflow" + ] + +def tests := [testsForValidStrings, testsForInvalidStrings] + +-- Uncomment for interactive debugging +-- #eval TestSuite.runAll tests + +end UnitTest.Decimal \ No newline at end of file diff --git a/cedar-lean/UnitTest/IPAddr.lean b/cedar-lean/UnitTest/IPAddr.lean new file mode 100644 index 000000000..8a747e160 --- /dev/null +++ b/cedar-lean/UnitTest/IPAddr.lean @@ -0,0 +1,166 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec.Ext.IPAddr +import UnitTest.Run + +/-! This file defines unit tests for IPAddr functions. -/ + +namespace UnitTest.IPAddr + +open Cedar.Spec.Ext.IPAddr + +private def ipv4 (a₀ a₁ a₂ a₃ : UInt8) (pre : Nat) : IPNet := + IPNet.V4 (IPv4Addr.mk a₀ a₁ a₂ a₃) (Fin.ofNat pre) + +private def ipv6 (a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : UInt16) (pre : Nat) : IPNet := + IPNet.V6 (IPv6Addr.mk a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇) (Fin.ofNat pre) + +private def testValid (str : String) (ip : IPNet) : TestCase := + test str (checkEq (parse str) ip) + +def testsForValidStrings := + suite "IPAddr.parse for valid strings" + [ + testValid "127.0.0.1" (ipv4 127 0 0 1 V4_SIZE), + testValid "127.3.4.1/2" (ipv4 127 3 4 1 2), + testValid "::" (ipv6 0 0 0 0 0 0 0 0 V6_SIZE), + testValid "::/5" (ipv6 0 0 0 0 0 0 0 0 5), + testValid "a::" (ipv6 0xa 0 0 0 0 0 0 0 V6_SIZE), + testValid "::f" (ipv6 0 0 0 0 0 0 0 0xf V6_SIZE), + testValid "F:AE::F:5:F:F:0" (ipv6 0xf 0xae 0 0xf 0x5 0xf 0xf 0 V6_SIZE), + testValid "a::f/120" (ipv6 0xa 0 0 0 0 0 0 0xf 120) + ] + +private def testInvalid (str : String) (msg : String) : TestCase := + test s!"{str} [{msg}]" (checkEq (parse str) .none) + +def testsForInvalidStrings := + suite "IPAddr.parse for invalid strings" + [ + testInvalid "127.0.0.1." "trailing dot", + testInvalid ".127.0.0.1" "leading dot", + testInvalid "127.0..0.1" "double dot", + testInvalid "256.0.0.1" "group out of range", + testInvalid "127.0.a.1" "no hex in IPv4", + testInvalid "127.3.4.1/33" "prefix out of range", + testInvalid "::::" "too many double colons", + testInvalid "::f::" "too many double colons", + testInvalid "F:AE::F:5:F:F:0:0" "too many groups", + testInvalid "F:A:F:5:F:F:0:0:1" "too many groups", + testInvalid "F:A" "too few groups", + testInvalid "::ffff1" "group out of range", + testInvalid "F:AE::F:5:F:F:0/129" "prefix out of range", + testInvalid "::ffff:127.0.0.1" "no IPv4 embedded in IPv6" + ] + +deriving instance Inhabited for IPNet + +private def parse! (str : String) : IPNet := + match parse str with + | .some ip => ip + | .none => panic! s!"not a valid IP address {str}" + + +private def testIsLoopback (str : String) (expected : Bool) : TestCase := + test s!"isLoopback {str}" (checkEq (parse! str).isLoopback expected) + +private def testToUInt128 (str : String) (expected : UInt128) : TestCase := + test s!"toUInt128 {str}" (checkEq (parse! str).toUInt128 expected) + +def testsForIsLoopback := + suite "IPAddr.isLoopback" + [ + testIsLoopback "127.0.0.1" true, + testIsLoopback "::B" false, + testIsLoopback "::1" true, + -- As in Rust, IPv4 embedded in IPv6 only uses IPv6 loopback: + testIsLoopback "::ffff:ff00:0001" false + ] + +def testsForUInt128Conversion := + suite "IPAddr.toUInt128" + [ + testToUInt128 "192.0.2.235" 3221226219, + testToUInt128 "::1:2" (0x10000 + 0x2) + ] + +def ip! (str : String) : IPNet := + match (ip str) with + | .some ip => ip + | .none => panic! s!"not a valid IP address {str}" + +def testInRange (str₁ str₂ : String) (expected : Bool) : TestCase := + test s!"inRange {str₁} {str₂}" (checkEq ((ip! str₁).inRange (ip! str₂)) expected) + +def testsForInRange := + suite "IPAddr.inRange" + [ + testInRange "238.238.238.238" "238.238.238.41/12" true, + testInRange "238.238.238.238" "238.238.238.238" true, + testInRange "F:AE::F:5:F:F:0" "F:AE::F:5:F:F:0" true, + testInRange "F:AE::F:5:F:F:1" "F:AE::F:5:F:F:0/127" true, + testInRange "F:AE::F:5:F:F:2" "F:AE::F:5:F:F:0/127" false, + testInRange "0.0.0.0" "::" false, + testInRange "::" "0.0.0.0" false, + testInRange "10.0.0.0" "10.0.0.0/24" true, + testInRange "10.0.0.0" "10.0.0.0/32" true, + testInRange "10.0.0.0" "10.0.0.1/24" true, + testInRange "10.0.0.0" "10.0.0.1/32" false, + testInRange "10.0.0.1" "10.0.0.0/24" true, + testInRange "10.0.0.1" "10.0.0.1/24" true, + testInRange "10.0.0.0/24" "10.0.0.0/32" false, + testInRange "10.0.0.0/32" "10.0.0.0/24" true, + testInRange "10.0.0.1/24" "10.0.0.0/24" true, + testInRange "10.0.0.1/24" "10.0.0.1/24" true, + testInRange "10.0.0.0/24" "10.0.0.1/24" true, + testInRange "10.0.0.0/24" "10.0.0.0/29" false, + testInRange "10.0.0.0/29" "10.0.0.0/24" true, + testInRange "10.0.0.0/24" "10.0.0.1/29" false, + testInRange "10.0.0.0/29" "10.0.0.1/24" true, + testInRange "10.0.0.1/24" "10.0.0.0/29" false, + testInRange "10.0.0.1/29" "10.0.0.0/24" true, + testInRange "10.0.0.0/32" "10.0.0.0/32" true, + testInRange "10.0.0.0/32" "10.0.0.0" true + ] + +private def testEq (str₁ str₂ : String) (expected : Bool) : TestCase := + let eq : Bool := (ip! str₁) = (ip! str₂) + test s!"{str₁} == {str₂}" (checkEq eq expected) + +def testsForIpNetEquality := + suite "IpAddr.eq" + [ + testEq "10.0.0.0" "10.0.0.0" true, + testEq "10.0.0.0" "10.0.0.1" false, + testEq "10.0.0.0/32" "10.0.0.0" true, + testEq "10.0.0.0/24" "10.0.0.0" false, + testEq "10.0.0.0/24" "10.0.0.0/24" true, + testEq "10.0.0.0/24" "10.0.0.0/29" false + ] + +def tests := [ + testsForValidStrings, + testsForInvalidStrings, + testsForIsLoopback, + testsForUInt128Conversion, + testsForInRange, + testsForIpNetEquality] + +-- Uncomment for interactive debugging +-- #eval TestSuite.runAll tests + +end UnitTest.IPAddr \ No newline at end of file diff --git a/cedar-lean/UnitTest/Main.lean b/cedar-lean/UnitTest/Main.lean new file mode 100644 index 000000000..cd6b2f686 --- /dev/null +++ b/cedar-lean/UnitTest/Main.lean @@ -0,0 +1,23 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import UnitTest.Decimal +import UnitTest.IPAddr + +open UnitTest + +def main : IO Unit := do + TestSuite.runAll (Decimal.tests ++ IPAddr.tests) diff --git a/cedar-lean/UnitTest/Run.lean b/cedar-lean/UnitTest/Run.lean new file mode 100644 index 000000000..7920c070f --- /dev/null +++ b/cedar-lean/UnitTest/Run.lean @@ -0,0 +1,82 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Std + +/-! This file defines simple utilities for unit testing. -/ + +namespace UnitTest + +def pass : IO Bool := pure true + +def fail (name : String) (message : String) : IO Bool := do + IO.println "--------------------" + IO.println s!"FAILED: {name}" + IO.println message + IO.println "--------------------" + pure false + +def checkEq {α} [DecidableEq α] [Repr α] (actual expected : α) (name : String) : IO Bool := + if actual = expected + then pass + else fail name s!"actual: {reprArg actual}\nexpected: {reprArg expected}" + +structure TestCase where + name : String + exec : String → IO Bool + +structure TestSuite where + name : String + tests : List TestCase + +def test (name : String) (exec : String → IO Bool) : TestCase := + TestCase.mk name exec + +def suite (name : String) (tests : List TestCase) : TestSuite := + TestSuite.mk name tests + +/-- +Runs the test case and returns true if the tests passes. +Otherwise prints the error message and returns false. +-/ +def TestCase.run (case : TestCase) : IO Bool := case.exec case.name + +/-- +Runs the test suite, prints the stats, and returns the number of +failed test cases. +-/ +def TestSuite.run (suite : TestSuite) : IO Nat := do + IO.println "====================" + IO.println s!"Running {suite.name}" + let outcomes ← suite.tests.mapM TestCase.run + let total := outcomes.length + let successes := outcomes.count true + let failures := total - successes + IO.println s!"{successes} success(es) {failures} failure(s) {total} test(s) run" + pure failures + +/-- +Runs all the given test suites and prints the stats. +-/ +def TestSuite.runAll (suites : List TestSuite) : IO Unit := do + let outcomes ← suites.mapM TestSuite.run + let total := suites.foldl (fun n ts => n + ts.tests.length) 0 + let failures := outcomes.foldl (· + ·) 0 + let successes := total - failures + IO.println "====== TOTAL =======" + IO.println s!"{successes} success(es) {failures} failure(s) {total} test(s) run" + +end UnitTest \ No newline at end of file diff --git a/cedar-lean/lake-manifest.json b/cedar-lean/lake-manifest.json new file mode 100644 index 000000000..5edde18eb --- /dev/null +++ b/cedar-lean/lake-manifest.json @@ -0,0 +1,52 @@ +{"version": 6, + "packagesDir": "lake-packages", + "packages": + [{"git": + {"url": "https://github.com/leanprover-community/mathlib4", + "subDir?": null, + "rev": "b8e9a283b47b6bf9126508810ab00dd7b36b2c83", + "opts": {}, + "name": "mathlib", + "inputRev?": null, + "inherited": false}}, + {"git": + {"url": "https://github.com/leanprover/std4", + "subDir?": null, + "rev": "dd2549f76ff763c897fe997061e2625a7d628eaf", + "opts": {}, + "name": "std", + "inputRev?": "main", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover-community/quote4", + "subDir?": null, + "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2", + "opts": {}, + "name": "Qq", + "inputRev?": "master", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover-community/aesop", + "subDir?": null, + "rev": "b601328752091a1cfcaebdd6b6b7c30dc5ffd946", + "opts": {}, + "name": "aesop", + "inputRev?": "master", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover/lean4-cli", + "subDir?": null, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "opts": {}, + "name": "Cli", + "inputRev?": "nightly", + "inherited": true}}, + {"git": + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "subDir?": null, + "rev": "27715d1daf32b9657dc38cd52172d77b19bde4ba", + "opts": {}, + "name": "proofwidgets", + "inputRev?": "v0.0.18", + "inherited": true}}], + "name": "Cedar"} diff --git a/cedar-lean/lakefile.lean b/cedar-lean/lakefile.lean new file mode 100644 index 000000000..2e0eb5134 --- /dev/null +++ b/cedar-lean/lakefile.lean @@ -0,0 +1,32 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Lake +open Lake DSL + +require mathlib from git + "https://github.com/leanprover-community/mathlib4" + +package Cedar + +lean_lib Cedar where + defaultFacets := #[LeanLib.staticFacet] + +lean_lib UnitTest where + defaultFacets := #[LeanLib.staticFacet] + +lean_exe CedarUnitTests where + root := `UnitTest.Main \ No newline at end of file diff --git a/cedar-lean/lean-toolchain b/cedar-lean/lean-toolchain new file mode 100644 index 000000000..a61d28285 --- /dev/null +++ b/cedar-lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.2.0-rc3