[katjabercic]

Problem

Since the switch to the new code generator (Lean v4.22), builds on dev emit

shared RC State.addClause: cnf is shared (performance bug!)

e.g. 10× for the single #eval! in Trestle/Encode/Cardinality/Sinz.lean, and the corresponding #guard_msgs test had to be disabled.

Root cause

In EncCNF.withTemps, the source reads let vMap := s.vMap before running the inner encoder so that s dies early. The new LCNF simplifier treats the projection as a free-to-move value and substitutes it to its use site — after the inner run. The resulting IR does inc s, runs the whole inner encoder, and only then proj s.vMap; dec s. So the outer state, and hence its cnf, stays live across the entire inner run: the first addClause in every withTemps scope sees a shared cnf and copies the whole array. Since every tseitin[...] fragment opens its own scope, encodings degrade to one full CNF copy per fragment (quadratic overall).

Fix

Extract the tempified state and the surviving vMap in one step through a @[noinline] helper (LawfulState.withTempsAux) that is consumed before the inner run, and destructure its result with match. The compiler can then no longer move any read of s past the run. Checked the compiled IR: the pair is projected and freed before the inner call, and nothing references s afterwards.

Two notes:

• A getter returning the bare function (@[noinline] def vMapGet s := s.vMap) makes things worse: it compiles to a pap capturing the whole state, which then lives inside the restored vMap forever — the same bug the !!!!! comment in this file describes. The surviving value must be a saturated object, hence the pair.
• The first commit is an unrelated one-line compile fix (C.map _ vMap → C.map vMap) that dev currently needs to build at all; drop it if you already have your own version.

Verification

Full lake build on v4.28.0: succeeds with zero sharing warnings (previously Sinz ×10, Tseitin ×3). The #guard_msgs test in Sinz.lean is re-enabled and passes. Isolated #eval tests of plain EncCNF, seq, for_all, nested/sequential withTemps are all silent.

The underlying compiler behavior (projection substitution extending an object's lifetime past a call, defeating destructive updates) still reproduces on v4.32.2 and is probably worth an upstream lean4 issue; dumping the IR of a clone of withTemps with set_option trace.compiler.ir.result true demonstrates it directly.