Use Lean4 modules in more files

Strata.lean

@@ -22,6 +22,7 @@ import Strata.Util.Sarif
 /- Strata Core -/
 import Strata.Languages.Core.FactoryWF
 import Strata.Languages.Core.StatementSemantics
+import Strata.Languages.Core.Core
 import Strata.Languages.Core.SarifOutput
 
 /- Code Transforms -/

Strata/Backends/CBMC/GOTO/SourceLocation.lean

@@ -3,9 +3,11 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Lean.Data.Json
+public import Lean.Data.Json
 
+public section
 namespace CProverGOTO
 -------------------------------------------------------------------------------
 
@@ -28,3 +30,5 @@ instance : ToString SourceLocation where
     else s!"{loc.file}:{loc.line}:{loc.column}"
 
 -------------------------------------------------------------------------------
+end CProverGOTO
+end

Strata/DDM/Integration/Categories.lean

@@ -4,7 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 module
+
 public import Strata.DDM.AST
+public import Std.Data.HashSet.Basic
 
 public section
 namespace Strata.DDM.Integration
@@ -34,3 +36,4 @@ def abstractCategories : Std.HashSet QualifiedIdent := Std.HashSet.ofList [
 ]
 
 end Strata.DDM.Integration
+end

Strata/DL/Imperative/EvalError.lean

@@ -3,10 +3,9 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-
-
-import Strata.DL.Imperative.PureExpr
+public import Strata.DL.Imperative.PureExpr
 
 namespace Imperative
 open Std (ToFormat Format format)
@@ -17,7 +16,7 @@ open Std (ToFormat Format format)
 `EvalError` denotes the kinds of errors that may arise during (partial)
 evaluation of Imperative programs.
 -/
-inductive EvalError (P : PureExpr) where
+public inductive EvalError (P : PureExpr) where
   | InitVarExists (tid : P.TypedIdent) (existing_value : P.Expr)
   | AssignVarNotExists (tid : P.Ident) (value : P.Expr)
   | HavocVarNotExists (tid : P.Ident)
@@ -49,7 +48,7 @@ def EvalError.toFormat [ToFormat P.Expr] [ToFormat P.Ident] [ToFormat P.Ty]
 instance [ToFormat P.Expr] [ToFormat P.Ident] [ToFormat P.Ty] : ToFormat (EvalError P) where
   format := EvalError.toFormat
 
-inductive EvalWarning (P : PureExpr) where
+public inductive EvalWarning (P : PureExpr) where
   | AssumeFail (label : String) (b : P.Expr)
 
 def EvalWarning.toFormat [ToFormat P.Expr] [ToFormat P.Ident] [ToFormat P.Ty]

Strata/DL/Imperative/HasVars.lean

@@ -3,8 +3,11 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.DL.Imperative.PureExpr
+public import Strata.DL.Imperative.PureExpr
+
+public section
 
 namespace Imperative
 
@@ -46,3 +49,5 @@ class HasVarsTrans
 abbrev HasVarsProcTrans (P : PureExpr) (PT : Type) := HasVarsTrans P PT PT
 
 end Imperative
+
+end

Strata/DL/Imperative/PureExpr.lean

@@ -3,8 +3,9 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-
+public section
 
 namespace Imperative
 
@@ -64,3 +65,5 @@ class HasBoolVal (P : PureExpr) [HasBool P] [HasVal P] where
   bool_is_val : (@HasVal.value P) HasBool.tt ∧ (@HasVal.value P) HasBool.ff
 
 end Imperative
+
+end

Strata/DL/Lambda/MetaData.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 namespace Lambda
 /--
@@ -11,7 +12,7 @@ Metadata annotations.
 [Stopgap] We will eventually design a structured metadata language that we will
 modify along with our code transformation functions.
 -/
-structure Info where
+public structure Info where
   value : String
   deriving DecidableEq, Repr
 

Strata/DL/SMT/Basic.lean

@@ -3,13 +3,14 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-@[inline] def BitVec.width {n : Nat} (_ : BitVec n) : Nat := n
+@[inline] public def BitVec.width {n : Nat} (_ : BitVec n) : Nat := n
 
 def BitVec.signedMin (n : Nat) : Int := - 2 ^ (n-1)
 
 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)

Strata/DL/SMT/CexParser.lean

@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-
+module
 
 import Std.Internal.Parsec.String
 
@@ -15,7 +15,7 @@ open Std (Format ToFormat format)
 Represents a key-value pair, representing the value of a variable (key) in a
 counterexample.
 -/
-structure KeyValue where
+public structure KeyValue where
   key: String
   value: String
 deriving Repr
@@ -24,11 +24,11 @@ instance : ToFormat KeyValue where
   format kv := f!"({kv.key} {kv.value})"
 
 /-- Represents a counterexample as a list of key-value pairs -/
-structure CEx where
+public structure CEx where
   pairs: List KeyValue
 deriving Repr
 
-def CEx.format (cex : CEx) : Format :=
+public def CEx.format (cex : CEx) : Format :=
   go cex.pairs
   where go pairs :=
   match pairs with
@@ -90,7 +90,7 @@ def parseCEx1 : Parser CEx := do
     ws
     return { pairs := [] }))
 
-def parseCEx (cex : String) : Except Format CEx :=
+public def parseCEx (cex : String) : Except Format CEx :=
   match parseCEx1 ⟨cex, cex.startValidPos⟩ with
   | Std.Internal.Parsec.ParseResult.success _ result => Except.ok result
   | Std.Internal.Parsec.ParseResult.error ⟨_, pos⟩ msg => Except.error s!"Parse error at {pos.offset}: {msg}"

