[SwayamInSync]

Every copy of a Layer-3 term copied the whole term, and a module is mostly copies. Each obligation's goal states every assumption before it, !A1 || (!A2 || ... || C), cloned from the passive program; each obligation's query clones its goal under a negation, the complete goal clones every goal, and the complete query clones the complete goal. So a module's memory grows with its obligations times what comes before them, four times over, and the simplifier rebuilds the complete goal while the old one is alive.

The ULEB128 case study (suite/llvm_uleb128.cpp, --jobs=8 in its RUN line) is where that stops CI. On main it peaks at 14.9 GB (ru_maxrss, 4 cores), and the Linux runners have 16 GB beside the three other lit workers. In a run of the Verify suite in lit's order on 4 workers, the whole run's anonymous memory peaked at 16.4 GB: this test at 14.6 GB while the certifier of lean_semantics.cpp held 1.7 GB. That is the The runner has received a shutdown signal (exit 143) of the Linux release jobs: main after #61 (run 39956700035), #62 twice, and #63's own release job (run 39993647759), 18 to 28 minutes into check-clang, whatever else each fixed. A heap profile of lowering it (valgrind massif, --lower-only, one job) puts 11.7 of its 12.1 GB peak in cloneVCExpr.

It grew in #57: --lower-only took 8.2 GB on #57's base and 12.7 GB after it, since the definedness checks of contract clauses gave encode_uleb128 60 more bounds obligations (64 instead of 4): one for the buffer[k] each of its 20 postconditions reads, and two (on entry and preserved) for each of its 20 loop invariants. Every one repeats the whole path before it.

Design

Terms share their subterms, which nothing changes once shared, as Verus's AIR shares Arc<ExprX>, Frama-C's Qed hash-conses its terms, and Lean shares Expr:

