ethos-eoc takes a proof calculus written in Eunoia and compiles it: into a proof checker for that calculus, and into the obligations that say the calculus is sound.

This is experimental work alongside the human-maintained Ethos checker. The question is whether a calculus and its model semantics can produce usable checker code and soundness obligations from the same input. Its goals are to compile signatures, generate obligations, and keep that translation testable. It does not prove every generated obligation, define the Eunoia language, or establish equivalence with the C++ checker.

The compiler reuses Ethos's parser and plugin API. Its C++ implementation lives under plugins/, and the parent's CI builds it and runs the child regressions; it is therefore not isolated from the parent build infrastructure. It remains experimental, with any change in its status reserved for the human maintainers.

What is where in this project: compiler/ holds the implementation -- the configuration compiler, the language it reads and what it writes -- and semantics/ the sets the tool ships. driver.py is the entry point, and is the one path a caller of another tree names, so it stands here rather than beside the modules it drives. docs/ and test/ hold the pages and the regressions; out/ is what a run writes and is not checked in.

As of 2026-09-18, Logos uses this compiler to regenerate calculus modules; its hand-written specification and checked proofs determine what the resulting checker establishes. The documentation index covers the compiler's pages. The Ethos user manual remains the account of the language supported by the checker.

A run names the signature to compile and, separately, what its symbols mean. The local regressions compile tests/Booleans-rules.eo and tools/eoc/test/nary-nil.eo using semantics/development-cpc.eos. There are no CPC wrapper scripts in this checkout. As of 2026-09-18, Logos supplies its CPC semantics at install/defs/Cpc.eos; pass that file explicitly when compiling against that development. A new calculus can reuse the compiler's existing embedding, but operations outside that embedding can require compiler changes.

Whichever calculus it is, it compiles to each of these targets, from one description of what its symbols mean:

The calculus and backend are separate: a target is a backend rather than a restatement of the calculus, and a calculus is a description rather than another compiler. What a symbol means is written once, as configuration, and every target is compiled from it; new symbols within the supported embedding can reach each target through configuration. Generated lemmas still require proofs, and solver results are relative to the generated encoding and the chosen semantics.

The configuration language has a reference -- the grammar, every entry with the attributes it may carry, the four vocabularies a body may be written in and how one is cast between them, what the compiler checks, worked examples, and what every diagnostic means. It is maintained in the eunoia repository, by its sapheneia project, and not in this tree.

Almost all work on a calculus is an edit to one of those files rather than a change to anything here, and a target is reached by writing configuration rather than by writing a compiler, so that is the page to have open. The sets are tools/eoc/semantics/ for what a calculus and SMT-LIB mean, and the .eos beside each stage under plugins/ for what that stage is told.

tools/eoc/driver.py is the entrypoint for all of them, and exposes them as one documented interface. See Quick start to run one, and the proof pipeline for where this sits in the wider cvc5 proof pipeline.

ethos-eoc is the Eunoia binary built with the compiler plugins, one to a stage:

• desugar
• trim-defs
• model-smt
• smt-meta
• lean-meta

The default ethos build does not include them: it checks proofs, and this one compiles the calculus the proofs are written in. Build it with the two commands under Building ethos-eoc.

model-smt gives every symbol of the signature its SMT-LIB semantics. A symbol that instead has no semantics of its own is eliminated on the way to the SMT-LIB term layer, i.e. it is defined in terms of the other symbols of the signature. Such a reduction is written in the syntax of the signature itself, as an ordinary define whose name is $eo_reduce_ followed by the symbol it reduces.

What a symbol means to the model is said by two files, and a run may name either: the semantics of the input with --semantics, and the SMT-LIB semantics it is written against with --smt-semantics.

tools/eoc/out/smt_defs.eo   the SMT-LIB semantics, written in the embedding
tools/eoc/out/user_defs.eo  how the input's symbols transform into it

