use Lean modules in more files

cedar-lean/Cedar/Data/Int64.lean

@@ -32,6 +32,7 @@ public def MAX : Int :=  9223372036854775807
 
 ----- Definitions -----
 
+@[expose]
 public def ofIntChecked (i : Int) (_ : MIN ≤ i ∧ i ≤ MAX) : Int64 :=
   Int64.ofInt i
 
@@ -41,20 +42,15 @@ public def ofInt? (i : Int) : Option Int64 :=
   else .none
 
 /-- We don't @[expose] the definition of `ofInt?`; but callers can use this
-theorem, which partially specifies its behavior -/
+theorem, which specifies its behavior -/
 public theorem ofInt?_some_iff {i : Int} :
-  MIN ≤ i ∧ i ≤ MAX ↔ (ofInt? i).isSome
-:= by simp [ofInt?]
+  MIN ≤ i ∧ i ≤ MAX ↔ (ofInt? i) = some (Int64.ofInt i)
+:= by simp [ofInt?, ofIntChecked]
 
-/-- Corollary of the above -/
+/-- Inverse of the above -/
 public theorem ofInt?_none_iff {i : Int} :
   i < MIN ∨ i > MAX ↔ (ofInt? i) = none
-:= by
-  have h := ofInt?_some_iff (i := i)
-  simp_all only [Option.isSome, gt_iff_lt]
-  split at h
-  · simp_all
-  · by_cases i < MIN <;> simp_all
+:= by grind [ofInt?, ofIntChecked]
 
 public def add? (i₁ i₂ : Int64) : Option Int64 := ofInt? (i₁.toInt + i₂.toInt)
 

cedar-lean/Cedar/Spec/Entities.lean

@@ -37,28 +37,34 @@ public structure EntityData where
 
 public abbrev Entities := Map EntityUID EntityData
 
+@[expose]
 public def Entities.ancestors (es : Entities) (uid : EntityUID) : Result (Set EntityUID) := do
   let d ← es.findOrErr uid .entityDoesNotExist
   .ok d.ancestors
 
+@[expose]
 public def Entities.ancestorsOrEmpty (es : Entities) (uid : EntityUID) : Set EntityUID :=
   match es.find? uid with
   | some d => d.ancestors
   | none   => Set.empty
 
+@[expose]
 public def Entities.attrs (es : Entities) (uid : EntityUID) : Result (Map Attr Value) := do
   let d ← es.findOrErr uid .entityDoesNotExist
   .ok d.attrs
 
+@[expose]
 public def Entities.attrsOrEmpty (es : Entities) (uid : EntityUID) : Map Attr Value :=
   match es.find? uid with
   | some d => d.attrs
   | none   => Map.empty
 
+@[expose]
 public def Entities.tags (es : Entities) (uid : EntityUID) : Result (Map Tag Value) := do
   let d ← es.findOrErr uid .entityDoesNotExist
   .ok d.tags
 
+@[expose]
 public def Entities.tagsOrEmpty (es : Entities) (uid : EntityUID) : Map Tag Value :=
   match es.find? uid with
   | some d => d.tags

cedar-lean/Cedar/Spec/ExtFun.lean

@@ -56,6 +56,7 @@ public def res {α} [Coe α Ext] : Option α → Result Value
   | some v => .ok v
   | none   => .error .extensionError
 
+@[expose]
 public def call : ExtFun → List Value → Result Value
   | .decimal, [.prim (.string s)]               => res (Decimal.decimal s)
   | .lessThan,

cedar-lean/Cedar/SymCC/Compiler.lean

@@ -82,14 +82,16 @@ def reducibleEq (ty₁ ty₂ : TermType) : Result Bool :=
   else .error .typeError
 
 def compileInₑ (t₁ t₂ : Term) (ancs? : Option UnaryFunction) : Term :=
-  let isEq := if t₁.typeOf = t₂.typeOf then eq t₁ t₂ else false
-  let isIn := if let some ancs := ancs? then set.member t₂ (app ancs t₁) else false
   or isEq isIn
+  where
+    isEq := if t₁.typeOf = t₂.typeOf then eq t₁ t₂ else false
+    isIn := if let some ancs := ancs? then set.member t₂ (app ancs t₁) else false
 
 def compileInₛ (t ts : Term) (ancs? : Option UnaryFunction) : Term :=
-  let isIn₁ := if ts.typeOf = .set t.typeOf then set.member t ts else false
-  let isIn₂ := if let some ancs := ancs? then set.intersects ts (app ancs t) else false
   or isIn₁ isIn₂
