From 69fe3cd3ca2534c0fa04018022d61e71178e7eca Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 13:38:10 +0000 Subject: [PATCH 1/9] Add missing import to Strata.lean --- Strata.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Strata.lean b/Strata.lean index eb8afef34..ff01335f8 100644 --- a/Strata.lean +++ b/Strata.lean @@ -17,6 +17,7 @@ import Strata.DL.Imperative.Imperative /- Strata Core -/ import Strata.Languages.Core.StatementSemantics +import Strata.Languages.Core.Core /- Backends -/ import Strata.Backends.CBMC.CProver From fddbca9e8f1ecc645597437bfa6a921fb73c67fb Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 13:46:30 +0000 Subject: [PATCH 2/9] PureExpr is now a module --- Strata/DL/Imperative/PureExpr.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Strata/DL/Imperative/PureExpr.lean b/Strata/DL/Imperative/PureExpr.lean index 9428839c2..389ae9fd3 100644 --- a/Strata/DL/Imperative/PureExpr.lean +++ b/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 From 2b9d157d5c95193c0504be96cbb3e718a5c7da65 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 14:13:53 +0000 Subject: [PATCH 3/9] Add more module --- Strata/DL/Imperative/HasVars.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Strata/DL/Imperative/HasVars.lean b/Strata/DL/Imperative/HasVars.lean index 4658df925..7300e390e 100644 --- a/Strata/DL/Imperative/HasVars.lean +++ b/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 From 047f0f430758d3fe2b7c73f40334f3c84405fd1e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 14:18:26 +0000 Subject: [PATCH 4/9] Convert EvalError.lean and HasVars.lean to modules --- Strata/DL/Imperative/EvalError.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Strata/DL/Imperative/EvalError.lean b/Strata/DL/Imperative/EvalError.lean index e9de28ead..ff05060b1 100644 --- a/Strata/DL/Imperative/EvalError.lean +++ b/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] From 1834e955db267c19cce312d38fab85a83eada9b0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 14:47:31 +0000 Subject: [PATCH 5/9] Add more modules --- Strata/DL/Lambda/MetaData.lean | 1 + Strata/DL/SMT/Basic.lean | 5 +++-- Strata/DL/Util/DecidableEq.lean | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Strata/DL/Lambda/MetaData.lean b/Strata/DL/Lambda/MetaData.lean index abd6eebbe..3aa103e53 100644 --- a/Strata/DL/Lambda/MetaData.lean +++ b/Strata/DL/Lambda/MetaData.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module namespace Lambda /-- diff --git a/Strata/DL/SMT/Basic.lean b/Strata/DL/SMT/Basic.lean index 25bd10969..1eabbee6f 100644 --- a/Strata/DL/SMT/Basic.lean +++ b/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) diff --git a/Strata/DL/Util/DecidableEq.lean b/Strata/DL/Util/DecidableEq.lean index f74ae5e33..26a4f484c 100644 --- a/Strata/DL/Util/DecidableEq.lean +++ b/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) : From 19ee4fce50ee7f9f4f67e20de5dc6f845c9d05f8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 29 Jan 2026 15:40:13 +0000 Subject: [PATCH 6/9] Add more module --- Strata/DL/Util/Counter.lean | 17 +++++++++-------- Strata/DL/Util/List.lean | 15 ++++++++------- Strata/DL/Util/ListUtils.lean | 5 +++-- Strata/DL/Util/Nodup.lean | 1 + 4 files changed, 21 insertions(+), 17 deletions(-) diff --git a/Strata/DL/Util/Counter.lean b/Strata/DL/Util/Counter.lean index 09b577516..f08727542 100644 --- a/Strata/DL/Util/Counter.lean +++ b/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 diff --git a/Strata/DL/Util/List.lean b/Strata/DL/Util/List.lean index 38097bcd4..117891e28 100644 --- a/Strata/DL/Util/List.lean +++ b/Strata/DL/Util/List.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module /-! # List Utilities -/ @@ -20,7 +21,7 @@ theorem List.subset_append_cons_right {α : Type} [DecidableEq α] {a b c : List /-- Remove duplicates in a list. -/ -def dedup {α : Type} [DecidableEq α] : List α → List α +public def dedup {α : Type} [DecidableEq α] : List α → List α | [] => [] | a :: as => let as := as.dedup @@ -114,7 +115,7 @@ theorem length_dedup_cons_of_mem {α : Type} [DecidableEq α] (a : α) (l : List have : a ∈ l.dedup := mem_of_mem_dedup l a h simp [this] -theorem length_dedup_cons_of_not_mem {α : Type} [DecidableEq α] (a : α) (l : List α) +public theorem length_dedup_cons_of_not_mem {α : Type} [DecidableEq α] (a : α) (l : List α) (h : a ∉ l) : (a :: l).dedup.length = 1 + l.dedup.length := by induction l · simp_all [dedup] @@ -245,7 +246,7 @@ theorem length_dedup_of_removeAll {α : Type} [DecidableEq α] (a : α) (l : Lis simp_all omega -theorem length_dedup_append_le_left {α : Type} [DecidableEq α] (l₁ l₂ : List α) : +public theorem length_dedup_append_le_left {α : Type} [DecidableEq α] (l₁ l₂ : List α) : l₁.dedup.length ≤ (l₁ ++ l₂).dedup.length := by induction l₁ generalizing l₂ case nil => simp [dedup] @@ -305,7 +306,7 @@ theorem length_dedup_append_all_in_right {α : Type} [DecidableEq α] (l₁ l₂ simp_all done -theorem length_dedup_append_subset_right {α : Type} [DecidableEq α] (l₁ l₂ : List α) +public theorem length_dedup_append_subset_right {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : l₁ ⊆ l₂) : (l₁ ++ l₂).dedup.length = l₂.dedup.length := by simp_all [List.instHasSubset, List.Subset] @@ -336,7 +337,7 @@ theorem length_dedup_all_in_eq {α : Type} [DecidableEq α] (l₁ l₂ : List α have h_2 := @length_dedup_append_all_in_left _ _ l₁ l₂ h2 simp_all -theorem length_dedup_subset_eq {α : Type} [DecidableEq α] (l₁ l₂ : List α) +public theorem length_dedup_subset_eq {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h1 : l₁ ⊆ l₂) (h2 : l₂ ⊆ l₁) : l₁.dedup.length = l₂.dedup.length := by have := @length_dedup_all_in_eq _ _ l₁ l₂ @@ -391,7 +392,7 @@ theorem length_dedup_of_subset_not_mem_lt {α : Type} [DecidableEq α] (l₁ l have := @length_dedup_of_all_in_not_mem_lt _ _ l₁ l₂ a simp_all [List.instHasSubset, List.Subset] -theorem length_dedup_of_subset_le {α : Type} [DecidableEq α] (l₁ l₂ : List α) +public theorem length_dedup_of_subset_le {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : l₁ ⊆ l₂) : l₁.dedup.length ≤ l₂.dedup.length := by induction l₁ with | nil => simp_all [dedup] @@ -411,7 +412,7 @@ theorem length_dedup_of_subset_le {α : Type} [DecidableEq α] (l₁ l₂ : List simp_all [dedup] omega -theorem subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: s1 ⊆ s2) : s1.length ≤ s2.length := by +public theorem subset_nodup_length {α} {s1 s2: List α} (hn: s1.Nodup) (hsub: s1 ⊆ s2) : s1.length ≤ s2.length := by induction s1 generalizing s2 with | nil => simp | cons x t IH => diff --git a/Strata/DL/Util/ListUtils.lean b/Strata/DL/Util/ListUtils.lean index fed1532a0..0ce4a31e3 100644 --- a/Strata/DL/Util/ListUtils.lean +++ b/Strata/DL/Util/ListUtils.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module /-! ## List Properties Utilities This file contains miscellaneous utilities for manipulating lists and @@ -47,7 +48,7 @@ Taken from mathlib4 https://github.com/leanprover-community/mathlib4/blob/d7a4adb961ed411dbec6ff6857cfc771859ec83f/Mathlib/Data/List/Defs.lean#L131-L137 https://github.com/leanprover-community/mathlib4/blob/d7a4adb961ed411dbec6ff6857cfc771859ec83f/Mathlib/Data/List/Basic.lean#L1203-L1206 -/ -def Forall (p : α → Prop) : List α → Prop +public def Forall (p : α → Prop) : List α → Prop | [] => True | x :: [] => p x | x :: l => p x ∧ Forall p l @@ -91,7 +92,7 @@ def List.replaceAll [BEq α] : List α → α → α → List α /-- `Disjoint l₁ l₂` means that `l₁` and `l₂` have no elements in common. Taken from https://github.com/leanprover-community/batteries/blob/3613427d66262c4e25e19b40a6a49242e94ba072/Batteries/Data/List/Basic.lean#L512-L514 -/ -def List.Disjoint (l₁ l₂ : List α) : Prop := +public def List.Disjoint (l₁ l₂ : List α) : Prop := ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False theorem List.removeAll_Sublist [BEq α] {xs ys : List α}: diff --git a/Strata/DL/Util/Nodup.lean b/Strata/DL/Util/Nodup.lean index 4666eb762..9a726612d 100644 --- a/Strata/DL/Util/Nodup.lean +++ b/Strata/DL/Util/Nodup.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module /-! ## No Duplication Properties This file contains theormes related to `List.Nodup` property. The main theorem From 607f1d261c8822bdbebaadf9a8189df3bb0bbbe6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 30 Jan 2026 10:27:41 +0000 Subject: [PATCH 7/9] More modules --- Strata/Backends/CBMC/GOTO/SourceLocation.lean | 6 +++++- Strata/DDM/Integration/Categories.lean | 6 +++++- Strata/DDM/Integration/Java.lean | 1 + Strata/DDM/Integration/Java/Gen.lean | 1 + Strata/DL/SMT/TermType.lean | 3 +++ Strata/Languages/Core/Options.lean | 5 +++-- 6 files changed, 18 insertions(+), 4 deletions(-) diff --git a/Strata/Backends/CBMC/GOTO/SourceLocation.lean b/Strata/Backends/CBMC/GOTO/SourceLocation.lean index 142e33162..06a10034e 100644 --- a/Strata/Backends/CBMC/GOTO/SourceLocation.lean +++ b/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 diff --git a/Strata/DDM/Integration/Categories.lean b/Strata/DDM/Integration/Categories.lean index 208b61d06..c1b483e3a 100644 --- a/Strata/DDM/Integration/Categories.lean +++ b/Strata/DDM/Integration/Categories.lean @@ -3,9 +3,12 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module -import Strata.DDM.AST +public import Strata.DDM.AST +public import Std.Data.HashSet.Basic +public section namespace Strata.DDM.Integration open Strata @@ -35,3 +38,4 @@ def abstractCategories : Std.HashSet QualifiedIdent := Std.HashSet.ofList [ ] end Strata.DDM.Integration +end diff --git a/Strata/DDM/Integration/Java.lean b/Strata/DDM/Integration/Java.lean index deb694736..5f433bd42 100644 --- a/Strata/DDM/Integration/Java.lean +++ b/Strata/DDM/Integration/Java.lean @@ -3,5 +3,6 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module import Strata.DDM.Integration.Java.Gen diff --git a/Strata/DDM/Integration/Java/Gen.lean b/Strata/DDM/Integration/Java/Gen.lean index 577cf00dc..556b2cd46 100644 --- a/Strata/DDM/Integration/Java/Gen.lean +++ b/Strata/DDM/Integration/Java/Gen.lean @@ -3,6 +3,7 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module import Strata.DDM.AST import Strata.DDM.Integration.Categories diff --git a/Strata/DL/SMT/TermType.lean b/Strata/DL/SMT/TermType.lean index 48f0ea0b5..0a4adb9a3 100644 --- a/Strata/DL/SMT/TermType.lean +++ b/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 diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean index c85c0028a..53c349a0b 100644 --- a/Strata/Languages/Core/Options.lean +++ b/Strata/Languages/Core/Options.lean @@ -3,8 +3,9 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module -inductive VerboseMode where +public inductive VerboseMode where | quiet | normal | debug @@ -36,7 +37,7 @@ instance : LE VerboseMode where instance : DecidableRel (fun a b : VerboseMode => a ≤ b) := fun a b => decidable_of_iff (a.toNat ≤ b.toNat) Iff.rfl -structure Options where +public structure Options where verbose : VerboseMode parseOnly : Bool typeCheckOnly : Bool From af83d20ba6b4725115d0898956b3068456dc000f Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 2 Feb 2026 09:40:37 +0000 Subject: [PATCH 8/9] More modules --- Strata/DDM/Integration/Java/Gen.lean | 8 +- Strata/DL/Lambda/MetaData.lean | 2 +- Strata/DL/SMT/CexParser.lean | 10 +- Strata/DL/SMT/Solver.lean | 20 +++- Strata/DL/Util/ListUtils.lean | 96 +++++++++---------- Strata/DL/Util/Nodup.lean | 18 ++-- Strata/Languages/Core/Options.lean | 6 +- Strata/Languages/Core/Verifier.lean | 6 +- .../Languages/Dyn/DDMTransform/Translate.lean | 2 + Strata/Languages/Dyn/Verify.lean | 2 + .../Laurel/LaurelToCoreTranslator.lean | 2 +- Strata/Languages/Python/Regex/ReParser.lean | 6 ++ 12 files changed, 101 insertions(+), 77 deletions(-) diff --git a/Strata/DDM/Integration/Java/Gen.lean b/Strata/DDM/Integration/Java/Gen.lean index 556b2cd46..cf0ad38ef 100644 --- a/Strata/DDM/Integration/Java/Gen.lean +++ b/Strata/DDM/Integration/Java/Gen.lean @@ -5,7 +5,7 @@ -/ module -import Strata.DDM.AST +public import Strata.DDM.AST import Strata.DDM.Integration.Categories namespace Strata.Java @@ -160,7 +160,7 @@ structure JavaInterface where permits : Array String /-- All generated Java source files for a dialect. -/ -structure GeneratedFiles where +public structure GeneratedFiles where sourceRange : String node : String interfaces : Array (String × String) -- (filename, content) @@ -320,7 +320,7 @@ def generateBuilders (package : String) (dialectName : String) (d : Dialect) (na let methods := d.declarations.filterMap fun | .op op => some (method op) | _ => none s!"package {package};\n\npublic class {dialectName} \{\n{"\n".intercalate methods.toList}\n}\n" -def generateDialect (d : Dialect) (package : String) : Except String GeneratedFiles := do +public def generateDialect (d : Dialect) (package : String) : Except String GeneratedFiles := do let names := assignAllNames d let opsByCategory := groupOpsByCategory d names @@ -367,7 +367,7 @@ def packageToPath (package : String) : System.FilePath := let parts := package.splitOn "." ⟨String.intercalate "/" parts⟩ -def writeJavaFiles (baseDir : System.FilePath) (package : String) (files : GeneratedFiles) : IO Unit := do +public def writeJavaFiles (baseDir : System.FilePath) (package : String) (files : GeneratedFiles) : IO Unit := do let dir := baseDir / packageToPath package IO.FS.createDirAll dir diff --git a/Strata/DL/Lambda/MetaData.lean b/Strata/DL/Lambda/MetaData.lean index 3aa103e53..accee0743 100644 --- a/Strata/DL/Lambda/MetaData.lean +++ b/Strata/DL/Lambda/MetaData.lean @@ -12,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 diff --git a/Strata/DL/SMT/CexParser.lean b/Strata/DL/SMT/CexParser.lean index 74903d459..df11e324f 100644 --- a/Strata/DL/SMT/CexParser.lean +++ b/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}" diff --git a/Strata/DL/SMT/Solver.lean b/Strata/DL/SMT/Solver.lean index ca6f3b0b4..a2502fa23 100644 --- a/Strata/DL/SMT/Solver.lean +++ b/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 diff --git a/Strata/DL/Util/ListUtils.lean b/Strata/DL/Util/ListUtils.lean index 0ce4a31e3..6110803c5 100644 --- a/Strata/DL/Util/ListUtils.lean +++ b/Strata/DL/Util/ListUtils.lean @@ -12,10 +12,10 @@ module /-- Two predicates `P` and `Q` are disjoint, that is, they cannot both hold on a same instance of type `α` -/ -def PredDisjoint (P Q : α → Prop) : Prop := ∀ a, P a → Q a → False +public def PredDisjoint (P Q : α → Prop) : Prop := ∀ a, P a → Q a → False /-- Predicate `P` implies predicate `Q` -/ -def PredImplies (P Q : α → Prop) : Prop := ∀ a, P a → Q a +public def PredImplies (P Q : α → Prop) : Prop := ∀ a, P a → Q a /-- A list with global properties (`π`) and element-wise properties (`πs`). The @@ -24,7 +24,7 @@ def PredImplies (P Q : α → Prop) : Prop := ∀ a, P a → Q a Usually, the global property makes use of the `Forall` predicate. -/ -class ListP {α : Type} (π : α → Prop) (πs : List α → Prop) where +public class ListP {α : Type} (π : α → Prop) (πs : List α → Prop) where split : ∀ {a : α} , πs (a :: as) → π a ×' πs as /-- A `mapM` function that keeps track of the fact that the function is applied @@ -38,7 +38,7 @@ def mapM₁ {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} Enable attaching the instance itself to properties about the instance. See `WFProcedure` and `WFProgram`. -/ -class Wrapper (α : Type) where +public class Wrapper (α : Type) where self : α open List @@ -54,15 +54,15 @@ public def Forall (p : α → Prop) : List α → Prop | x :: l => p x ∧ Forall p l @[simp] -theorem List.Forall_cons (p : α → Prop) (x : α) : ∀ l : List α, Forall p (x :: l) ↔ p x ∧ Forall p l +public theorem List.Forall_cons (p : α → Prop) (x : α) : ∀ l : List α, Forall p (x :: l) ↔ p x ∧ Forall p l | [] => (and_iff_left_of_imp fun _ ↦ trivial).symm | _ :: _ => Iff.rfl -theorem List.Forall_mem_iff : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p x +public theorem List.Forall_mem_iff : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p x | [] => (iff_true_intro <| forall_mem_nil _).symm | x :: l => by rw [List.forall_mem_cons, List.Forall_cons, List.Forall_mem_iff] -theorem List.Forall_append : Forall P (a ++ b) ↔ Forall P a ∧ Forall P b := by +public theorem List.Forall_append : Forall P (a ++ b) ↔ Forall P a ∧ Forall P b := by apply Iff.intro . induction a <;> simp [Forall] case cons h t ih => @@ -82,7 +82,7 @@ theorem List.Forall_append : Forall P (a ++ b) ↔ Forall P a ∧ Forall P b := * `replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]` Adapted from List.replace -/ -def List.replaceAll [BEq α] : List α → α → α → List α +public def List.replaceAll [BEq α] : List α → α → α → List α | [], _, _ => [] | a::as, b, c => match b == a with | true => c :: replaceAll as b c @@ -95,27 +95,27 @@ Taken from https://github.com/leanprover-community/batteries/blob/3613427d66262c public def List.Disjoint (l₁ l₂ : List α) : Prop := ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False -theorem List.removeAll_Sublist [BEq α] {xs ys : List α}: +public theorem List.removeAll_Sublist [BEq α] {xs ys : List α}: (xs.removeAll ys).Sublist xs := by induction xs case nil => simp_all case cons h t ih => simp [List.removeAll] -theorem List.removeAll_Disjoint [BEq α] [LawfulBEq α] {xs ys : List α}: +public theorem List.removeAll_Disjoint [BEq α] [LawfulBEq α] {xs ys : List α}: (xs.removeAll ys).Disjoint ys := by induction xs <;> simp [removeAll, Disjoint] at * -theorem List.Disjoint.mono (h₁ : a.Sublist b) (h₂ : c.Sublist d) : +public theorem List.Disjoint.mono (h₁ : a.Sublist b) (h₂ : c.Sublist d) : Disjoint b d → Disjoint a c := λ Hdis _ Hin1 Hin2 ↦ Hdis (Sublist.mem Hin1 h₁) (Sublist.mem Hin2 h₂) -theorem List.Disjoint.mono_left (h : a.Sublist b) : +public theorem List.Disjoint.mono_left (h : a.Sublist b) : Disjoint b c → Disjoint a c := λ Hdis ↦ mono h (Sublist.refl c) Hdis -theorem List.Disjoint.mono_right (h : c.Sublist d) : +public theorem List.Disjoint.mono_right (h : c.Sublist d) : Disjoint a d → Disjoint a c := λ Hdis ↦ mono (Sublist.refl a) h Hdis -theorem List.Disjoint.removeAll [BEq α] [LawfulBEq α ] {xs ys zs: List α} : +public theorem List.Disjoint.removeAll [BEq α] [LawfulBEq α ] {xs ys zs: List α} : Disjoint xs ys → Disjoint (zs ++ xs) (ys.removeAll zs) := by intros Hdisj a Hin1 Hin2 simp_all only [mem_append] @@ -129,17 +129,17 @@ theorem List.Disjoint.removeAll [BEq α] [LawfulBEq α ] {xs ys zs: List α} : . have Hsub := List.removeAll_Sublist (xs:=ys) (ys:=zs) exact Sublist.mem Hin2 Hsub -theorem List.Disjoint_cons_head : (h :: t).Disjoint l → ¬h ∈ l := by +public theorem List.Disjoint_cons_head : (h :: t).Disjoint l → ¬h ∈ l := by intros Hdis Hin simp [Disjoint] at Hdis exact Hdis.1 Hin -theorem List.Disjoint_cons_tail : (h :: t).Disjoint l → t.Disjoint l := by +public theorem List.Disjoint_cons_tail : (h :: t).Disjoint l → t.Disjoint l := by intros Hdis Hin simp [Disjoint] at Hdis exact Hdis.2 Hin -theorem List.Disjoint_app : +public theorem List.Disjoint_app : List.Disjoint l1 l ∧ l2.Disjoint l ↔ (l1 ++ l2).Disjoint l := by apply Iff.intro . induction l1 @@ -170,7 +170,7 @@ theorem List.Disjoint_app : . specialize ih (Disjoint_cons_tail Hnin) exact ih.2 -theorem List.Disjoint_Nodup_iff : +public theorem List.Disjoint_Nodup_iff : List.Nodup a ∧ b.Nodup ∧ a.Disjoint b ↔ (a ++ b).Nodup := by apply Iff.intro . intros H @@ -193,29 +193,29 @@ theorem List.Subset.empty : [].Subset s := by /-- From Mathlib4 https://github.com/leanprover-community/mathlib4/blob/ccca47289b3f94a9572a38975e0876c139690a21/Mathlib/Data/List/Lattice.lean#L39-L40 -/ -theorem List.Disjoint.symm : Disjoint a b → Disjoint b a := fun H _ Hin1 Hin2 => H Hin2 Hin1 +public theorem List.Disjoint.symm : Disjoint a b → Disjoint b a := fun H _ Hin1 Hin2 => H Hin2 Hin1 theorem List.Disjoint.symm_app (d : Disjoint l (l₁ ++ l₂)) : Disjoint l (l₂ ++ l₁) := fun _ Hin1 Hin2 => d Hin1 (mem_append.mpr $ Or.symm (mem_append.mp Hin2)) -theorem List.Disjoint_Subset_right : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by +public theorem List.Disjoint_Subset_right : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by intros Hdis Hsub simp [Disjoint, List.Subset] at * intros a Hin1 Hin2 specialize Hdis Hin1 simp_all -theorem List.Disjoint_Subset_left : Disjoint vs ks → List.Subset vs' vs → vs'.Disjoint ks := by +public theorem List.Disjoint_Subset_left : Disjoint vs ks → List.Subset vs' vs → vs'.Disjoint ks := by intros Hdis Hsub apply List.Disjoint.symm apply Disjoint_Subset_right (Disjoint.symm Hdis) Hsub -theorem List.Disjoint_Subsets : Disjoint vs ks → List.Subset vs' vs → List.Subset ks' ks → vs'.Disjoint ks' := by +public theorem List.Disjoint_Subsets : Disjoint vs ks → List.Subset vs' vs → List.Subset ks' ks → vs'.Disjoint ks' := by intros Hdis Hsub1 Hsub2 exact List.Disjoint_Subset_left (Disjoint_Subset_right Hdis Hsub2) Hsub1 -theorem List.DisjointAppLeft' : +public theorem List.DisjointAppLeft' : Disjoint vs (ks ++ ks') → Disjoint vs ks' := by intros Hdist h simp [Disjoint] at * @@ -223,33 +223,33 @@ theorem List.DisjointAppLeft' : specialize Hdist Hin1 simp_all -theorem List.DisjointAppRight' : +public theorem List.DisjointAppRight' : List.Disjoint vs (ks ++ ks') → List.Disjoint vs ks := by intros Hdist have Hdist' := List.Disjoint.symm_app Hdist exact List.DisjointAppLeft' Hdist' -theorem List.Subset.subset_app_of_or_2 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 → l ⊆ l1 ++ l2 := by +public theorem List.Subset.subset_app_of_or_2 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 → l ⊆ l1 ++ l2 := by simp [Subset, List.Subset] intro H a Ha cases H <;> simp_all -theorem List.Subset.subset_app_of_or_3 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 → l ⊆ l1 ++ l2 ++ l3 := by +public theorem List.Subset.subset_app_of_or_3 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 → l ⊆ l1 ++ l2 ++ l3 := by simp [Subset, List.Subset] intro H a Ha cases H <;> try (rename_i H; cases H) any_goals simp_all -theorem List.Subset.subset_app_of_or_4 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 ∨ l ⊆ l4 → l ⊆ l1 ++ l2 ++ l3 ++ l4 := by +public theorem List.Subset.subset_app_of_or_4 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 ∨ l ⊆ l4 → l ⊆ l1 ++ l2 ++ l3 ++ l4 := by simp [Subset, List.Subset] intro H a Ha cases H <;> try (rename_i H; cases H <;> try (rename_i H; cases H)) any_goals simp_all -theorem List.Subset.assoc {l: List α}: l ⊆ l1 ++ l2 ++ l3 ↔ l ⊆ l1 ++ (l2 ++ l3) := by +public theorem List.Subset.assoc {l: List α}: l ⊆ l1 ++ l2 ++ l3 ↔ l ⊆ l1 ++ (l2 ++ l3) := by simp [Subset, List.Subset] -theorem List.replaceAll_app {α : Type} [DecidableEq α] {h h' : α} {as bs : List α}: +public theorem List.replaceAll_app {α : Type} [DecidableEq α] {h h' : α} {as bs : List α}: List.replaceAll as h h' ++ List.replaceAll bs h h' = List.replaceAll (as ++ bs) h h' := by induction as generalizing bs case nil => simp [List.replaceAll] @@ -267,7 +267,7 @@ theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} : xs.removeAll ys := by simp [List.removeAll, List.filter_cons] -theorem List.app_removeAll {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: +public theorem List.app_removeAll {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: (xs₁ ++ xs₂).removeAll ys = (xs₁.removeAll ys) ++ (xs₂.removeAll ys) := by induction xs₁ <;> simp_all @@ -277,7 +277,7 @@ theorem List.app_removeAll {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by simp [List.removeAll] -theorem List.removeAll_app {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: +public theorem List.removeAll_app {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: ys.removeAll (xs₁ ++ xs₂) = (ys.removeAll xs₁).removeAll xs₂ := by induction ys @@ -293,7 +293,7 @@ theorem List.removeAll_app {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: simp [cons_removeAll] exact HH -theorem List.removeAll_comm {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: +public theorem List.removeAll_comm {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: (ys.removeAll xs₂).removeAll xs₁ = (ys.removeAll xs₁).removeAll xs₂ := by @@ -314,13 +314,13 @@ theorem List.removeAll_comm {α : Type} [BEq α] {xs₁ xs₂ ys : List α}: /-- From Mathlib4 https://github.com/leanprover-community/mathlib4/blob/e70dc4ede17dd5fcda9926c84268e0f270147cba/Mathlib/Data/List/Zip.lean#L32-L37 -/ @[simp] -theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (List.zip l₁ l₂).map Prod.swap = List.zip l₂ l₁ +public theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (List.zip l₁ l₂).map Prod.swap = List.zip l₂ l₁ | [], _ => List.zip_nil_right.symm | l₁, [] => by rw [List.zip_nil_right]; rfl | a :: l₁, b :: l₂ => by simp only [List.zip_cons_cons, List.map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk] -theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: List α}: +public theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: List α}: k ∈ (t.replaceAll h h') → k ∈ t ∨ k = h' := by intros Hr induction t generalizing k h h' <;> simp [List.replaceAll] at * @@ -337,21 +337,21 @@ theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: L specialize ih hin cases ih <;> simp_all -theorem zip_self_eq : +public theorem zip_self_eq : (k1, k2) ∈ List.zip ks ks → k1 = k2 := by intros Hin induction ks <;> simp_all case cons h t ih => cases Hin <;> simp_all -theorem zip_self_eq' : +public theorem zip_self_eq' : k ∈ ks → (k, k) ∈ List.zip ks ks := by intros Hin induction ks <;> simp_all case cons h t ih => cases Hin <;> simp_all -theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 : α} {vs t: List α}: +public theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 : α} {vs t: List α}: k2 ∈ (vs.replaceAll h h').removeAll t → k2 = h' ∨ k2 ∈ vs.removeAll t := by intros H induction vs generalizing k2 <;> simp [List.removeAll, List.replaceAll] at * @@ -369,7 +369,7 @@ theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 : have Hor := replaceAll_mem Hin cases Hor <;> simp_all -theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t : List α} : +public theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t : List α} : k ≠ h → k ∈ List.removeAll vs t → k ∈ List.removeAll vs (h :: t) := by @@ -378,11 +378,11 @@ theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t : case cons h' t' ih => simp_all -theorem removeAll_sublist {α : Type u} [BEq α] [LawfulBEq α] (as bs : List α): +public theorem removeAll_sublist {α : Type u} [BEq α] [LawfulBEq α] (as bs : List α): (List.removeAll as bs).Sublist as := by induction as <;> simp [List.removeAll] -theorem replaceAll_not_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' : α} {vs : List α}: +public theorem replaceAll_not_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' : α} {vs : List α}: h ≠ h' → ¬ h ∈ (vs.replaceAll h h') := by intros Hne Hin @@ -399,7 +399,7 @@ theorem replaceAll_not_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' : α} {vs have hne := ne_of_beq_false hne simp_all -theorem List.mem_zip_1 {l₁ : List α} {l₂ : List β} : +public theorem List.mem_zip_1 {l₁ : List α} {l₂ : List β} : l₁.length = l₂.length → a ∈ l₁ → ∃ b, (a, b) ∈ l₁.zip l₂ := by intros Hlen Hin @@ -415,7 +415,7 @@ case cons h t ih => | intro b Hin => refine ⟨b, Or.inr Hin⟩ -theorem List.mem_zip_2 {l₁ : List α} {l₂ : List β} : +public theorem List.mem_zip_2 {l₁ : List α} {l₂ : List β} : l₁.length = l₂.length → b ∈ l₂ → ∃ a, (a, b) ∈ l₁.zip l₂ := by intros Hlen Hin @@ -434,7 +434,7 @@ case cons h t ih => theorem List.PredDisjoint_comm : PredDisjoint P Q → PredDisjoint Q P := fun H x Hq Hp => H x Hp Hq -theorem List.PredDisjoint_Disjoint : +public theorem List.PredDisjoint_Disjoint : Forall P as → Forall Q bs → PredDisjoint P Q → @@ -444,31 +444,31 @@ apply Hdis x . exact (List.Forall_mem_iff.mp H1) x Hin1 . exact (List.Forall_mem_iff.mp H2) x Hin2 -theorem List.Forall_PredImplies : +public theorem List.Forall_PredImplies : Forall P as → PredImplies P Q → Forall Q as := by intros Hp Hpq apply List.Forall_mem_iff.mpr intros x Hin exact Hpq _ (List.Forall_mem_iff.mp Hp x Hin) -theorem List.PredDisjoint_PredImplies_left : +public theorem List.PredDisjoint_PredImplies_left : PredDisjoint R Q → PredImplies P R → PredDisjoint P Q := by intros Hdis Himp a Hp Hq exact Hdis a (Himp a Hp) Hq -theorem List.PredDisjoint_PredImplies_right : +public theorem List.PredDisjoint_PredImplies_right : PredDisjoint P R → PredImplies Q R → PredDisjoint P Q := by intros Hdis Himp a Hp Hq exact Hdis a Hp (Himp a Hq) -theorem List.Forall_filter : +public theorem List.Forall_filter : Forall (P ·) (List.filter P l) := by apply Forall_mem_iff.mpr intros x Hin simp at Hin exact Hin.2 -theorem List.Forall_flatMap : +public theorem List.Forall_flatMap : Forall (fun x => Forall P (f x)) ls ↔ Forall P (List.flatMap f ls) := by apply Iff.intro . induction ls <;> simp [Forall] diff --git a/Strata/DL/Util/Nodup.lean b/Strata/DL/Util/Nodup.lean index 9a726612d..7dc21b3d5 100644 --- a/Strata/DL/Util/Nodup.lean +++ b/Strata/DL/Util/Nodup.lean @@ -72,17 +72,17 @@ theorem nodup_notin : (l ++ h :: l').Nodup → ¬h ∈ l ∧ ¬ h ∈ l' := by specialize left h' unfold Not; intros Heq; simp_all -theorem nodup_swap : +public theorem nodup_swap : List.Nodup (l ++ l') → List.Nodup (l' ++ l) := by intros Hnodup simp [List.Nodup] at * refine (List.pairwise_append_comm ?_).mp Hnodup exact fun {x y} a a_1 => a (Eq.symm a_1) -theorem nodup_swap' : +public theorem nodup_swap' : List.Nodup (l ++ l') = List.Nodup (l' ++ l) := propext ⟨nodup_swap, nodup_swap⟩ -theorem nodup_reverse : +public theorem nodup_reverse : List.Nodup l → List.Nodup l.reverse := by intros Hnodup simp [List.Nodup] at * @@ -93,20 +93,20 @@ theorem nodup_reverse : cases Hnodup with | intro left _ => exact fun a => left a' Ha' (Eq.symm a) -theorem nodup_reverse' : +public theorem nodup_reverse' : List.Nodup l.reverse → List.Nodup l:= by intros Hnodup rw [← @List.reverse_reverse _ l] exact nodup_reverse Hnodup -theorem nodup_middle: +public theorem nodup_middle: List.Nodup (l ++ h :: l') → List.Nodup (h :: (l ++ l')) := by intros Hnodup simp only [List.Nodup] at * refine (List.pairwise_middle fun {x y} a => (Ne.symm a)).mp ?_ simp_all -theorem nodup_middle': +public theorem nodup_middle': List.Nodup (h :: (l ++ l')) → List.Nodup (l ++ h :: l') := by intros Hnodup simp only [List.Nodup] at * @@ -212,7 +212,7 @@ theorem loop_insert_nodup : ∀ α {h : α} {t l l': List α} [BEq α] [LawfulBE simp_all exact fun a => heq' (Eq.symm a) -theorem eraseDups_Nodup : ∀ α {l : List α} [BEq α] [LawfulBEq α], l.eraseDups.Nodup := by +public theorem eraseDups_Nodup : ∀ α {l : List α} [BEq α] [LawfulBEq α], l.eraseDups.Nodup := by intros α l inst inst2 simp [List.eraseDups] induction l @@ -269,7 +269,7 @@ theorem eraseDupsBy.loop_mem_as {α : Type u} [BEq α] [LawfulBEq α] {h : α} { apply ih exact List.not_mem_cons_of_ne_of_not_mem (fun a => hne (Eq.symm a)) Hnin -theorem eraseDupsBy.sound {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α}: +public theorem eraseDupsBy.sound {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α}: a ∈ as → a ∈ as.eraseDups := by intros Hin simp [List.eraseDups] @@ -293,7 +293,7 @@ case cons h t ih => apply loop_mem_as ?_ eq simp_all -theorem filter_nodup : as.Nodup → (List.filter p as).Nodup := by +public theorem filter_nodup : as.Nodup → (List.filter p as).Nodup := by intros H induction as <;> simp [List.filter] case cons h t ih => diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean index 53c349a0b..b36ec7051 100644 --- a/Strata/Languages/Core/Options.lean +++ b/Strata/Languages/Core/Options.lean @@ -47,7 +47,7 @@ public structure Options where /-- Solver time limit in seconds -/ solverTimeout : Nat -def Options.default : Options := { +public def Options.default : Options := { verbose := .normal, parseOnly := false, typeCheckOnly := false, @@ -60,8 +60,8 @@ def Options.default : Options := { instance : Inhabited Options where default := .default -def Options.quiet : Options := +public def Options.quiet : Options := { Options.default with verbose := .quiet } -def Options.debug : Options := +public def Options.debug : Options := { Options.default with verbose := .debug } diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean index 372b2d305..ca95ca2fa 100644 --- a/Strata/Languages/Core/Verifier.lean +++ b/Strata/Languages/Core/Verifier.lean @@ -407,7 +407,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option def verify (smtsolver : String) (program : Program) (tempDir : System.FilePath) - (options : Options := Options.default) + (options : Options := default) (moreFns : @Lambda.Factory CoreLParams := Lambda.Factory.default) : EIO Format VCResults := do match Core.typeCheckAndPartialEval options program moreFns with @@ -428,7 +428,7 @@ namespace Strata open Lean.Parser -def typeCheck (ictx : InputContext) (env : Program) (options : Options := Options.default) +def typeCheck (ictx : InputContext) (env : Program) (options : Options := default) (moreFns : @Lambda.Factory Core.CoreLParams := Lambda.Factory.default) : Except Std.Format Core.Program := do let (program, errors) := TransM.run ictx (translateProgram env) @@ -446,7 +446,7 @@ def Core.getProgram def verify (smtsolver : String) (env : Program) (ictx : InputContext := Inhabited.default) - (options : Options := Options.default) + (options : Options := default) (moreFns : @Lambda.Factory Core.CoreLParams := Lambda.Factory.default) (tempDir : Option String := .none) : IO Core.VCResults := do diff --git a/Strata/Languages/Dyn/DDMTransform/Translate.lean b/Strata/Languages/Dyn/DDMTransform/Translate.lean index 23218b125..5fc2f1c53 100644 --- a/Strata/Languages/Dyn/DDMTransform/Translate.lean +++ b/Strata/Languages/Dyn/DDMTransform/Translate.lean @@ -4,6 +4,8 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module + -- TODO: Translation from concrete syntax to abstract syntax namespace Strata diff --git a/Strata/Languages/Dyn/Verify.lean b/Strata/Languages/Dyn/Verify.lean index 1ea5a2fec..536c9d4d8 100644 --- a/Strata/Languages/Dyn/Verify.lean +++ b/Strata/Languages/Dyn/Verify.lean @@ -4,6 +4,8 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module + -- TODO: Verification integration for Dyn language import Strata.Languages.Dyn.Dyn diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 19606899b..c568304ca 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -470,7 +470,7 @@ def translate (program : Program) : Except (Array DiagnosticModel) Core.Program Verify a Laurel program using an SMT solver -/ def verifyToVcResults (smtsolver : String) (program : Program) - (options : Options := Options.default) + (options : Options := default) (tempDir : Option String := .none) : IO (Except (Array DiagnosticModel) VCResults) := do let strataCoreProgramExcept := translate program diff --git a/Strata/Languages/Python/Regex/ReParser.lean b/Strata/Languages/Python/Regex/ReParser.lean index 1bc31796e..5f24decff 100644 --- a/Strata/Languages/Python/Regex/ReParser.lean +++ b/Strata/Languages/Python/Regex/ReParser.lean @@ -4,6 +4,8 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +module + namespace Strata namespace Python @@ -19,6 +21,8 @@ for a reference implementation. ------------------------------------------------------------------------------- +public section + inductive ParseError where /-- `patternError` is raised when Python's `re.patternError` exception is @@ -310,5 +314,7 @@ set_option backwards.match.sparseCases true def parseTop (s : String) : Except ParseError RegexAST := parseGroup s 0 none |>.map (fun (r, _) => r) +end -- public section + ------------------------------------------------------------------------------- end Strata.Python From 097c13e4f7aaa12b65592f92f1a13ee7272d1ef0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 5 Feb 2026 14:48:47 +0000 Subject: [PATCH 9/9] Add missing publics --- Strata/Languages/Core/Options.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean index a84998249..153bd6add 100644 --- a/Strata/Languages/Core/Options.lean +++ b/Strata/Languages/Core/Options.lean @@ -11,13 +11,13 @@ public inductive VerboseMode where | debug deriving Inhabited, Repr, DecidableEq -def VerboseMode.toNat (v : VerboseMode) : Nat := +public def VerboseMode.toNat (v : VerboseMode) : Nat := match v with | .quiet => 0 | .normal => 1 | .debug => 2 -def VerboseMode.ofBool (b : Bool) : VerboseMode := +public def VerboseMode.ofBool (b : Bool) : VerboseMode := match b with | false => .quiet | true => .normal