• The type. LogicExpr::Children and Patterns are LogicExprRef, llvm::IntrusiveRefCntPtr<const LogicExpr> (LLVM's intrusive count, 8-byte pointers, no control block). A term's root is still owned (std::unique_ptr<LogicExpr>) and may be changed; its subterms are const, so the compiler rejects any change to a node another term may share. Every root field and every reader stays as it was.
• Copies. cloneLogicExpr copies the root's fields and shares its children. A goal then states its assumptions, its query negates it, and the complete goal conjoins the goals without copying them; the static cloneVCExpr in the builder, a second deep copy, is gone.
• Rewriting. Code that stole or rewrote children in place takes a shallow copy instead (the builder's mode conversions, the Z3 adapter's case splits) or rewrites copy-on-write: the simplifier copies a node only when a child changes, and memoizes each subterm for the module, so a subterm that many goals share is simplified once and stays shared. A memoized subterm adds the rewrites its first simplification counted, so the statistics in Layer-3 dumps are those of the tree. The certifier's substitute, rename, inlineAt, approximate, fold, and the renaming in readsApart rewrite through rewriteSlots, which copies a node once, only when a child changes.
• Annotation. A node's Source is the one field written after a term is shared: a function of its Loc alone (mutable). Annotation visits each node once and writes only a value that differs, so it never writes a node that an earlier module shares and other threads may read.
• Caches by address. Each holds what depends on the node alone, so a node shared by two places cannot answer for the wrong one: the Z3 encoder's Done (a variable is encoded by its name, and the traversal keeps no scope), the certifier's Costly, and the Lean printer's let names, which now name a large subterm once where a statement shares it rather than once per copy.
• What stays quadratic. The goals still repeat their assumptions as trees: validation, hashing, and serialization traverse every occurrence, as before. Hash-consing the terms and memoizing those traversals would make lowering linear in the program; this is the representation step that comes first.

Measured

llvm_uleb128.cpp and safe_fib.cpp, 4 cores, one job unless stated:

	main	this branch
ULEB128, --lower-only: time, peak address space	53.5 s, 12.80 GB	10.4 s, 0.43 GB
ULEB128, verified with its --jobs=8: peak RSS, time	14.92 GB, 75 s	0.91 GB, 73 s
safe_fib.cpp, --lower-only: time, peak address space	16.2 s, 4.74 GB	7.1 s, 0.35 GB

The 31 verdicts of the case study are the same, line for line.

The exhaustive decoder (suite/llvm_uleb128_decoder_exhaustive.cpp, UNSUPPORTED in the suite for its memory) with its own --jobs=8 --timeout=30000: on main it takes about 87 GB and 1655 s, and its length-10 function times out; here all 78 functions verify in 279 s, peaking at 9.8 GB (16 cores), now the eight jobs' Z3 queries rather than Layer 3. --lower-only with one job, which on main passed 57 GB in one function before it was stopped, takes 1229 s within 1.5 GB of address space: memory no longer limits it, and the time is the traversals that stay quadratic (below).

The Verify suite on a release build: 443 passed, 1 unsupported (the exhaustive decoder, as on main), in 1036 s with 32 workers.

Tests

suite/shared_logic_terms.test (Linux): under ulimit -v 2000000 (2 GB of address space), --lower-only lowers every function of llvm_uleb128.cpp and safe_fib.cpp. On main both runs end with LLVM ERROR: out of memory. It also checks the Layer-3 rewrite count of a function whose goals share rewritten subterms (set_value of backend_counterexample_trace.cpp, 265, as on main), and exports the case study to Lean and checks with Inputs/lean_let_names.py that no statement binds one let name twice in the lets it starts with.

Mutants, each built and run on shared_logic_terms.test, obligation_ir.cpp, obligation_simplify.cpp, obligation_archive.test, certified_quantifier_ranges.cpp, nested_quantifier_counterexamples.cpp, choose.cpp, choose_axioms.cpp, inductive_counterexamples.cpp, inductive_predicates.cpp, spec_fuel_counterexamples.cpp, and read_instances.cpp (the two in the certifier also on the CertifyTest and MachineIntegerEncodingTest unit tests):

Mutant	Result
the clone copies every subterm	killed: shared_logic_terms (out of memory)
the Lean printer names a shared subterm once per place	killed: shared_logic_terms (lets)
a memoized subterm counts no rewrites	killed: shared_logic_terms (rewrites 265 of set_value in backend_counterexample_trace.cpp, 124 under the mutant; 1515 simplification lines of the suite's dumps change)
annotation never writes a source	killed: obligation_archive, nested_quantifier_counterexamples, read_instances
the simplifier copies every node it visits	survives: lowering the case study takes 10.5 s and 0.41 GB (10.2 s, 0.43 GB)
the simplifier without its memo	survives: 11.7 s and 0.43 GB
both	survives: 14.0 s and 0.54 GB, safe_fib.cpp 7.9 s and 0.41 GB
renaming also renames under a quantifier that rebinds the name	survives
substitution keeps substituting under the binder	survives

The three simplifier mutants change only time and memory, by the factors shown; no output depends on them, and the memo and copy-on-write stay for those factors and for keeping a rewritten shared subterm shared. The last two are in code this change rewrote from in-place to copy-on-write, but they are not new gaps: main's rename and substitute have the same two conditions, and no test makes the certifier rename a binder apart inside a quantifier that rebinds the name (an inlined definition whose quantifier's binder is a name the argument mentions).

A first version of the annotation mutant (&& false on the last comparison of the condition) disabled the write only when the end column alone differed, and survived; the mutant above makes it never write.

Equivalence with main

Over every Verify source (467 files), main's binary and this branch's were run the same three ways and their outputs compared by SHA-256:

• --lower-only --dump-ir=3,4 --obligation-out=...: Layer 3 (with every semantic hash) and Layer 4 dumps and the archive are byte-identical for 466 files. The other, crash_report_url.cpp, crashes on purpose and prints the binary's name.
• --backend=bmc --unroll=2 --lower-only --dump-ir=3: identical for the same 466.
• --backend=lean --lean-out=...: identical for 458. In the other 8 (the ULEB128 case study and its portfolio input, mvp_factorial, safe_fib, pointer_subobjects, and the three UTF-8 files) a statement names a large subterm it shares once instead of once per copy: in encode_uleb128's obligation 213, 15 lets instead of 16, one of which bound the same 1630-character term twice. Lean checked that each of the 1053 theorems of those 8 exports has the same type on main and here, up to definitional equality (both exports in one file, each in its own namespace, isDefEq with every constant of one mapped to the other's).

Docs

• ARCHITECTURE.md (Layer 3): shared subterms, copy-on-write rewriting, annotation, the caches by address, what stays quadratic, and the memory before and after.
• Release notes: "Large functions take less memory".

Checked

• Full Verify suite, above; VerifyTests: 62 pass, 1 skipped (as on main); docs_coverage.test and docs_examples.test pass.
• The equivalence and definitional-equality checks above.
• shared_logic_terms.test on main's binary: both lowering runs end with LLVM ERROR: out of memory.