Both are generated, from the configuration under tools/eoc/semantics, which tools/eoc/compiler/sem_compile.py compiles before any stage runs; neither is checked in. What the options name is therefore the central file of a configuration set rather than what it compiles to:

python3 tools/eoc/driver.py lean --all \
  --semantics tools/eoc/semantics/development-cpc.eos \
  <cvc5>/proofs/eo/cpc/Cpc.eo

A file that is not a central file is taken to be a signature already written out and is passed through, which is what lets one that has no configuration still be given directly. See the .eos reference for what the configuration is and the language it is written in.

A run compiles one set of each role, and the set an option names stands in for the one the tool ships with rather than compiling beside it. Where a set compiles to is said by its role and by nothing else, so the generated files have the names above whatever a run names and wherever the sets stand.

The model-smt stage reads these two signatures. The separate user_desugar.eo file supplies predicates to the earlier desugar stage. A symbol the input declares that the file says nothing about is an error rather than a term the model would silently say nothing about. The plugin ships with the SMT-LIB semantics but with no signature of an input, so a run that names none is an error once that stage runs.

Pass --semantics for model compilation. The quick-start examples below use the local development semantics explicitly; for another calculus, supply a set describing that input.

Each is a sequence of blocks, one per symbol, opened by a ; -- X line. For a symbol X, smt_defs.eo gives the constructor $emb_sm.X and the macro $sm_X, the cases X contributes to $smtx_typeof and to $smtx_model_eval (as $eoc_typeof_X and $eoc_eval_X), and the auxiliary programs those cases call. user_defs.eo gives $eoc_transform_X, the cases X contributes to $eo_to_smt, and $eoc_transform_type_X for a type constructor.

What a block says to the compiler is named $eoc_, which is what tells it apart from what the compiler emits: the case of an $eoc_ program is spliced into the aggregate its family names, so the name itself never reaches the generated file. Nil predicates are separate programs named $eo_is_list_nil_X, written to user_desugar.eo and inserted by the driver before the desugar output calls them.

Which families there are is not something either side knows by name. The head of each generated file declares them, one line to an aggregate:

; $eoc-aggregate $smtx_typeof $eoc_typeof_ $SMT_TYPEOF_CASES$
; $eoc-aggregate $smtx_model_eval $eoc_eval_ $SMT_EVAL_CASES$

which says the aggregate a case joins, the name the case is written under, and the marker of plugins/model_smt/model_smt.eo the stage writes them at; the longest matching case prefix identifies the aggregate a program belongs to. The lines are compiled from plugins/model_smt/model_smt.eos, which is where an aggregate is to be changed or added, and the stage reads them rather than knowing any of it, so adding one asks nothing of ethos-eoc. See the .eos reference.

A block may also be of a helper rather than of a symbol, in which case the ; -- X line names the helper itself, e.g. ; -- $smtx_typeof_bv_op_2 for the typing of a bit-vector operator whose two arguments must be of one width. Such a block is taken only when a block that is kept names it, so a signature with no bit-vectors in it compiles to a model that has never heard of them.

A helper belongs in the signature when only theory operators call it. That is the whole of what a signature may hold beside its symbols: a set says what a theory does and never what the embedding is, so it writes programs and never a declaration, and a form that is neither is refused rather than carried over as the text it is; see the .eos reference. The programs over a map -- looking an entry up, typing one, saying whether one is written the one way -- are therefore written in the configuration beside the sort they belong to, while the $smt_Map they are written over is declared in plugins/model_smt/model_smt.eo with the rest of the embedding.

What remains in plugins/model_smt/model_smt.eo is what says what the embedding is, and what no theory is what asks for:

• the term, type and value languages the file declares itself -- the shapes a value is built over among them -- and the aggregates written over them;
• the datatypes, which an input declares rather than a theory naming, and the types the embedding keeps for what an input declares -- USort, FunType, DtcAppType, TypeRef;
• the binders, an application, and the programs over types that everything else is written against -- well-foundedness, boundedness and the default of a type.