+  where
+    isIn₁ := if ts.typeOf = .set t.typeOf then set.member t ts else false
+    isIn₂ := if let some ancs := ancs? then set.intersects ts (app ancs t) else false
 
 def compileHasTag (entity tag : Term) : Option (Option SymTags) → Result Term
   | .none            => .error .noSuchEntityType

cedar-lean/Cedar/SymCC/ExtFun.lean

@@ -47,27 +47,27 @@ open Factory Batteries
 
 namespace Decimal
 
-def lessThan (t₁ t₂ : Term) : Term :=
+public def lessThan (t₁ t₂ : Term) : Term :=
   bvslt (ext.decimal.val t₁) (ext.decimal.val t₂)
 
-def lessThanOrEqual (t₁ t₂ : Term) : Term :=
+public def lessThanOrEqual (t₁ t₂ : Term) : Term :=
   bvsle (ext.decimal.val t₁) (ext.decimal.val t₂)
 
-def greaterThan (t₁ t₂ : Term) : Term :=
+public def greaterThan (t₁ t₂ : Term) : Term :=
   lessThan t₂ t₁
 
-def greaterThanOrEqual (t₁ t₂ : Term) : Term :=
+public def greaterThanOrEqual (t₁ t₂ : Term) : Term :=
   lessThanOrEqual t₂ t₁
 
 end Decimal
 
 namespace IPAddr
 open BitVec
 
-def isIpv4 (t : Term) : Term :=
+public def isIpv4 (t : Term) : Term :=
   ext.ipaddr.isV4 t
 
-def isIpv6 (t : Term) : Term :=
+public def isIpv6 (t : Term) : Term :=
   not (ext.ipaddr.isV4 t)
 
 def subnetWidth (w : Nat) (ipPre : Term) : Term :=
@@ -100,7 +100,7 @@ def inRangeV (isIp : Term → Term) (range : Term → Term × Term) (t₁ t₂ :
     (and (isIp t₁) (isIp t₂))
     (inRange range t₁ t₂))
 
-def isInRange (t₁ t₂ : Term) : Term :=
+public def isInRange (t₁ t₂ : Term) : Term :=
   (or
     (inRangeV isIpv4 rangeV4 t₁ t₂)
     (inRangeV isIpv6 rangeV6 t₁ t₂))
@@ -113,45 +113,45 @@ def inRangeLit (t : Term) (cidr₄ : Ext.IPAddr.CIDR Ext.IPAddr.V4_WIDTH) (cidr
     (inRange rangeV4 t (ipTerm (Ext.IPAddr.IPNet.V4 cidr₄)))
     (inRange rangeV6 t (ipTerm (Ext.IPAddr.IPNet.V6 cidr₆))))
 
-def isLoopback (t : Term) : Term :=
+public def isLoopback (t : Term) : Term :=
   inRangeLit t Ext.IPAddr.LOOP_BACK_CIDR_V4 Ext.IPAddr.LOOP_BACK_CIDR_V6
 
- def isMulticast (t : Term) : Term :=
+public def isMulticast (t : Term) : Term :=
   inRangeLit t Ext.IPAddr.MULTICAST_CIDR_V4 Ext.IPAddr.MULTICAST_CIDR_V6
 
 end IPAddr
 
 namespace Duration
 
-def toMilliseconds (t : Term) : Term := ext.duration.val t
+public def toMilliseconds (t : Term) : Term := ext.duration.val t
 
-def toSeconds (t : Term) : Term :=
+public def toSeconds (t : Term) : Term :=
   bvsdiv (toMilliseconds t) (.prim (.bitvec (Int64.toBitVec 1000)))
 
-def toMinutes (t : Term) : Term :=
+public def toMinutes (t : Term) : Term :=
   bvsdiv (toSeconds t) (.prim (.bitvec (Int64.toBitVec 60)))
 
-def toHours (t : Term) : Term :=
+public def toHours (t : Term) : Term :=
   bvsdiv (toMinutes t) (.prim (.bitvec (Int64.toBitVec 60)))
 
-def toDays (t : Term) : Term :=
+public def toDays (t : Term) : Term :=
   bvsdiv (toHours t) (.prim (.bitvec (Int64.toBitVec 24)))
 
 end Duration
 
 namespace Datetime
 
-def offset (dt dur : Term) : Term :=
+public def offset (dt dur : Term) : Term :=
   let dt_val := ext.datetime.val dt
   let dur_val := ext.duration.val dur
   ifFalse (bvsaddo dt_val dur_val) (ext.datetime.ofBitVec (bvadd dt_val dur_val))
 
