Frontend and session preservation map

Checked against Primo’s command parser, frontend, session dispatcher, retained engines, and existing tests on 2026-10-01. Current explanations are in frontend and sessions. The historical measurements below are retained at their original revision; the documentation build does not requalify them.

Original material	Disposition and destination
Streaming checklist	Frontend representation and live-command parsing; source/specification links replace the implementation checklist as current exposition.
Rebuild ownership and operations	Session representation, journal replay, and scoped trace.
Append/rebuild-on-pop proposal	Retained design history. Current retained engines use selector retirement instead; the proposal is not described as shipped behavior.
Supported boundary	Session command table, admission restrictions, responses and tests. The old statement that persistent solving is unimplemented is superseded by opt-in assumptions mode.
Session validation procedures	Contributor experiment/validation extraction; native-prefix and stream tests must remain separate from whole-session timing.
Definition binding	Frontend definition expansion and worked capture example.
Native and rebuild qualifications; later gate	Retained dated evidence, including incomplete sessions and limitations of per-query model coverage.
Opt-in assumptions overview	Session retained-engine explanation.
Lexical repair and compatibility policy	Frontend token categories, canonical identity, attributes, binding policy, ownership and limitations. Old wrong answers are dated repaired incidents.
External lexical coverage	Retained coverage provenance; external solver tests are not Primo implementation or copied fixtures.
Lexical procedure and qualification	Contributor validation procedure and historical evidence. Character extensions remain distinct from normative conformance.
LRA engine design	Session selectors, preparation, callback lifetime, model visibility, safe preprocessing and costs. MathSAT deletion and preprocessing replay remain unimplemented.
LRA comparisons	Retained revision-specific correctness, native-session and OpenSMT comparisons.
UF engine design	Session retained identities, option restrictions, active roots, and model snapshots.
UF acceptance and evaluation	Retained dated comparison and correctness limits; not current performance evidence.
UF model replay and preparation	Session active lowered roots and new-atom suffix preparation; profiling and earlier checklists remain history.

Primary sections inspected

SMT-LIB 2.7 §§3.1–3.6, 4.1.4–4.1.5 and 4.2.2–4.2.3; MathSAT5 §§4.2–4.3; Bjørner–Fazekas §3.2 and §5. The session chapter records the implemented subset and the departures from these sources. No external solver implementation was used as an implementation source.