Make Map.kvs private and Map.toList opaque (#880)

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>

Author: cdisselkoen

cedar-lean/Cedar/Data/Map.lean

@@ -37,7 +37,7 @@ deriving Repr, DecidableEq, Inhabited
 
 namespace Map
 
-public abbrev kvs  {α : Type u} {β : Type v} (m : Map α β) := m.1
+private abbrev kvs {α : Type u} {β : Type v} (m : Map α β) := m.1
 
 ----- Definitions -----
 
@@ -51,18 +51,17 @@ public def empty {α β} : Map α β := .mk []
 /-- Returns an ordered and duplicate free list provided the given map is well-formed. -/
 public def toList {α : Type u} {β : Type v} (m : Map α β) : List (Prod α β) := m.kvs
 
-
 /-- Returns the keys of `m` as a set. -/
 public def keys {α β} (m : Map α β) : Set α :=
-  Set.mk (m.kvs.map Prod.fst) -- well-formed by construction
+  Set.mk (m.toList.map Prod.fst) -- well-formed by construction
 
 /-- Returns the values of `m` as a list. -/
 public def values {α β} (m : Map α β) : List β :=
-  m.kvs.map Prod.snd
+  m.toList.map Prod.snd
 
 /-- Returns the binding for `k` in `m`, if any. -/
 public def find? {α β} [BEq α] (m : Map α β) (k : α) : Option β :=
-  match m.kvs.find? (λ ⟨k', _⟩ => k' == k) with
+  match m.toList.find? (λ ⟨k', _⟩ => k' == k) with
   | some (_, v) => some v
   | _           => none
 
@@ -84,23 +83,26 @@ public def find! {α β} [Repr α] [BEq α] [Inhabited β] (m : Map α β) (k :
 
 /-- Filters `m` using `f`. -/
 public def filter {α β} (f : α → β → Bool) (m : Map α β) : Map α β :=
-  Map.mk (m.kvs.filter (λ ⟨k, v⟩ => f k v))
+  Map.mk (m.toList.filter (λ ⟨k, v⟩ => f k v))
 
 public def size {α β} (m : Map α β) : Nat :=
-  m.kvs.length
+  m.toList.length
 
 public def mapOnValues {α β γ} (f : β → γ) (m : Map α β) : Map α γ :=
-  Map.mk (m.kvs.map (λ (k, v) => (k, f v)))
+  Map.mk (m.toList.map (λ (k, v) => (k, f v)))
+
+public def mapOnValues₃ {α β γ} (f : β → γ) (m : Map α β) : Map α γ :=
+  Map.mk (m.toList.map₃ (λ ⟨(k, v), _⟩ => (k, f v)))
 
 public def mapOnKeys {α β γ} [LT γ] [DecidableLT γ] (f : α → γ) (m : Map α β) : Map γ β :=
-  Map.make (m.kvs.map (λ (k, v) => (f k, v)))
+  Map.make (m.toList.map (λ (k, v) => (f k, v)))
 
 public def mapMOnValues {α β γ} [LT α] [DecidableLT α] [Monad m] (f : β → m γ) (map : Map α β) : m (Map α γ) := do
-  let kvs ← map.kvs.mapM (λ (k, v) => f v >>= λ v' => pure (k, v'))
+  let kvs ← map.toList.mapM (λ (k, v) => f v >>= λ v' => pure (k, v'))
   pure (Map.mk kvs)
 
 public def mapMOnKeys {α β γ} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) (map : Map α β) : m (Map γ β) := do
-  let kvs ← map.kvs.mapM (λ (k, v) => f k >>= λ k' => pure (k', v))
+  let kvs ← map.toList.mapM (λ (k, v) => f k >>= λ k' => pure (k', v))
   pure (Map.make kvs)
 
 public def wellFormed {α β} [LT α] [DecidableLT α] (m : Map α β) : Bool :=
@@ -109,17 +111,17 @@ public def wellFormed {α β} [LT α] [DecidableLT α] (m : Map α β) : Bool :=
 ----- Instances -----
 
 public instance [LT (Prod α β)] : LT (Map α β) where