Every helper a signature writes is emitted together, before the first aggregate whose cases may call one; they are one stream because they are one dependency graph, and what orders them is the signature itself, which writes a program after the ones it calls. See $SMT_HELPER_PROGS$ in the template.

The stage takes the blocks of the symbols the input declares, together with every block those name, and puts what each says where it belongs; it knows nothing about any symbol itself. A block is copied as text, which is what keeps the definitions of the embedding it names, e.g. $vsm_bool, from being expanded on the way. See plugins/model_smt/defs_reader.h.

Both files are ordered so that a symbol follows the ones its cases name, which is why neither needs a forward declaration. Adding, changing or removing a symbol is a change to one block and does not require rebuilding ethos-eoc.

A block may name a symbol of the input rather than of the embedding, as the transformation of @quantifiers_skolemize names forall in the pattern it matches. Trimming a signature to one proof rule has to keep such a symbol, so the driver reads those dependencies off the blocks and tells trim-defs; see Pipeline.defs_depends in tools/eoc/driver.py. The blocks a set writes for the desugar stage are read the same way, since they are spliced into a trimmed signature too: the nil predicate of str.++ names seq.empty, and a run that keeps the one has to keep the other. See head_lines in tools/eoc/compiler/sem_compile.py, which writes both.

A block may also say that the compilation has no place for what it is of at all: SMT-LIB gives a proof-level binder no meaning, so lambda and everything that reduces an application of one are left out rather than modelled. A block says so with directives of the following forms:

(echo "eoc-exclude symbol lambda")
(echo "eoc-exclude method $beta_reduce")
(echo "eoc-exclude rule beta-reduce")

The configuration writes :exclude on the symbol, the method or the rule itself -- a method with define-method and a rule with define-rule -- and the compiler puts the directive back, the kind being what the form that declared it says one is; see the .eos reference.

Pipeline.defs_excludes collects them and gives them to the desugar stage, which is what drops what they name; a rule among them is also left out of --all-rules, since there is nothing to verify about it. The names are matched literally: the compiler neither checks that a name exists nor computes a dependency closure, so every declaration that goes with an omitted one says so for itself.

Lean has to be told why a recursive definition terminates whenever it cannot see this for itself, and no measure the compiler could guess would do for the programs that need one. So the clause is stated as the Lean text it is, under :lean in the configuration set of the signature the program is of (see the .eos reference), and the lean-meta stage appends it to the definition of the program it names:

tools/eoc/out/smt_termination.lean   the programs of the deep embedding, which
                                     every input is compiled through; read by
                                     the stage itself
tools/eoc/out/user_termination.lean  the programs of the input signature,
                                     passed to the stage by the driver

Both are generated by sem_compile.py, so what is to be changed is the :lean attribute of the set. A block of one runs from a line naming one or more programs, written -- $name ..., to the next comment line, and what lies between is the clause. An input whose programs all recurse structurally needs no clauses of its own; a signature given already written out rather than as a configuration names its clauses with --lean-config. Without clauses the generated Lean simply carries none for those programs, which Lean will reject if one was needed.

A clause may not name the native layer, which the compiler checks. It is text the stage appends rather than text the stage printed, so naming a definition of the layer there asks for nothing: the definition may have been dropped as unreached, see "The native layer" below. Every native type abbreviates a Lean type, which is what a measure writes instead.

What a signature written in the embedding may call that no compiler writes is declared in plugins/desugar/natives.eos, one entry to a native:

(declare-native binary_and ((w <numeral>) (n1 <numeral>) (n2 <numeral>)))
(declare-native z_zero () :op "0")

sem_compile.py compiles that set into tools/eoc/out/native_defs.eo, the declarations the desugar layer carries, which stand where the (include "native_defs.eo") of plugins/desugar/native_embed.eo names them. Nothing writes one by hand: a declaration says only the name, what each argument is and the operator it forwards to, and the set says all three.