-def durationSince (dt₁ dt₂ : Term) : Term :=
+public def durationSince (dt₁ dt₂ : Term) : Term :=
   let dt₁_val := ext.datetime.val dt₁
   let dt₂_val := ext.datetime.val dt₂
   ifFalse (bvssubo dt₁_val dt₂_val) (ext.duration.ofBitVec (bvsub dt₁_val dt₂_val))
 
-def toDate (dt : Term) : Term :=
+public def toDate (dt : Term) : Term :=
   let zero := .prim (.bitvec (Int64.toBitVec 0))
   let one := .prim (.bitvec (Int64.toBitVec 1))
   let ms_per_day := .prim (.bitvec (Int64.toBitVec 86400000))
@@ -166,7 +166,7 @@ def toDate (dt : Term) : Term :=
     )
   )
 
-def toTime (dt : Term) : Term :=
+public def toTime (dt : Term) : Term :=
   let zero := .prim (.bitvec (Int64.toBitVec 0))
   let ms_per_day := .prim (.bitvec (Int64.toBitVec 86400000))
   let dt_val := ext.datetime.val dt

cedar-lean/Cedar/SymCC/Factory.lean

@@ -47,8 +47,10 @@ namespace Factory
 
 ---------- Term constructors ----------
 
+@[inline, expose]
 public def noneOf (ty : TermType) : Term := .none ty
 
+@[inline, expose]
 public def someOf (t : Term) : Term := .some t
 prefix:0 "⊙" => someOf
 

cedar-lean/Cedar/SymCC/Function.lean

@@ -59,12 +59,12 @@ public def UnaryFunction.outType : UnaryFunction → TermType
   | .uuf f => f.out
   | .udf f => f.out
 
-@[inline]
+@[inline, expose]
 public def UnaryFunction.isUUF : UnaryFunction → Bool
   | .uuf _ => true
   | .udf _ => false
 
-@[inline]
+@[inline, expose]
 public def UnaryFunction.isUDF : UnaryFunction → Bool
   | .udf _ => true
   | .uuf _ => false
@@ -73,6 +73,7 @@ public def UDF.isLiteral (f : UDF) : Bool :=
   f.default.isLiteral &&
   f.table.toList.all λ (tᵢ, tₒ) => tᵢ.isLiteral && tₒ.isLiteral
 
+@[inline, expose]
 public def UnaryFunction.isLiteral : UnaryFunction → Bool
   | .udf f => f.isLiteral
   | .uuf _ => false

cedar-lean/Cedar/SymCC/Interpretation.lean

@@ -164,6 +164,7 @@ decreasing_by
     omega
   · omega
 