Strata/DL/SMT/Solver.lean

@@ -4,6 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+module
+
 /-!
 Based on Cedar's Term language.
 (https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/SymCC/Solver.lean)
@@ -15,7 +17,7 @@ s-expressions encoded as strings. The interface is based on
 
 namespace Strata.SMT
 
-inductive Decision where
+public inductive Decision where
   | sat
   | unsat
   | unknown
@@ -31,16 +33,18 @@ deriving DecidableEq, Repr
  each command. We don't have an error stream here, since we configure solvers to
  run in quiet mode and not print anything to the error stream.
 -/
-structure Solver where
+public structure Solver where
   smtLibInput : IO.FS.Stream
   smtLibOutput : Option IO.FS.Stream
 
-abbrev SolverM (α) := ReaderT Solver IO α
+public abbrev SolverM (α) := ReaderT Solver IO α
 
 def SolverM.run (solver : Solver) (x : SolverM α) : IO α := ReaderT.run x solver
 
 namespace Solver
 
+public section
+
 /--
   Returns a Solver for the given path and arguments. This function expects
   `path` to point to an SMT solver executable, and `args` to specify valid
@@ -84,12 +88,16 @@ def fileWriter (h : IO.FS.Handle) : IO Solver :=
 def bufferWriter (b : IO.Ref IO.FS.Stream.Buffer) : IO Solver :=
   return ⟨IO.FS.Stream.ofBuffer b, .none⟩
 
+end
+
 private def emitln (str : String) : SolverM Unit := do
   -- dbg_trace "{str}" -- uncomment to see input sent to the solver
   let solver ← read
   solver.smtLibInput.putStr s!"{str}\n"
   solver.smtLibInput.flush
 
+public section
+
 def setLogic (logic : String) : SolverM Unit :=
   emitln s!"(set-logic {logic})"
 
@@ -145,11 +153,15 @@ def declareDatatypes (dts : List (String × List String × List String)) : Solve
   let bodyStr := String.intercalate "\n  " bodies
   emitln s!"(declare-datatypes ({sortDeclStr})\n  ({bodyStr}))"
 
+end
+
 private def readlnD (dflt : String) : SolverM String := do
   match (← read).smtLibOutput with
   | .some stdout => stdout.getLine
   | .none        => pure dflt
 
+public section
+
 def checkSat (vars : List String) : SolverM Decision := do
   emitln "(check-sat)"
   let result := (← readlnD "unknown").trim
@@ -171,6 +183,8 @@ def reset : SolverM Unit :=
 def exit : SolverM Unit :=
   emitln "(exit)"
 
+end
+
 end Solver
 
 end Strata.SMT

Strata/DL/SMT/TermType.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 /-!
 Based on Cedar's Term language.
@@ -11,6 +12,7 @@ This file defines the types of Terms.  See `Term.lean` for the
 definition of the Term language.
 -/
 
+public section
 namespace Strata.SMT
 
 inductive TermPrimType where
@@ -191,3 +193,4 @@ def TermType.isConstrType : TermType → Bool
   | _         => false
 
 end Strata.SMT
+end

Strata/DL/Util/Counter.lean

@@ -3,6 +3,7 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
 /-! ## Counter Generator
   This file contains a counter generator `genCounter`, as well as its underlying
@@ -20,35 +21,35 @@
 
 namespace Counter
 
-structure CounterState where
+public structure CounterState where
   counter : Nat := 0
   generated : List Nat := [] -- a set of numbers generated by the generator
 
-instance : HasSubset CounterState where
+public instance : HasSubset CounterState where
   Subset σ₁ σ₂ := σ₁.generated.Subset σ₂.generated
 
 @[simp]
-def CounterState.emp : CounterState := { counter := 0, generated := [] }
+public def CounterState.emp : CounterState := { counter := 0, generated := [] }
 
-def WF (σ : CounterState)
+public def WF (σ : CounterState)
   := (∀ c, c ∈ σ.generated → c < σ.counter)
       ∧ σ.generated.Nodup
 
-def genCounter (σ : CounterState)
+public def genCounter (σ : CounterState)
   : Nat × CounterState
   := (σ.counter, { σ with
       counter := σ.counter + 1,
       generated := σ.counter :: σ.generated
     })
 
-theorem genCounterSubset : genCounter σ = (n, σ') → σ ⊆ σ' := by
+public theorem genCounterSubset : genCounter σ = (n, σ') → σ ⊆ σ' := by
   intros Hgen
   simp [genCounter] at Hgen
   simp [← Hgen, HasSubset.Subset]
   intros a Hin
   simp_all
 
-theorem genCounterContains :
+public theorem genCounterContains :
   genCounter σ = (n, σ') →
   n ∈ σ'.generated := by
   intros Hgen
@@ -66,7 +67,7 @@ theorem genCounterValue :
 theorem emptyCounterWF :
   WF .emp := by simp [WF]
 
-theorem genCounterWFMono :
+public theorem genCounterWFMono :
   WF σ →
   genCounter σ = (n, σ') →
   WF σ' := by

Strata/DL/Util/DecidableEq.lean

@@ -3,8 +3,9 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-def beq_eq_DecidableEq
+public def beq_eq_DecidableEq
   {T : Type}
   (beq : T → T → Bool)
   (beq_eq : (x1 x2 : T) → beq x1 x2 = true ↔ x1 = x2) :