A native is written under one name and comes out under several, one per place it reaches. Taking zplus, which the embedding calls where a signature adds two numerals:

The eo-meta backend is the one that adds no spelling of its own: what it writes is Eunoia, and Eunoia already calls it $native_zplus.

A definition a Lean block writes for itself, rather than the one it declares, is named impl_native_ instead, which is what says it is private to that block: impl_native_int_log_rec is nothing a signature may reach.

Where a name is spelled is settled in LAYERS in tools/eoc/compiler/sem_compile.py, one entry to a backend.

What is left in native_embed.eo is what the embedding is rather than what it calls, and nothing else: the $native_apply_*, $native_type_* and $native_embed_* constructors, declared and never written over. It holds no definition at all.

Everything else the set says. It declares the primitive types the natives are written over as well as the natives themselves -- <numeral> is what a configuration calls what a backend calls Int -- so that a set says the kind of thing it means rather than the sort some target happens to have. Three of the six name no SMT-LIB sort at all.

A native that forwards to nothing says what it is instead, under :is, written in the vocabulary every body of a configuration is written in:

(declare-native z_dec ((x1 <numeral>)) :is ("zplus" x1 "z_neg_one"))

What a native that forwards to an operator does is a separate thing, said by each backend in a native layer of its own; see below. The two are apart because neither implies the other: a backend may define what the embedding never calls, and the embedding may call what a backend gets from its own language. A native written with :is needs neither, since what it is has been said once already.

What a backend generates is written against a layer of definitions that gives the deep embedding its arithmetic, its strings, its regular expressions and the rest -- what the generated text is allowed to call and no compiler writes. Each backend has one, and the two are the same thing said twice:

The inductive a datatype of the embedding prints as, and the ordering key beside it, are generated: a constructor the target declares reaches the backend like any other, and the backend gives an inductive to whatever it is handed, named as the type the constructor returns. Nine datatypes come out that way -- the term, the type and the value, and the map, the sequence, the regular language and the three a datatype declaration is made of.

A datatype's constructors are therefore said once, in semantics/smt.eos, and their order there is what the tags of its ordering key are taken from.

A native written with :is is defined in terms of other natives. A native that forwards to a literal needs no backend definition. A primitive operator needs a native-layer definition unless the target language already supplies it.

There is no complete machine-checked register of the latter group. The SMT-LIB layer can use builtin operators such as and, or, not, ite and to_real. An eo-meta native without an implementation falls back to an opaque $native_apply_N. Missing or unused definitions are not comprehensively checked against what each backend supports. See the design notes.

A layer is a configuration set, which tools/eoc/compiler/sem_compile.py compiles; one entry is one definition, under the attribute that says which language it is written in:

