use module system in Decoder.lean and Encoder.lean (#906)

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

Author: cdisselkoen

cedar-lean/Cedar/SymCC.lean

@@ -14,16 +14,21 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Extractor
-import Cedar.SymCC.Decoder
-import Cedar.SymCC.Encoder
-import Cedar.SymCC.SatUnsat
-import Cedar.SymCC.Solver
-import Cedar.SymCC.Verifier
-import Cedar.Validation.Validator
+module
+
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.SymCC.Extractor
+public import Cedar.SymCC.Decoder
+public import Cedar.SymCC.Encoder
+public import Cedar.SymCC.SatUnsat
+public import Cedar.SymCC.Solver
+public import Cedar.SymCC.Verifier
+public import Cedar.Validation.Validator
 
 /-! This file contains the top-level interface to SymCC. -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC
 
 open Cedar.Spec

cedar-lean/Cedar/SymCC/Decoder.lean

@@ -14,9 +14,11 @@
  limitations under the License.
 -/
 
+module
+
 import Cedar.Spec
-import Cedar.SymCC.Encoder
-import Cedar.SymCC.Interpretation
+public import Cedar.SymCC.Encoder
+public import Cedar.SymCC.Interpretation
 import Cedar.Validation
 import Std.Internal.Parsec.Basic
 
@@ -34,7 +36,8 @@ See also Appendix B of https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-0
 namespace Cedar.SymCC.Decoder
 
 open Std.Internal.Parsec String Batteries
-open Cedar.Spec Cedar.Validation Cedar.Data
+open Cedar.Validation Cedar.Data
+open Cedar.Spec hiding Result
 
 ----- Parsing functions for SMTLib syntax -----
 
@@ -188,7 +191,7 @@ where
     let etyId ← enc.types.find? (.entity ety)
     .some (mems.mapIdx λ i eid => (Encoder.enumId etyId i, ⟨ety, eid⟩))
 
-abbrev Result (α) := Except String α
+public abbrev Result (α) := Except String α
 
 instance : Coe α (Result α) where
   coe := Except.ok
@@ -356,21 +359,21 @@ def defaultPrim (eidOf : EntityType → String) : TermPrimType → TermPrim
   | .entity ety => .entity ⟨ety, eidOf ety⟩
   | .ext xty    => defaultExt xty
 
-def defaultLit (eidOf : EntityType → String) : TermType → Term
+public def defaultLit (eidOf : EntityType → String) : TermType → Term
   | .prim pty   => .prim (defaultPrim eidOf pty)
   | .option ty  => .none ty
   | .set ty     => .set Set.empty ty
   | .record tys => .record (tys.mapOnValues₂ λ ⟨ty, _⟩ => defaultLit eidOf ty)
 
-def defaultUDF (eidOf : EntityType → String) (f : UUF) : UDF :=
+public def defaultUDF (eidOf : EntityType → String) (f : UUF) : UDF :=
   ⟨f.arg, f.out, Map.empty, defaultLit eidOf f.out⟩
 
-def eidOfForEntities (εs : SymEntities) (ety : EntityType) : String :=
+public def eidOfForEntities (εs : SymEntities) (ety : EntityType) : String :=
   match εs.find? ety with
   | .some ⟨_, _, .some (Set.mk (eid :: _)), _⟩ => eid
   | _                                          => ""
 
-def defaultInterpretation (εs : SymEntities) : Interpretation :=
+public def defaultInterpretation (εs : SymEntities) : Interpretation :=
   let eidOf := (eidOfForEntities εs)
   {
     vars := λ v => defaultLit eidOf v.ty,
@@ -386,7 +389,7 @@ environment `εnv`. If `εnv` is well-formed, the terms `ts` are well-formed wit
 respect to `εnv.entities`, and CVC5 is sound, the the resulting Interpretation
 satisfies `ts` and is well-formed with respect to `εnv.entities`.
 -/
-def decode (model : String) (enc : EncoderState) : Result Interpretation := do
+public def decode (model : String) (enc : EncoderState) : Result Interpretation := do
   let x ← SExpr.parse |>.run model
   let ⟨vars, uufs⟩ ← x.decodeModel (IdMaps.ofEncoderState enc)
   let eidOf := λ ety =>

cedar-lean/Cedar/SymCC/Encoder.lean

@@ -14,10 +14,12 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Env
+module
+
+public import Cedar.SymCC.Env
 import Cedar.SymCC.Factory
-import Cedar.SymCC.Solver
-import Batteries.Data.RBMap
+public import Cedar.SymCC.Solver
+public import Batteries.Data.RBMap
 
 /-!
 This file defines the Cedar encoder, which translates a list of boolean Terms
@@ -69,7 +71,7 @@ namespace Cedar.SymCC
 open Cedar.Spec Cedar.Validation
 open Solver Batteries
 
-structure EncoderState where
+public structure EncoderState where
   terms : RBMap Term String (compareOfLessAndEq · ·)
   types : RBMap TermType String (compareOfLessAndEq · ·)
   uufs  : RBMap UUF String (compareOfLessAndEq · ·)
@@ -84,12 +86,12 @@ abbrev EncoderM (α) := StateT EncoderState SolverM α
 
 namespace Encoder
 
-def termId (n : Nat)                    : String := s!"t{n}"
-def uufId (n : Nat)                     : String := s!"f{n}"
-def entityTypeId (n : Nat)              : String := s!"E{n}"
-def enumId (E : String) (n : Nat)       : String := s!"{E}_m{n}"
-def recordTypeId (n : Nat)              : String := s!"R{n}"
-def recordAttrId (R : String) (a : Nat) : String := s!"{R}_a{a}"
+def termId (n : Nat)                     : String := s!"t{n}"
+def uufId (n : Nat)                      : String := s!"f{n}"
+def entityTypeId (n : Nat)               : String := s!"E{n}"
+public def enumId (E : String) (n : Nat) : String := s!"{E}_m{n}"
+def recordTypeId (n : Nat)               : String := s!"R{n}"
+def recordAttrId (R : String) (a : Nat)  : String := s!"{R}_a{a}"
 
 def typeNum : EncoderM Nat := do return (← get).types.size
 def termNum : EncoderM Nat := do return (← get).terms.size
@@ -146,7 +148,7 @@ The maximum Unicode code point supported in SMT-LIB 2.7.
 Also see `num_codes` in cvc5:
 https://github.com/cvc5/cvc5/blob/b78e7ed23348659db52a32765ad181ae0c26bbd5/src/util/string.h#L53
 -/
-def smtLibMaxCodePoint : Nat := 196607
+public def smtLibMaxCodePoint : Nat := 196607
 
 /-
 This function needs to encode unicode strings with two levels of
@@ -335,7 +337,7 @@ Solver.lean.
 Note that `encode` itself first resets the solver in order to define datatypes
 etc.
 -/
-def encode (ts : List Term) (εnv : SymEnv) (produceModels : Bool := false) : SolverM EncoderState := do
+public def encode (ts : List Term) (εnv : SymEnv) (produceModels : Bool := false) : SolverM EncoderState := do
   Solver.reset
   Solver.setOptionProduceModels produceModels
   Solver.setLogic "ALL"

cedar-lean/Cedar/SymCC/Extractor.lean

@@ -14,10 +14,12 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Enforcer
-import Cedar.SymCC.Concretizer
-import Cedar.SymCC.Interpretation
+module
 
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.SymCC.Enforcer
+public import Cedar.SymCC.Concretizer
+public import Cedar.SymCC.Interpretation
 
 /-!
 # Extracting strongly well-formed counterexamples to verification queries
@@ -41,6 +43,8 @@ See `Cedar.Thm.SymCC.Verification` for how this is used to prove that verificati
 queries based on Cedar's compiler and hierarchy enforcer are correct.
 -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC
 
 open Data Factory Spec

cedar-lean/Cedar/SymCC/SatUnsat.lean

@@ -14,12 +14,17 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Concretizer
-import Cedar.SymCC.Decoder
-import Cedar.SymCC.Extractor
-import Cedar.SymCC.Interpretation
-import Cedar.SymCC.Solver
-import Cedar.SymCC.Verifier
+module
+
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.SymCC.Concretizer
+public import Cedar.SymCC.Decoder
+public import Cedar.SymCC.Extractor
+public import Cedar.SymCC.Interpretation
+public import Cedar.SymCC.Solver
+public import Cedar.SymCC.Verifier
+
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
 
 namespace Cedar.SymCC
 

cedar-lean/Cedar/SymCCOpt.lean

@@ -14,15 +14,20 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC
-import Cedar.SymCCOpt.CompiledPolicies
-import Cedar.SymCCOpt.Extractor
-import Cedar.SymCCOpt.SatUnsat
-import Cedar.SymCCOpt.Verifier
-import Cedar.Validation.Validator
+module
+
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.SymCC
+public import Cedar.SymCCOpt.CompiledPolicies
+public import Cedar.SymCCOpt.Extractor
+public import Cedar.SymCCOpt.SatUnsat
+public import Cedar.SymCCOpt.Verifier
+public import Cedar.Validation.Validator
 
 /-! This file contains the top-level interface to optimized SymCC. -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC
 
 open Cedar.Spec

cedar-lean/Cedar/SymCCOpt/Authorizer.lean

@@ -14,25 +14,27 @@
  limitations under the License.
 -/
 
-import Cedar.SymCCOpt.Compiler
+module
+
+public import Cedar.SymCCOpt.Compiler
 
 namespace Cedar.SymCC.Opt
 
 open Factory Cedar.Spec
 
-def compileWithEffect (effect : Effect) (policy : Policy) (εnv : SymEnv) : Result (Option CompileResult) :=
+public def compileWithEffect (effect : Effect) (policy : Policy) (εnv : SymEnv) : Result (Option CompileResult) :=
   if policy.effect == effect
   then Opt.compile policy.toExpr εnv
   else .ok .none
 
-def satisfiedPolicies (effect : Effect) (policies : Policies) (εnv : SymEnv) : Result CompileResult := do
+public def satisfiedPolicies (effect : Effect) (policies : Policies) (εnv : SymEnv) : Result CompileResult := do
   let ress ← policies.filterMapM (compileWithEffect effect · εnv)
   .ok {
     term := anyTrue (eq · (someOf true)) (ress.map CompileResult.term)
     footprint := ress.mapUnion CompileResult.footprint
   }
 
-def isAuthorized (policies : Policies) (εnv : SymEnv) : Result CompileResult := do
+public def isAuthorized (policies : Policies) (εnv : SymEnv) : Result CompileResult := do
   let forbids ← satisfiedPolicies .forbid policies εnv
   let permits ← satisfiedPolicies .permit policies εnv
   .ok {

cedar-lean/Cedar/SymCCOpt/CompiledPolicies.lean

@@ -14,11 +14,16 @@
  limitations under the License.
 -/
 
-import Cedar.Spec
-import Cedar.SymCC
-import Cedar.SymCCOpt.Authorizer
-import Cedar.SymCCOpt.Compiler
-import Cedar.Validation.Validator
+module
+
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.Spec
+public import Cedar.SymCC
+public import Cedar.SymCCOpt.Authorizer
+public import Cedar.SymCCOpt.Compiler
+public import Cedar.Validation.Validator
+
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
 
 namespace Cedar.SymCC
 

cedar-lean/Cedar/SymCCOpt/Compiler.lean

@@ -14,10 +14,13 @@
  limitations under the License.
 -/
 
-import Cedar.SymCC.Compiler
-import Cedar.SymCC.Env
-import Cedar.SymCC.ExtFun
-import Cedar.SymCC.Factory
+module
+
+-- TODO: once we remove the `@[expose]`s below, do all of these need to be public imports?
+public import Cedar.SymCC.Compiler
+public import Cedar.SymCC.Env
+public import Cedar.SymCC.ExtFun
+public import Cedar.SymCC.Factory
 
 /-!
 This file defines an optimized Cedar symbolic compiler, which computes the
@@ -30,6 +33,8 @@ For notes on the meaning of compile or footprint, see SymCC/Compiler.lean and
 SymCC/Enforcer.lean, which have clearer, unoptimized implementations.
 -/
 
+@[expose] public section -- TODO: make the public interface more granular/intentional, instead of having everything public and exposed
+
 namespace Cedar.SymCC.Opt
 
 open Cedar.Data Cedar.Spec Cedar.Validation

cedar-lean/Cedar/SymCCOpt/Enforcer.lean

@@ -14,8 +14,10 @@
  limitations under the License.
 -/
 
+module
+
 import Cedar.SymCC.Enforcer
-import Cedar.SymCCOpt.CompiledPolicies
+public import Cedar.SymCCOpt.CompiledPolicies
 
 namespace Cedar.SymCC
 
@@ -24,22 +26,22 @@ open Cedar.Data Cedar.Spec Factory
 /--
 Returns the ground acyclicity and transitivity assumptions for a single `CompiledPolicy`.
 -/
-def enforceCompiledPolicy (cp : CompiledPolicy) : Set Term :=
+public def enforceCompiledPolicy (cp : CompiledPolicy) : Set Term :=
   let tr := cp.footprint.elts.flatMap (λ t => cp.footprint.elts.map (transitivity t · cp.εnv.entities))
   Set.make (cp.acyclicity.elts ++ tr)
 
 /--
 Returns the ground acyclicity and transitivity assumptions for a single `CompiledPolicySet`.
 -/
-def enforceCompiledPolicySet (cpset : CompiledPolicySet) : Set Term :=
+public def enforceCompiledPolicySet (cpset : CompiledPolicySet) : Set Term :=
   let tr := cpset.footprint.elts.flatMap (λ t => cpset.footprint.elts.map (transitivity t · cpset.εnv.entities))
   Set.make (cpset.acyclicity.elts ++ tr)
 
 /--
 Returns the ground acyclicity and transitivity assumptions for a pair of `CompiledPolicy`.
 Caller guarantees that `cp₁` and `cp₂` were compiled for the same `εnv`.
 -/
-def enforcePairCompiledPolicy (cp₁ : CompiledPolicy) (cp₂ : CompiledPolicy) : Set Term :=
+public def enforcePairCompiledPolicy (cp₁ : CompiledPolicy) (cp₂ : CompiledPolicy) : Set Term :=
   assert! cp₁.εnv = cp₂.εnv
   let footprint := cp₁.footprint ++ cp₂.footprint
   let tr := footprint.elts.flatMap (λ t => footprint.elts.map (transitivity t · cp₁.εnv.entities))
@@ -49,7 +51,7 @@ def enforcePairCompiledPolicy (cp₁ : CompiledPolicy) (cp₂ : CompiledPolicy)
 Returns the ground acyclicity and transitivity assumptions for a pair of `CompiledPolicySet`.
 Caller guarantees that `cpset₁` and `cpset₂` were compiled for the same `εnv`.
 -/
-def enforcePairCompiledPolicySet (cpset₁ : CompiledPolicySet) (cpset₂ : CompiledPolicySet) : Set Term :=
+public def enforcePairCompiledPolicySet (cpset₁ : CompiledPolicySet) (cpset₂ : CompiledPolicySet) : Set Term :=
   assert! cpset₁.εnv = cpset₂.εnv
   let footprint := cpset₁.footprint ++ cpset₂.footprint
   let tr := footprint.elts.flatMap (λ t => footprint.elts.map (transitivity t · cpset₁.εnv.entities))