sc-spec — Math & Specification Extraction (Pipeline Stage 2.5)

Checklists smell math bugs ("this looks like a rounding issue"); this stage proves them. It captures what the math is supposed to be (from the docs) as an exact-arithmetic reference model, so stage 5 can fuzz the real contract and show a concrete input where the implementation diverges from intent. A divergence with a number behind it is the hardest finding to dismiss.

This is the answer to the structural blind spot of pure checklists: protocol- specific math that no catalog anticipates.

When to Use

• After sc-map and sc-graph; orchestrator calls this at stage 2.5.
• User says: "check the math", "verify the formulas", "does the code match the whitepaper".

Announce

Begin with: "I'm using the sc-spec skill to extract the protocol's intended math and build reference models..."

Workflow

1. Scan for the math worth specifying (deterministic)

python skills/sc-spec/scripts/scan_math.py <audit_dir>   # default .audit

Writes .audit/spec/math-candidates.json: documentation files, math-bearing functions (ranked), precision-risk hints (division-before-multiply, narrow downcasts), and NatSpec that already states a formula. This focuses the expensive extraction on the few functions where a formula bug actually matters.

2. Read the docs for intent

• Read the listed doc_files. For PDFs, use the pdf skill to extract text.
• Read the top math_functions at source level and their NatSpec.
• For each economically-meaningful quantity (share price, redeem/mint conversion, interest/accrual, fee, AMM output, collateral ratio, reward-per-share, auction price) capture the intended formula, its variables + decimals/units, and its intended rounding direction. Rounding direction matters more than magnitude — rounding toward the user is the bug even at 1 wei.

3. Build reference models (exact arithmetic)

For each formula write a Python reference under .audit/spec/reference/F-N_<name>.py from templates/reference_model.template.py. Rules:

• Encode INTENT (the doc), not the code. The reference is the oracle; if you copy the implementation you can't detect the implementation's bug.
• Exact integer arithmetic (// for floor); encode rounding explicitly. Never float.
• Compute in the spec's stated order (multiply-then-divide if that's the spec).
• Fill KNOWN_VECTORS from any worked numeric example in the docs.

Then verify every reference reproduces the docs' own numbers:

python skills/sc-spec/scripts/check_reference.py <audit_dir>/spec/reference/*.py

If a reference can't reproduce the doc's worked example, your transcription is wrong — fix it before stage 5 trusts it.

4. Map formula → chunk (use the call graph)

For each formula set implemented_by to the chunk ID(s) that compute it. Use call-graph.json reachability and the math-candidates ranking to find them (e.g. redeem → previewRedeem → the arithmetic). If the mapping is uncertain, say so in open_question rather than guessing — an unverified mapping is worse than a flagged unknown.

5. Extract doc-stated invariants

Pull invariants the docs assert ("the vault is always solvent", "shares never lose value", "debt ≤ collateral") into doc_invariants with provenance: doc. Then append them to project-map.json invariants, continuing the INV-N numbering. A finding that breaks an invariant the protocol itself promised is near-impossible to argue with.

6. Write math-spec.json

Conform to templates/math-spec.schema.json. One entry per formula with its reference model, tolerance, favors_user_if, divergence risk, confidence.

Graceful degradation (no usable docs)

If scan_math.py finds no docs (or they contain no formulas):

• Set degraded_mode: true, docs_available: false.
• Do not invent a spec. Instead derive the implemented math (source: code-derived) and shift verification from a differential oracle to property invariants: monotonicity (more shares ⇒ ≥ assets), no-free-money (deposit then immediate redeem ≤ deposit), conservation, round-trip bounds. Hand these to foundry-invariant-gen at stage 5 instead of a differential test.
• The tool still adds value — just property-based instead of spec-differential.

What stages 4–5 consume

• sc-hypothesize turns each formula with a divergence_risk (and every precision hint) into a math-divergence hypothesis targeting the relevant INV-N.
• sc-verify builds the differential PoC: fuzz implemented_by, compare to reference_model (Foundry vm.ffi to the Python reference when ffi is enabled, else precomputed vectors from the reference), and flag divergence beyond rounding_tolerance or in the favors_user_if direction.

Anti-False-Positive Principles

1. The reference is verified against the doc's own numbers before use (check_reference.py) — no oracle built on a misread formula.
2. Differential evidence is numeric — "on (7, 3000, 1000) the contract returns 0, spec says 21" is not arguable.
3. Uncertain mapping → open_question, not a claim. A formula mapped to the wrong function produces phantom divergences; flag instead of guess.
4. Spec may be stale, not the code. Frame divergences as "code does X, doc says Y — which is intended?" when confidence is below high.

Handoff

Tell the orchestrator: formulas extracted, references verified (pass/fail), doc- invariants promoted (new INV-N), degraded_mode true/false. Next stage: sc-hypothesize.