(define-native-method str_to_upper
  :lean-impl "def impl_native_char_to_upper (c : native_Char) : native_Char :=
  if 97 <= c && c <= 122 then c - 32 else c

def native_str_to_upper : native_String -> native_String
  | s => s.map impl_native_char_to_upper")

(define-native-method int.to_nat
  :smt-impl "(declare-fun int.to_nat (Int) Nat)
(assert (! (forall ((x Int))
  (! (= (int.to_nat x) (ite (<= x 0) nat.zero (nat.succ (int.to_nat (- x 1)))))
  :pattern ((int.to_nat x))))
  :named smtx.int.to_nat.def))")

The name is spelled the way the embedding names it: the Lean backend puts the native_ back, and the SMT-LIB one forwards the name as it stands, which is why int.to_nat is written under that name there and under int_to_nat in the Lean set. Whatever else an entry defines has no name here and so is private to it, which impl_native_ rather than native_ is what says on the Lean side. A definition that is axiomatised rather than defined -- a declare-fun and the assert that says what it is -- is one entry, since neither half is of any use without the other.

Everything below holds of both layers: what a stage is given is the same file in two languages, and the code that reads it is one class, ethos::NativeLayer in plugins/native_layer.cpp.

Only what the compilation of an input reaches is emitted. Most of a layer is dead for any one input: a signature with no strings in it has no use for the regular-expression matcher, and one of Booleans alone has none for arithmetic. The emitted definitions depend on the selected signature, rules and semantics; a smaller input can omit entire groups of natives and quantified axioms.

A backend has one place per module its generated text is read in, each taking what comes out there as an ordinary replacement:

Which of them a block comes out in is the demand for it: the module that names it, the one they share when two do -- which is the scope every module sees -- and the one module that can hold it when its text names what only that module declares. A block named by a block is named wherever that one comes out, so the demand is closed over what each calls.

Neither of the two things this is read off is the generated text:

• What a block names is read by the compiler, off the block itself, and written on the line that opens it: the scope it cannot be written above, and the rest of the layer it calls. See lean_needs, vc_needs and native_deps in tools/eoc/compiler/sem_compile.py. Reading it there rather than beside the definition is what keeps it from drifting: an annotation can, and the text cannot drift from itself.
• What an input names is what the stage wrote: a name of the layer reaches generated text only by being printed into it, so the stage notes each as it prints it, against the scope the text it is printing comes out in. See NativeLayer::use, and getEmbedName in either stage for where a name is printed.

What no input reaches is what the resources of a stage name themselves -- native_ite in the term ITE of lean_meta_checker.lean, native_Bool in the equality of lean_meta_checker_term.lean. Such a definition says :keep in its set and comes out in the scope every module sees, which is what every resource that names one can see. A resource that names one and does not say so gets generated text naming a definition that was never written, which Lean, or cvc5 reading the verification condition, is what reports.

EO leaves what eo::hash returns underconstrained. This backend supplies no interpretation of hash, and the layer defines no native_thash.

The lean-meta stage therefore refuses to print $eo_hash, the program of the embedding that would call it, the way it refuses $eo_ite; see LeanMetaReduce::finalizeProgram. A signature that uses hash gets generated Lean naming a definition that was never written, and Lean is what reports it -- the stage checks nothing further, since the generated file is not what says whether a name exists. The other backends are unaffected: $native_thash reaches SMT-LIB and SyGuS as the uninterpreted function it is.

ethos-eoc is built by the standalone CMake project in plugins/, which compiles the ethos core sources together with the plugins. The main ethos build is unaffected. From the repository root:

cmake -S plugins -B build-eoc
cmake --build build-eoc --target ethos-eoc -j4

Pass -DCMAKE_BUILD_TYPE=Debug to the configure step for a debug build with assertions and tracing. The driver configures the build directory automatically if it does not exist yet.

--build-dir defaults to the current working directory, so pass it explicitly whenever you invoke the driver from somewhere other than the build tree. The examples below all use build-eoc.

python3 tools/eoc/test/driver.py             # read-only rule listing and errors
python3 tools/eoc/test/regress.py            # say whether the bytes moved
python3 tools/eoc/test/regress.py --update   # take this run as what is written

The compiler is refactored more often than it is extended, and what a refactor has to be is output-preserving. regress.py compiles two signatures of this tree, tests/Booleans-rules.eo and tools/eoc/test/nary-nil.eo, each for one rule, and compares the digest of every file the runs leave behind -- stage files and published artifacts alike -- with what is checked in beside it. A run that changed something says which files it changed. CI runs it on every push.

The second signature is there for the one thing the first cannot reach: its str.++ has a nil that is not ground, which is what makes the desugar stage ask the input's semantics for a nil predicate and so the only thing that exercises inline_called_blocks in tools/eoc/driver.py on a block it has to keep.

What is checked in is the digest of each file rather than the file, since the tree checks in no generated artifact at all; see the tools/eoc/out/ line of .gitignore. The digests are of what the pipeline wrote under these semantics, so a change to semantics/smt.eos or to semantics/development-cpc.eos moves them, and rightly: --update is how a run that meant to change the model says so, and the diff of expected.txt then shows how much of the output that change reached.

The whole-signature path is not covered. No signature in this tree is one the semantics the tool ships with covers entirely, so lean --all over one stops at the first symbol the semantics says nothing about; what covers it is a calculus of another tree.

python3 tools/eoc/compiler/sem_compile.py --check is the other half: it says the generated signatures hold what compiling the configuration writes, and that each block of one stands after the blocks it names.

The driver resolves input paths relative to the directory where you invoke python3 tools/eoc/driver.py, not relative to the build directory.

For example, from the repository root:

python3 tools/eoc/driver.py vc --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos tests/Booleans-rules.eo and_intro

The input path tests/Booleans-rules.eo is interpreted relative to the repository root. The driver writes its EO stage files and final published outputs under tools/eoc/out by default.

Every tool of the pipeline says what it is doing the same way, which matters because the checks that run this compiler live in other repositories -- logos and cvc5 -- and read its output there. One step of a run is a line under -- , what a step is made of is indented two spaces further, and a path is written from the root of the repository, so that a log reads the same whichever machine wrote it. An illustrative fragment:

-- Generating a verification condition
--   [1/4] desugar -> tools/eoc/out/trim-d-example.eo
--   [2/4] model-smt -> tools/eoc/out/vcm-def-example.eo

A path outside the repository -- the signature of a calculus, the tree the Lean is installed into -- is written as it stands, since nothing else would name it.

What went wrong is not a step. It goes to stderr as error: ..., which is what a caller's CI looks for, and the run exits non-zero; a run that carried on regardless says so as warning: .... Anything meant to be read by a program rather than a person -- the rule names of list-rules -- is written plainly to stdout with no prefix at all.

The style is defined in one place, tools/eoc/compiler/report.py, which every tool here reports through.

The driver uses two output trees:

• tools/eoc/out/ for stage EO files and final published outputs, unless overridden with --final-out-dir or EOC_FINAL_OUT_DIR, and for what the configuration compiles to, which stands there whatever a run overrides and is not checked in
• <build-dir>/out/plugins/ for plugin-private generated files consumed by the driver

Published and stage files:

tools/eoc/out/
  smt_defs.eo               what the configuration compiles to, see
  user_defs.eo              eunoia's tools/sapheneia/docs/eos.md
  smt_termination.lean
  user_termination.lean
  lean_native.lean          the native layer of each backend, see above
  smt_vc_native.smt2
  trim-*.eo
  trim-d-*.eo
  vcm-def-*.eo
  vcmt-def-*.eo
  desugar.eo
  lean-*-trim.eo
  lean-*-desugar.eo
  lean-*-defs.eo
  lean-*-final.eo
  trim_defs/trim_gen.eo
  vc/final-*.smt2
  sygus/final-*.sy
  lean/
    Logos.lean
    LogosTerm.lean
    Parser.lean
    SmtEval.lean
    SmtModelDefs.lean
    SmtValueOrder.lean
    SmtModel.lean
    Spec.lean
    Proofs/
      RuleLemmas.lean
      Rules/
        <Rule>.lean

out/lean/ has the layout of the destination package, but is not a Lean package that builds on its own: the generated modules import <Calc>.Proofs.CheckerCore and <Calc>.Proofs.RuleSupport.Support, which the compiler never writes and which belong to that package. The proof-side modules stand under Proofs/, which is what the import <Calc>.Proofs.Rules.<Rule> lines RuleLemmas.lean carries name; every other file stands at the root, where its name already is its import. Installing is therefore a copy of the tree, and a file added to LEAN_OUTPUTS in tools/eoc/driver.py arrives with no change to the install wrappers.

<Calc> is what --calc-name says, which is the name of the package the run installs into; a run that names none calls the calculus after its input file, up to the first dot.

A published module is read by whoever reads the package, so what the resource it was rendered from says to whoever edits the resource -- what a tag stands for, why something is written there rather than where it belongs -- is written as a note, a comment whose text opens with a $: -- $ where the resource is Lean and ; $ where it is SMT-LIB. A note is dropped when the resource is rendered, so it never reaches the package; see dropResourceNotes in plugins/utils.cpp. Everything else a resource writes is published as it stands, and is written to the reader of the package.

Plugin-private files:

<build-dir>/out/plugins/
  desugar/
  lean_meta/
  model_smt/
  smt_meta/
  trim_defs/

Generate one VC:

python3 tools/eoc/driver.py vc --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos tests/Booleans-rules.eo and_intro

Generate one SyGuS query:

python3 tools/eoc/driver.py vc --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos --sygus tests/Booleans-rules.eo and_intro

Generate Lean for selected rules:

python3 tools/eoc/driver.py lean --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos tests/Booleans-rules.eo and_intro contra

Generate Lean for the whole signature:

python3 tools/eoc/driver.py lean --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos --all <cvc5>/proofs/eo/cpc/Cpc.eo

A declaration the signature of the input leaves out of the compilation is dropped by this run without anything being said on the command line; see "The signatures written in the deep embedding" above.

List all rules declared by a signature and its includes:

python3 tools/eoc/driver.py list-rules <cvc5>/proofs/eo/cpc/Cpc.eo

Run every discovered rule through the VC pipeline:

python3 tools/eoc/driver.py batch --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos vc <cvc5>/proofs/eo/cpc/Cpc.eo --all-rules --clean

Run every discovered rule through the SyGuS pipeline:

python3 tools/eoc/driver.py batch --build-dir build-eoc --semantics tools/eoc/semantics/development-cpc.eos sygus <cvc5>/proofs/eo/cpc/Cpc.eo --all-rules --clean

INPUT, RULE and SEMANTICS below are placeholders for the signature, rule and input semantics configuration. The CLI definitions in driver.py are the source for option names; this reference is not mechanically compared with --help.

Generate a single SMT2 VC for one rule.

python3 tools/eoc/driver.py vc --build-dir build-eoc --semantics SEMANTICS INPUT RULE

Useful options:

• --sygus: generate a SyGuS query instead of SMT2
• --skip-cvc5: skip parse checks with cvc5
• --solve: run cvc5 on the generated VC or SyGuS file after optional parse checks
• --solve-args "ARGS": shell-style string of extra options passed to cvc5 during --solve
• --no-build: do not rebuild ethos-eoc first
• --cvc5 /path/to/cvc5: override the solver used for parse checks

Run many rules through the same pipeline.

python3 tools/eoc/driver.py batch --build-dir build-eoc --semantics SEMANTICS vc INPUT RULE1 RULE2 RULE3

Useful options:

• --all-rules: discover all (declare-rule ...) entries recursively
• --rules-file FILE: read one rule name per line from a file
• --clean: remove old files from out/vc or out/sygus first
• --keep-going: continue after failures and report all failed rules
• --skip-cvc5
• --solve
• --solve-args "ARGS"
• --no-build

Generate Lean output either for selected rules or for the full signature.

Selected rules:

python3 tools/eoc/driver.py lean --build-dir build-eoc --semantics SEMANTICS INPUT RULE1 RULE2

Whole signature:

python3 tools/eoc/driver.py lean --build-dir build-eoc --semantics SEMANTICS --all INPUT

Pass --no-parser to omit the signature-specific Parser.lean artifact while still generating the remaining Lean modules and per-rule files.

Pass --calc-name NAME to say what the generated Lean calls the calculus, which is the name of the package the run installs into, e.g. Cpc. Naming it here is what makes the imports of the published tree right where they are written; a run that names none calls the calculus after its input file, up to the first dot.

Pass --lean-config FILE to name the termination clauses of the input's own programs where the input was given already written out rather than as a configuration set; see "Why the generated Lean terminates" above.

The generated modules carry only the native_ definitions the input reaches, so the same signature compiled for fewer rules publishes a smaller native layer; see "The native layer" above.

Generated files are written to tools/eoc/out/lean/ by default, including per-rule files in tools/eoc/out/lean/Proofs/Rules/. The tree is written afresh each run, so it holds the whole of what that run compiled and nothing else. Parser.lean is the minimal calculus-specific instantiation of the generic Logos proof parser: it contains only the generated operator/rule tables, indexed-operator constructors, and surface desugaring configuration.

The operator tables also cover the identifiers the input introduces with define. Eunoia inlines a definition, so it has no counterpart in the compiled signature, but a proof may still use it. The desugar stage therefore re-emits each definition it can under the name $parse_<name>, which the later stages reparse and otherwise ignore. By convention a definition whose own name begins with $ is a helper of the signature and is not preserved, since a proof never mentions one. A preserved definition contributes to the parser only, never to a verification condition or to the generated proof checker. A definition that takes arguments becomes a macro of the parser, and one that takes none becomes a nullary operator, or an alias of the operator it names so that it inherits its indices and argument-list attribute.

Generate the desugared EO form of an input.

python3 tools/eoc/driver.py desugar --build-dir build-eoc INPUT

Output:

tools/eoc/out/desugar.eo

Run only the trim stage.

python3 tools/eoc/driver.py trim-defs --build-dir build-eoc INPUT TARGET1 TARGET2

Output:

tools/eoc/out/trim_defs/trim_gen.eo

Print discovered rules without running the pipeline.

python3 tools/eoc/driver.py list-rules INPUT

This walks include chains and preserves declaration order. It reads only the signatures, requires no build or semantics configuration, and writes no generated files. The scanner expects include and declare-rule forms to start on their own lines; it is not a complete Eunoia parser.

python3 tools/eoc/driver.py vc --build-dir build-eoc --semantics SEMANTICS INPUT RULE

python3 tools/eoc/driver.py batch --build-dir build-eoc --semantics SEMANTICS vc INPUT --all-rules --clean
python3 tools/eoc/driver.py batch --build-dir build-eoc --semantics SEMANTICS sygus INPUT --all-rules --clean

python3 tools/eoc/driver.py lean --build-dir build-eoc --semantics SEMANTICS --all INPUT
ls tools/eoc/out/lean

The tree under tools/eoc/out/lean is written with the layout of a Lean package, so a downstream tree that already has that layout takes it as it stands.

The driver writes the staged EO files into tools/eoc/out/. You can pass those directly to ethos-eoc if you want to debug a later stage manually.

Examples:

build-eoc/ethos-eoc tools/eoc/out/trim-d-booleans-rules.eo
build-eoc/ethos-eoc --plugin.smt-meta tools/eoc/out/vcmt-def-booleans-rules.eo
build-eoc/ethos-eoc --plugin.smt-meta-sygus tools/eoc/out/vcmt-def-booleans-rules.eo
build-eoc/ethos-eoc tools/eoc/out/lean-booleans-rules-final.eo
build-eoc/ethos-eoc --plugin.lean-meta tools/eoc/out/lean-booleans-rules-final.eo

By default, parse checks use:

1. --cvc5 /path/to/cvc5, if passed
2. $CVC5, if set
3. cvc5 on PATH

If none of those resolve, either pass --skip-cvc5 or set CVC5.

Check which directory you ran the driver from. Input paths are resolved relative to the current shell directory, not to --build-dir.

Either:

• pass --skip-cvc5
• pass --cvc5 /path/to/cvc5
• export CVC5=/path/to/cvc5

Look in tools/eoc/out/ for both the staged EO artifacts and the final published outputs. The plugin-private generated files remain under <build-dir>/out/plugins/.