modules in Cedar.SymCC and Cedar.Thm.SymCC.Data (#895)

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

Author: cdisselkoen

cedar-lean/Cedar/Data/Int64.lean

@@ -40,6 +40,22 @@ public def ofInt? (i : Int) : Option Int64 :=
   then .some (ofIntChecked i h)
   else .none
 
+/-- We don't @[expose] the definition of `ofInt?`; but callers can use this
+theorem, which partially specifies its behavior -/
+public theorem ofInt?_some_iff {i : Int} :
+  MIN ≤ i ∧ i ≤ MAX ↔ (ofInt? i).isSome
+:= by simp [ofInt?]
+
+/-- Corollary 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
+
 public def add? (i₁ i₂ : Int64) : Option Int64 := ofInt? (i₁.toInt + i₂.toInt)
 
 public def sub? (i₁ i₂ : Int64) : Option Int64 := ofInt? (i₁.toInt - i₂.toInt)

cedar-lean/Cedar/Data/SizeOf.lean

@@ -69,6 +69,19 @@ public theorem sizeOf_lt_of_value [SizeOf α] [SizeOf β] {m : Map α β} {k : 
     omega
   omega
 
+public theorem sizeOf_lt_of_find? [SizeOf α] [SizeOf β] [DecidableEq α] {m : Map α β} {k : α} {v : β}
+  (h : m.find? k = some v) :
+  sizeOf v < sizeOf m
+:= by
+  simp only [find?, toList] at h
+  split at h <;> simp only [Option.some.injEq, reduceCtorEq] at h
+  subst v
+  rename_i h
+  replace h := List.mem_of_find?_eq_some h
+  have := List.sizeOf_lt_of_mem h
+  simp_all only [sizeOf, Prod._sizeOf_1, _sizeOf_1]
+  omega
+
 public theorem sizeOf_lt_of_toList [SizeOf α] [SizeOf β] (m : Map α β) :
   sizeOf m.toList < sizeOf m
 := by

cedar-lean/Cedar/Spec/Value.lean

@@ -72,6 +72,16 @@ public inductive Value where
   | record (m : Map Attr Value)
   | ext (x : Ext)
 
+----- SizeOf -----
+
+public theorem Value.sizeOf_set' (s : Set Value) :
+  sizeOf (Value.set s) = 1 + sizeOf s
+:= by simp [Value.set.sizeOf_spec]
+
+public theorem Value.sizeOf_record' (m : Map Attr Value) :
+  sizeOf (Value.record m) = 1 + sizeOf m
+:= by simp [Value.record.sizeOf_spec]
+
 ----- Coercions -----
 
 @[expose]

cedar-lean/Cedar/SymCC/Authorizer.lean

@@ -14,8 +14,13 @@
  limitations under the License.
 -/
 
+module
+
+public import Cedar.Spec
 import Cedar.SymCC.Enforcer
+public import Cedar.SymCC.Env
 import Cedar.SymCC.Compiler
+public import Cedar.SymCC.Result
 
 /-!
 
@@ -33,16 +38,18 @@ namespace Cedar.SymCC
 
 open Factory Cedar.Spec
 
-def compileWithEffect (effect : Effect) (policy : Policy) (εnv : SymEnv) : Result (Option Term) :=
+-- TODO: make `private` once files like AllowDeny.lean are made `module`s and can `import all` this file (they prove things about these functions and need access to internals in this file)
+public def compileWithEffect (effect : Effect) (policy : Policy) (εnv : SymEnv) : Result (Option Term) :=
   if policy.effect == effect
   then compile policy.toExpr εnv
   else .ok .none
 
-def satisfiedPolicies (effect : Effect) (policies : Policies) (εnv : SymEnv) : Result Term := do
+-- TODO: make `private` once files like AllowDeny.lean are made `module`s and can `import all` this file (they prove things about these functions and need access to internals in this file)
+public def satisfiedPolicies (effect : Effect) (policies : Policies) (εnv : SymEnv) : Result Term := do
   let ts ← policies.filterMapM (compileWithEffect effect · εnv)
   anyTrue (eq · (someOf true)) ts
 
-def isAuthorized (policies : Policies) (εnv : SymEnv) : Result Term := do
+public def isAuthorized (policies : Policies) (εnv : SymEnv) : Result Term := do
   let forbids ← satisfiedPolicies .forbid policies εnv
   let permits ← satisfiedPolicies .permit policies εnv
   and permits (not forbids)

cedar-lean/Cedar/SymCC/Compiler.lean

@@ -14,9 +14,13 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Env
-import Cedar.SymCC.ExtFun
-import Cedar.SymCC.Factory
+module
+
+public import Cedar.Spec
+public import Cedar.SymCC.Env
+public import Cedar.SymCC.ExtFun
+public import Cedar.SymCC.Factory -- TODO: this need not be a public import
+public import Cedar.SymCC.Result
 
 /-!
 
@@ -31,6 +35,8 @@ environment: using this Term for verification will neither miss bugs
 (soundness) nor produce false positives (completeness).
 -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC
 
 open Cedar.Data Cedar.Spec Cedar.Validation

cedar-lean/Cedar/SymCC/Concretizer.lean

@@ -14,7 +14,13 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Env
+module
+
+public import Cedar.Data.SizeOf
+public import Cedar.Spec
+public import Cedar.SymCC.Env
+public import Cedar.SymCC.Factory -- TODO: this need not be a public import
+public import Cedar.SymCC.Term
 
 /-!
 # Concretizing symbolic environments
@@ -28,6 +34,8 @@ complete.
 See Cedar.Thm.SymbolicCompilation for a statement of the completeness theorem.
 -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.Spec
 
 open Data Spec
@@ -41,6 +49,16 @@ def Value.entityUIDs : Value → Set EntityUID
   | .set (Set.mk vs)     => vs.mapUnion₁ (λ ⟨v, _⟩ => v.entityUIDs)
   | .record avs          => avs.toList.mapUnion₃ (λ ⟨(_, v), _⟩ => v.entityUIDs)
   | .ext _               => Set.empty
+termination_by v => sizeOf v
+decreasing_by
+  all_goals simp_wf
+  · rename_i h
+    have := List.sizeOf_lt_of_mem h
+    omega
+  · rename_i h
+    have := Map.sizeOf_lt_of_toList avs
+    simp at *
+    omega
 
 def Value.entityUID? : Value → Option EntityUID
   | .prim (.entityUID uid) => .some uid

cedar-lean/Cedar/SymCC/Data.lean

@@ -14,33 +14,35 @@
  limitations under the License.
 -/
 
-import Cedar.Data
+module
+
+public import Cedar.Data
 import Cedar.Spec
 
 /-!
 This file contains generic utility functions shared by `SymCC` modules.
 -/
 
-@[inline] def BitVec.width {n : Nat} (_ : BitVec n) : Nat := n
+@[inline, expose] public def BitVec.width {n : Nat} (_ : BitVec n) : Nat := n
 
-def BitVec.signedMin (n : Nat) : Int := - 2 ^ (n-1)
+public def BitVec.signedMin (n : Nat) : Int := - 2 ^ (n-1)
 
-def BitVec.signedMax (n : Nat) : Int := 2 ^ (n-1) - 1
+public def BitVec.signedMax (n : Nat) : Int := 2 ^ (n-1) - 1
 
-def BitVec.overflows (n : Nat) (i : Int) : Bool :=
+public def BitVec.overflows (n : Nat) (i : Int) : Bool :=
   i < (BitVec.signedMin n) ||
   i > (BitVec.signedMax n)
 
 namespace Cedar.SymCC
 
 open Cedar.Data
 
-abbrev EntityTag (α) := Map String α
+public abbrev EntityTag (α) := Map String α
 
-abbrev EntityTag.mk {α} (entity tag : α) : EntityTag α :=
+public abbrev EntityTag.mk {α} (entity tag : α) : EntityTag α :=
   Map.mk [("entity", entity), ("tag", tag)]
 
-abbrev EntityTag.wf {α} : EntityTag α → Bool
+public abbrev EntityTag.wf {α} : EntityTag α → Bool
   | .mk _ _ => true
   | _       => false
 

cedar-lean/Cedar/SymCC/Enforcer.lean

@@ -14,7 +14,9 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Compiler
+module
+
+public import Cedar.SymCC.Compiler -- TODO: this need not be a public import
 
 /-!
 This file defines the algorithm for emitting well-formedness assumptions about
@@ -34,6 +36,8 @@ grounding procedure computes the footprint, and grounds the acyclicity and
 transitivity constraints on the set of entity terms in the footprint.
 -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC
 
 open Cedar.Data