+@[expose]
 public def SymRequest.interpret (I : Interpretation) (req : SymRequest)  : SymRequest :=
   {
     principal := req.principal.interpret I,
@@ -189,6 +190,7 @@ public def SymEntityData.interpret (I : Interpretation) (d : SymEntityData) : Sy
 public def SymEntities.interpret (I : Interpretation) (es : SymEntities)  : SymEntities :=
   es.mapOnValues (SymEntityData.interpret I)
 
+@[expose]
 public def SymEnv.interpret (I : Interpretation) (env : SymEnv) : SymEnv :=
   ⟨env.request.interpret I, env.entities.interpret I⟩
 

cedar-lean/Cedar/SymCC/TermType.lean

@@ -54,32 +54,32 @@ public abbrev TermType.ext (xty : ExtType) : TermType := .prim (.ext xty)
 public abbrev TermType.tagFor (ety : EntityType) : TermType :=
   .record (EntityTag.mk (.entity ety) .string)
 
-@[inline]
+@[inline, expose]
 public def TermType.isPrimType : TermType → Bool
   | .prim _ => true
   | _       => false
 
-@[inline]
+@[inline, expose]
 public def TermType.isEntityType : TermType → Bool
   | .prim (.entity _) => true
   | _                 => false
 
-@[inline]
+@[inline, expose]
 public def TermType.isBitVecType : TermType → Bool
   | .prim (.bitvec _) => true
   | _                 => false
 
-@[inline]
+@[inline, expose]
 public def TermType.isRecordType : TermType → Bool
   | .record _ => true
   | _         => false
 
-@[inline]
+@[inline, expose]
 public def TermType.isOptionType : TermType → Bool
   | .option _ => true
   | _         => false
 
-@[inline]
+@[inline, expose]
 public def TermType.isOptionEntityType : TermType → Bool
   | .option (.entity _) => true
   | _                   => false

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

@@ -79,6 +79,11 @@ public theorem wf_empty {α β} [LT α] [DecidableLT α] :
   (Map.empty : Map α β).WellFormed
 := by simp [Map.WellFormed, Map.make, Map.empty, List.canonicalize_nil, Map.toList]
 
+public theorem wf_singleton [LT α] [DecidableLT α] (a : α) (b : β) :
+  (Map.mk [(a, b)]).WellFormed
+:= by
+  simp [WellFormed, make, toList, List.canonicalize_singleton]
+
 /--
   In well-formed maps, if there are two pairs with the same key, then they have
   the same value

cedar-lean/Cedar/Thm/SymCC/Compiler/Attr.lean

@@ -16,6 +16,8 @@
 
 import Cedar.Thm.SymCC.Compiler.Invert
 import Cedar.Thm.SymCC.Compiler.WF
+import Cedar.Thm.SymCC.Env.Interpret
+import Cedar.Thm.SymCC.Term.Interpret
 
 /-!
 This file proves the compilation lemmas for `.hasAttr` and `.getAttr` expressions.
@@ -49,25 +51,25 @@ private theorem compile_evaluate_hasAttr_record_aux
     subst htₐ
     case inl =>
       replace hf := record_value?_find?_optional_none (wf_term_record_implies_wf_map hwo.left) hf ih
-      simp only [pe_isSome_none, bool_value?, Map.contains, hf, Option.isSome_none]
+      simp only [pe_isSome_none, value?_bool, Map.contains, hf, Option.isSome_none]
     case inr =>
       replace ⟨vₐ, hf, _⟩ := record_value?_find?_optional_some (wf_term_record_implies_wf_map hwo.left) hf ih
-      simp only [pe_isSome_some, bool_value?, Option.some.injEq, Value.prim.injEq,
+      simp only [pe_isSome_some, value?_bool, Option.some.injEq, Value.prim.injEq,
         Prim.bool.injEq]
       rw [eq_comm, Map.contains_iff_some_find?]
       exists vₐ
   case h_2 aty hnopt haty =>
     replace ⟨tₐ, hf, hf'⟩ := typeOf_term_record_attr_value hwo.right haty
     subst hf'
     replace ⟨vₐ, hf, _⟩ := record_value?_find?_required (wf_term_record_implies_wf_map hwo.left) hnopt hf ih
-    simp only [Same.same, SameResults, SameValues, bool_value?, Option.some.injEq,
+    simp only [Same.same, SameResults, SameValues, value?_bool, Option.some.injEq,
       Value.prim.injEq, Prim.bool.injEq]
     rw [eq_comm, Map.contains_iff_some_find?]
     exists vₐ
   case h_3 heq =>
     replace heq := typeOf_term_record_attr_value_none hwo.right heq
     replace heq := record_value?_find?_none (wf_term_record_implies_wf_map hwo.left) heq ih
-    simp only [Same.same, SameResults, SameValues, bool_value?, Map.contains, heq,
+    simp only [Same.same, SameResults, SameValues, value?_bool, Map.contains, heq,
       Option.isSome_none]
 
 private theorem compile_evaluate_hasAttr_record
@@ -172,7 +174,7 @@ private theorem compile_evaluate_hasAttr_entity
     have ht₁ := isLiteral_some.mp (same_ok_value_implies_lit ih)
     replace ⟨uid, ht₁, huid⟩ := wfl_of_type_entity_is_entity (And.intro hwo.left ht₁) hwo.right
     subst ht₁ huid
-    simp only [Same.same, SameResults, SameValues, entity_value?, Option.some.injEq] at ih
+    simp only [Same.same, SameResults, SameValues, value?_entity, Option.some.injEq] at ih
     subst ih
     simp only [hasAttr, attrsOf, Except.bind_ok]
     replace ⟨rt, happ, hrty, hwfl, hv⟩ := compile_evaluate_attrsOrEmpty heq hwε hf hwo hrty hwf₁
@@ -487,7 +489,7 @@ private theorem compile_evaluate_getAttr_entity
     have ht₁ := isLiteral_some.mp (same_ok_value_implies_lit ih)
     replace ⟨uid, ht₁, huid⟩ := wfl_of_type_entity_is_entity (And.intro hwo.left ht₁) hwo.right
     subst ht₁ huid
-    simp only [Same.same, SameResults, SameValues, entity_value?, Option.some.injEq] at ih
+    simp only [Same.same, SameResults, SameValues, value?_entity, Option.some.injEq] at ih
     subst ih
     simp only [getAttr, attrsOf]
     replace ⟨rt, happ, hrty, hwfl, hv⟩ := compile_evaluate_attrsOrEmpty heq hwε hf hwo hrty hwf₁