-  lt a b := a.kvs < b.kvs
+  lt a b := a.1 < b.1
 
 public instance decLt [LT (Prod α β)] [DecidableEq (Prod α β)] [DecidableLT (Prod α β)] : (n m : Map α β) → Decidable (n < m)
   | .mk nkvs, .mk mkvs => List.decidableLT nkvs mkvs
 
 -- enables ∈ notation for map keys
 public instance : Membership α (Map α β) where
-  mem m a := List.Mem a (m.kvs.map Prod.fst)
+  mem m a := List.Mem a (m.toList.map Prod.fst)
 
 public instance [LT α] [DecidableLT α] : HAppend (Map α β) (Map α β) (Map α β) where
-  hAppend a b := Map.make (a.kvs ++ b.kvs)
+  hAppend a b := Map.make (a.toList ++ b.toList)
 
 end Map
 

cedar-lean/Cedar/Data/SizeOf.lean

@@ -17,6 +17,7 @@
 module
 
 public import Cedar.Data.Map
+import all Cedar.Data.Map -- allow accessing internals of Cedar.Data.Map, necessary for sizeOf calculations
 public import Cedar.Data.Set
 
 /-!
@@ -44,21 +45,21 @@ public theorem sizeOf_lt_of_value [SizeOf α] [SizeOf β] {m : Map α β} {k : 
     omega
   omega
 
-public theorem sizeOf_lt_of_kvs [SizeOf α] [SizeOf β] (m : Map α β) :
-  sizeOf m.kvs < sizeOf m
+public theorem sizeOf_lt_of_toList [SizeOf α] [SizeOf β] (m : Map α β) :
+  sizeOf m.toList < sizeOf m
 := by
-  unfold kvs
+  unfold toList kvs
   conv => rhs ; unfold sizeOf _sizeOf_inst _sizeOf_1 ; simp only
   generalize sizeOf m.1 = s
   omega
 
 public theorem sizeOf_lt_of_tl [SizeOf α] [SizeOf β] {m : Map α β} {tl : List (α × β)}
-  (h : m.kvs = (k, v) :: tl) :
+  (h : m.toList = (k, v) :: tl) :
   1 + sizeOf tl < sizeOf m
 := by
   conv => rhs ; unfold sizeOf _sizeOf_inst _sizeOf_1
   simp only
-  unfold kvs at h
+  unfold toList at h
   simp only [h, List.cons.sizeOf_spec, Prod.mk.sizeOf_spec]
   omega
 

cedar-lean/Cedar/SymCC/Concretizer.lean

@@ -39,7 +39,7 @@ def Prim.entityUIDs : Prim → Set EntityUID
 def Value.entityUIDs : Value → Set EntityUID
   | .prim p              => p.entityUIDs
   | .set (Set.mk vs)     => vs.mapUnion₁ (λ ⟨v, _⟩ => v.entityUIDs)
-  | .record (Map.mk avs) => avs.mapUnion₃ (λ ⟨(_, v), _⟩ => v.entityUIDs)
+  | .record avs          => avs.toList.mapUnion₃ (λ ⟨(_, v), _⟩ => v.entityUIDs)
   | .ext _               => Set.empty
 
 def Value.entityUID? : Value → Option EntityUID
@@ -60,7 +60,7 @@ def EntityData.entityUIDs (d : EntityData) : Set EntityUID :=
   d.ancestors ∪ (Value.record d.attrs).entityUIDs ∪ (Value.record d.tags).entityUIDs
 
 def Entities.entityUIDs (es : Entities) : Set EntityUID :=
-  es.kvs.mapUnion (λ (uid, d) => (Set.singleton uid) ∪ d.entityUIDs)
+  es.toList.mapUnion (λ (uid, d) => (Set.singleton uid) ∪ d.entityUIDs)
 
 structure Env where
   request : Request
@@ -171,7 +171,7 @@ def SymRequest.entityUIDs (ρ : SymRequest) : Set EntityUID :=
 
 def UDF.entityUIDs (f : UDF) : Set EntityUID :=
   f.default.entityUIDs ∪
-  f.table.kvs.mapUnion (λ (tᵢ, tₒ) => tᵢ.entityUIDs ∪ tₒ.entityUIDs)
+  f.table.toList.mapUnion (λ (tᵢ, tₒ) => tᵢ.entityUIDs ∪ tₒ.entityUIDs)
 
 def UnaryFunction.entityUIDs : UnaryFunction → Set EntityUID
   | .uuf _ => Set.empty
@@ -184,13 +184,13 @@ where
     | .none      => Set.empty
     | .some eids => Set.make (eids.elts.map (EntityUID.mk ety))
   attrs := δ.attrs.entityUIDs
-  ancs  := δ.ancestors.kvs.mapUnion (λ (_, f) => f.entityUIDs)
+  ancs  := δ.ancestors.toList.mapUnion (λ (_, f) => f.entityUIDs)
   tags  := match δ.tags with
     | .none      => Set.empty
     | .some τs   => τs.vals.entityUIDs
 
 def SymEntities.entityUIDs (εs : SymEntities) : Set EntityUID :=
-  εs.kvs.mapUnion λ (ety, δ) => δ.entityUIDs ety
+  εs.toList.mapUnion λ (ety, δ) => δ.entityUIDs ety
 
 def SymEnv.entityUIDs (εnv : SymEnv) : Set EntityUID :=
   εnv.request.entityUIDs ∪ εnv.entities.entityUIDs
@@ -206,7 +206,7 @@ def SymRequest.concretize? (ρ : SymRequest) : Option Request := do
 def SymEntityData.concretize? (uid : EntityUID) (δ : SymEntityData) : Option EntityData := do
   let tuid  ← if isValidEntityUID then .some (Term.entity uid) else .none
   let attrs ← (app δ.attrs tuid).recordValue?
-  let ancs  ← δ.ancestors.kvs.mapM (λ (_, f) => (app f tuid).setOfEntityUIDs?)
+  let ancs  ← δ.ancestors.toList.mapM (λ (_, f) => (app f tuid).setOfEntityUIDs?)
   .some ⟨attrs, ancs.mapUnion id, ← (tags tuid)⟩
   where
     isValidEntityUID :=

cedar-lean/Cedar/SymCC/Enforcer.lean

@@ -123,7 +123,7 @@ where
     | .some f₁₃ => set.subset (app f₂₃ t₂') (app f₁₃ t₁') -- f₂₃ t₂' ⊆ f₁₃ t₁'
     | .none     => set.isEmpty (app f₂₃ t₂')              -- f₁₃ t₁' = ∅
   areAncestors t₂' (anc₂ : Map EntityType UnaryFunction) t₁' ety₁ :=
-    anc₂.kvs.foldl (λ acc ⟨ety₃, f₂₃⟩ => and acc (areAncestorsOfType t₂' f₂₃ ety₃ t₁' ety₁)) (.prim (.bool true))
+    anc₂.toList.foldl (λ acc ⟨ety₃, f₂₃⟩ => and acc (areAncestorsOfType t₂' f₂₃ ety₃ t₁' ety₁)) (.prim (.bool true))
 
 /--
 Returns the ground acyclicity and transitivity assumptions for xs and env.

cedar-lean/Cedar/SymCC/Extractor.lean

@@ -50,10 +50,10 @@ def UnaryFunction.uuf? : UnaryFunction → Option UUF
   | _      => .none
 
 def SymEntityData.uufAncestors (δ : SymEntityData) : Set UUF :=
-  Set.make (δ.ancestors.kvs.filterMap (UnaryFunction.uuf? ∘ Prod.snd))
+  Set.make (δ.ancestors.toList.filterMap (UnaryFunction.uuf? ∘ Prod.snd))
 
 def SymEntities.uufAncestors (εs : SymEntities) : Set UUF :=
-  εs.kvs.mapUnion (SymEntityData.uufAncestors ∘ Prod.snd)
+  εs.toList.mapUnion (SymEntityData.uufAncestors ∘ Prod.snd)
 
 def UUF.repairAncestors (fts : Set EntityUID) (I : Interpretation) (f : UUF) : UDF :=
   let udf := I.funs f

cedar-lean/Cedar/SymCC/Symbolizer.lean

@@ -70,7 +70,7 @@ where
       have := Map.find?_mem_toList _h
       have := List.sizeOf_lt_of_mem this
       cases rec
-      simp [Map.toList, Map.kvs] at this ⊢
+      simp at this ⊢
       omega
 
 /--

cedar-lean/Cedar/TPE/Input.lean

@@ -150,7 +150,7 @@ where
       else
         .error .entitiesDoNotMatch
   entitiesMatch :=
-      es₂.kvs.all λ (a₂, e₂) => match es₁.find? a₂ with
+      es₂.toList.all λ (a₂, e₂) => match es₁.find? a₂ with
         | .some e₁ =>
           let ⟨attrs₁, ancestors₁, tags₁⟩ := e₁
           partialIsValid e₂.attrs (· = attrs₁) &&

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

@@ -17,6 +17,7 @@
 import Cedar.Spec
 import Cedar.Thm.Data.Control
 import Cedar.Thm.Data.List
+import Cedar.Thm.Data.Map
 
 /-!
 This file contains useful lemmas about the `Evaluator` functions.
@@ -240,6 +241,7 @@ theorem record_value_contains_evaluated_attrs {rxs : List (Attr × Expr)} {rvs :
   simp only [evaluate] at he
   cases he₁ : rxs.mapM₂ fun x => bindAttr x.1.fst (evaluate x.1.snd request entities) <;>
     simp only [he₁, Except.bind_err, reduceCtorEq, Except.bind_ok, Except.ok.injEq, Value.record.injEq] at he
+  subst rvs
   rename_i rvs'
   replace he₁ : List.Forallᵥ (λ x y => evaluate x request entities = Except.ok y) rxs rvs' := by
     simp only [List.forallᵥ_def]
@@ -257,11 +259,11 @@ theorem record_value_contains_evaluated_attrs {rxs : List (Attr × Expr)} {rvs :
     split at hfv <;> simp only [Option.some.injEq, reduceCtorEq] at hfv
     subst hfv
     rename_i a' _ hfv
-    rw [←he, (by simpa using List.find?_some hfv : a' = a)] at hfv
+    rw [(by simpa using List.find?_some hfv : a' = a)] at hfv
     exact hfv
-  have ⟨(_, x), he₂, he₃, he₄⟩ := List.forall₂_implies_all_right he₁ (a, av) (List.mem_of_find?_eq_some hfv)
+  have ⟨(a', x), he₂, he₃, he₄⟩ := List.forall₂_implies_all_right he₁ (a, av) (List.mem_of_find?_eq_some hfv)
   subst he₃
   exists x
-  simp only [List.mem_of_sortedBy_implies_find? he₂ (List.canonicalize_sortedBy _ _), he₄, Map.make, Map.find?, and_self]
+  simp [List.mem_of_sortedBy_implies_find? he₂ (List.canonicalize_sortedBy _ _), he₄, Map.make, Map.find?, and_self]
 
 end Cedar.Thm

cedar-lean/Cedar/Thm/BatchedEvaluator.lean

@@ -47,7 +47,7 @@ theorem as_partial_request_refines {req : Request} :
 
 theorem any_refines_empty_entities :
   EntitiesRefine es Data.Map.empty := by
-  simp only [EntitiesRefine, Data.Map.empty, Data.Map.find?, Map.kvs]
+  simp only [EntitiesRefine, Data.Map.empty, Data.Map.find?, Map.toList]
   intro a e₂ h₁
   contradiction
 

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

@@ -560,7 +560,6 @@ public theorem isSorted_correct {α} [LT α] [DecidableLT α] {l : List α} :
 
 /-! ### Forallᵥ -/
 
-@[expose]
 public def Forallᵥ {α β γ} (p : β → γ → Prop) (kvs₁ : List (α × β)) (kvs₂ : List (α × γ)) : Prop :=
   List.Forall₂ (λ kv₁ kv₂ => kv₁.fst = kv₂.fst ∧ p kv₁.snd kv₂.snd) kvs₁ kvs₂