better again

Signed-off-by: Shaobo He <shaobohe@amazon.com>

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

@@ -20,6 +20,7 @@ import Cedar.Thm.Data.List
 import Cedar.Thm.Data.Set
 import Cedar.Thm.Data.Map
 import Cedar.Thm.Data.LT
+import Cedar.Data.SizeOf
 
 /-!
 This file contains useful lemmas about the `Evaluator` functions.
@@ -208,7 +209,7 @@ inductive Value.WellFormed : Value -> Prop
     (h₂ : s.WellFormed) :
     Value.WellFormed (.set s)
   | record_wf (m : Map Attr Value)
-    (h₁ : ∀ t, t ∈ m.values → Value.WellFormed t)
+    (h₁ : ∀ t, (a, t) ∈ m.kvs → Value.WellFormed t)
     (h₂ : m.WellFormed):
     Value.WellFormed (.record m)
 
@@ -221,21 +222,42 @@ theorem evaluate_value_roundtrip (v : Value) {req : Request} {es : Entities} :
   case set =>
     simp only [Value.toExpr, evaluate]
     rename_i s
-    rw [List.mapM₁_eq_mapM (fun x => evaluate x req es) (s.elts.map₁ fun x => Value.toExpr x.val)]
-    simp only [List.map₁_eq_map]
-    simp only [List.mapM_map_eq_mapM Value.toExpr (fun x => evaluate x req es) s.elts]
-    sorry
-    --simp only [evaluate_value_roundtrip]
-    --rw [List.mapM_all_ok s.elts]
-    --simp
-    -- last step: Set.make s.elts = s
-    -- which is true and unprovable at this moment
-    --sorry
+    cases h with
+    | set_wf _ hₐ hₛ =>
+    have h₁ : ∀ (x : { x : Value // x ∈ s.elts }),
+      evaluate (Value.toExpr x.val) req es = Except.ok x.val := by
+      intro x
+      have hₜ : sizeOf x.val < 1 + sizeOf s := by
+        have := Set.sizeOf_lt_of_mem x.property
+        omega
+      exact evaluate_value_roundtrip x.val (hₐ x.val x.property)
+    have h₂ : ((s.elts.map₁ fun x => Value.toExpr x.val).mapM₁ fun x => evaluate x.val req es)
+             = Except.ok s.elts := by
+      apply List.map₁_mapM₁_chain s.elts Value.toExpr (λ x => evaluate x req es)
+      intro x
+      exact h₁ x
+    rw [h₂]
+    simp
+    simp only [Set.WellFormed, Set.toList] at hₛ
+    symm
+    exact hₛ
   case record =>
-    simp only [Value.toExpr, evaluate]
+    simp only [Value.toExpr, evaluate, bindAttr]
+    rename_i m
+    cases h with
+    | record_wf _ hₐ hₘ =>
+    have h₁ : ∀ (x : { x // x ∈ m.kvs.attach₂ }),
+      evaluate (Value.toExpr x.val.1.snd) req es = Except.ok x.val.1.snd := by
+      intro x
+      rename_i a
+      have hᵢₙ : (a, x.val.val.snd) ∈ m.kvs := by
+        sorry
+      have hₜ : sizeOf x.val.val.snd < 1 + sizeOf m := by
+        have := x.val.property
+        have := Map.sizeOf_lt_of_kvs m
+        omega
+      exact evaluate_value_roundtrip x.val.1.snd (hₐ x.val.1.snd hᵢₙ)
     sorry
-decreasing_by
-  all_goals simp_wf
-  sorry
+termination_by sizeOf v
 
 end Cedar.Thm

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

@@ -113,7 +113,6 @@ theorem map₁_eq_map (f : α → β) (as : List α) :
 := by
   simp only [map₁, attach_def, map_pmap_subtype]
 
-
 theorem map_attach₂ {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {xs : List (α × β)} (f : (α × β) → γ) :
   xs.attach₂.map (λ x : { x : α × β // sizeOf x.snd < 1 + sizeOf xs } => f x.1) =
   xs.map f
@@ -386,6 +385,28 @@ theorem mapM₁_eq_mapM [Monad m] [LawfulMonad m]
 := by
   simp [mapM₁, attach_def, mapM_pmap_subtype]
 
+theorem map₁_mapM₁_chain {α β : Type} (xs : List α)
+  (f : α → β) (g : β → Except δ α)
+  (h : ∀ x : { x // x ∈ xs }, g (f x.val) = Except.ok x) :
+  ((xs.map₁ λ x => f x.val).mapM₁ λ x => g x.val) = Except.ok xs :=
+by
+  rw [mapM₁_eq_mapM, map₁_eq_map]
+  induction xs with
+  | nil =>
+    simp
+    rfl
+  | cons x xs h₁ =>
+    simp at h₁
+    simp
+    have hₓ : g (f x) = Except.ok x := by
+      apply h ⟨ x, List.mem_cons_self x xs⟩
+    rw [hₓ]
+    simp
+    have hₓₛ : ∀ x, x ∈ xs → g (f x) = Except.ok x :=
+      fun a as => h ⟨a, List.mem_cons_of_mem x as⟩
+    rw [h₁ hₓₛ]
+    simp
+
 theorem mapM₂_eq_mapM [Monad m] [LawfulMonad m]
   (f : (α × β) → m γ)
   (as : List (α × β)) :