From 69e9adcb37014aa02aec9f0867ec10f6ac5cfc75 Mon Sep 17 00:00:00 2001 From: sururu-k <2009hirotake@gmail.com> Date: Wed, 22 Jul 2026 20:57:16 +0900 Subject: [PATCH 1/3] feat: stage-2 quality judge + improve loop (speca#88) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The eval step of the #88 confirmed direction: eval is LLM-as-judge quality scoring (five axes, blind rubric), NOT recall — the verdict compares score distributions against the vendored solodit reference bar (data/solodit_checklist.csv, provenance pinned incl. git blob sha); the vuln dataset is improve-step teaching material only. Convergence needs BOTH the reference bar met AND a 3-round plateau; unconverged runs end honestly with converged=false. LLM access is injected (prompt->response subprocess seam): no API key in the repo, default CI runs the deterministic mock end to end, the real LLM run is dispatch-only on self-hosted (judge-dispatch.yml). recall.py untouched; generation (CHK-15) reused, not re-implemented. --- .github/workflows/ci.yml | 40 ++ .github/workflows/judge-dispatch.yml | 107 +++++ README.md | 33 ++ data/solodit_checklist.csv | 53 +++ data/solodit_checklist.meta.json | 13 + docs/judge-loop.md | 114 ++++++ src/speca_lean4/cli.py | 204 ++++++++++ src/speca_lean4/judge.py | 582 +++++++++++++++++++++++++++ tests/fixtures/mock_llm.py | 47 +++ tests/test_judge.py | 536 ++++++++++++++++++++++++ 10 files changed, 1729 insertions(+) create mode 100644 .github/workflows/judge-dispatch.yml create mode 100644 data/solodit_checklist.csv create mode 100644 data/solodit_checklist.meta.json create mode 100644 docs/judge-loop.md create mode 100644 src/speca_lean4/judge.py create mode 100644 tests/fixtures/mock_llm.py create mode 100644 tests/test_judge.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4f92b11..32e100f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -86,6 +86,46 @@ jobs: --health-json tests/fixtures/theorem_health.sample.json \ --out 01e_fixture.json speca-lean4 verify-recall --ours 01e_fixture.json --strict + - name: honesty check — vendored solodit reference provenance (speca#88 stage-2) + run: | + python3 -c " + import hashlib, json, csv + meta = json.load(open('data/solodit_checklist.meta.json', encoding='utf-8')) + raw = open('data/solodit_checklist.csv', 'rb').read() + sha = hashlib.sha1(b'blob %d\x00' % len(raw) + raw).hexdigest() + assert sha == meta['source_blob_sha'], f'vendored bytes drifted: {sha}' + assert b'\r' not in raw, 'CRLF crept into the vendored reference' + rows = list(csv.DictReader(open('data/solodit_checklist.csv', encoding='utf-8-sig'))) + assert len(rows) == meta['n_rows'], (len(rows), meta['n_rows']) + assert list(rows[0].keys()) == meta['columns'], rows[0].keys() + print(f'OK: {len(rows)} reference items, blob {sha} matches {meta[\"source_repo\"]}@{meta[\"source_commit\"][:12]}') + " + - name: judge + improve harness wiring with the MOCK LLM (no API key in default CI) + # The real LLM run is dispatch-only (judge-dispatch.yml, self-hosted + # authenticated Claude CLI). Here the injected-LLM seam is exercised + # end to end with the deterministic mock so this stays green keyless. + run: | + speca-lean4 judge \ + --ours 01e_fixture.json --id-prefix CHK- \ + --llm-cmd "python3 tests/fixtures/mock_llm.py" \ + --out judge_report_mock.json + speca-lean4 improve \ + --ours 01e_fixture.json --id-prefix CHK- \ + --llm-cmd "python3 tests/fixtures/mock_llm.py" \ + --ref-report judge_report_mock.json \ + --out-dir improve_run_mock --max-rounds 4 + python3 -c " + import json + rep = json.load(open('judge_report_mock.json', encoding='utf-8')) + assert rep['ours']['n'] == 15 and rep['reference']['n'] == 52 + log = json.load(open('improve_run_mock/score_log.json', encoding='utf-8')) + assert log['rounds'] and len(log['history_overall_mean']) == len(log['rounds']) + assert isinstance(log['converged'], bool) and log['stop_reason'] + props = json.load(open('improve_run_mock/improved_01e.json', encoding='utf-8'))['properties'] + assert len(props) == 15 + print('OK: judge report + improve score log written with the mock adapter;', + f\"converged={log['converged']} ({log['stop_reason']})\") + " lean: name: lean exporter build diff --git a/.github/workflows/judge-dispatch.yml b/.github/workflows/judge-dispatch.yml new file mode 100644 index 0000000..f449840 --- /dev/null +++ b/.github/workflows/judge-dispatch.yml @@ -0,0 +1,107 @@ +name: "judge + improve with the real LLM (speca#88 stage-2, dispatch-only)" + +# The default CI exercises the judge/improve harness with a deterministic +# mock (no API key anywhere in this repo). This workflow is the ONE place the +# real LLM runs: dispatch-only, on a self-hosted runner where the Claude CLI +# is already authenticated (same pattern as speca's 03/04 workflows). It +# emits the CHK checklist from the fixture health, judges it against the +# vendored solodit reference bar, runs the improve loop, and uploads the +# judge report + per-round score log as artifacts. +# +# No pull_request trigger on purpose: it occupies a shared runner and spends +# LLM budget. Honesty: the verification step only checks the artifacts are +# well-formed — it never asserts the bar was met or the loop converged; +# below-bar / unconverged are valid, reportable outcomes. + +on: + workflow_dispatch: + inputs: + model: + description: "claude -p --model value (empty = CLI default)" + required: false + type: string + default: "" + max_rounds: + description: "improve loop hard cap" + required: false + type: number + default: 6 + skip_improve: + description: "only judge (no improve loop) to bound LLM cost" + required: false + type: boolean + default: false + +permissions: + contents: read + +jobs: + judge-improve: + if: ${{ github.actor == 'grandchildrice' || github.actor == 'hirorogo' || github.actor == 'sururu-k' }} + runs-on: self-hosted + timeout-minutes: 120 + + env: + MODEL_INPUT: ${{ inputs.model }} + MAX_ROUNDS: ${{ inputs.max_rounds }} + SKIP_IMPROVE: ${{ inputs.skip_improve }} + + steps: + - uses: actions/checkout@v4 + + - name: install the plugin + run: pip install -e '.[dev]' + + - name: emit the CHK checklist 01e (fixture health; generation is CHK-15, not re-implemented) + run: | + speca-lean4 emit-01e \ + --scope tests/fixtures/bug_bounty_scope.sample.json \ + --health-json tests/fixtures/theorem_health.sample.json \ + --out 01e_fixture.json + + - name: judge against the solodit reference bar (real LLM) + run: | + set -euo pipefail + LLM_CMD="claude -p" + if [ -n "$MODEL_INPUT" ]; then LLM_CMD="claude -p --model $MODEL_INPUT"; fi + speca-lean4 judge \ + --ours 01e_fixture.json --id-prefix CHK- \ + --llm-cmd "$LLM_CMD" \ + --out judge_report.json + + - name: improve loop (real LLM, reference scores reused from the judge report) + if: ${{ inputs.skip_improve != true }} + run: | + set -euo pipefail + LLM_CMD="claude -p" + if [ -n "$MODEL_INPUT" ]; then LLM_CMD="claude -p --model $MODEL_INPUT"; fi + speca-lean4 improve \ + --ours 01e_fixture.json --id-prefix CHK- \ + --llm-cmd "$LLM_CMD" \ + --ref-report judge_report.json \ + --out-dir improve_run --max-rounds "$MAX_ROUNDS" + + - name: verify artifacts are well-formed (NOT that the bar was met) + run: | + python3 -c " + import json, os + rep = json.load(open('judge_report.json', encoding='utf-8')) + assert rep['ours']['n'] > 0 and rep['reference']['n'] == 52 + print('judge:', 'ours', rep['ours'], 'reference', rep['reference'], + 'meets_reference_bar =', rep['meets_reference_bar']) + if os.path.isdir('improve_run'): + log = json.load(open('improve_run/score_log.json', encoding='utf-8')) + assert log['rounds'] and log['stop_reason'] + print('improve:', 'converged =', log['converged'], + f\"({log['stop_reason']})\", 'progression =', log['history_overall_mean']) + " + + - name: upload judge report + score log + if: always() + uses: actions/upload-artifact@v4 + with: + name: judge-improve-real-llm + path: | + judge_report.json + improve_run/ + retention-days: 30 diff --git a/README.md b/README.md index 797d6f2..145ad8b 100644 --- a/README.md +++ b/README.md @@ -312,6 +312,39 @@ severity profile than the CRITICAL/HIGH-heavy benchmark, which we report rather than fake. Most consensus-layer findings (OOM/DoS, LMD-GHOST, BLS internals, eth1 ops) remain out of the FFG formal remit by construction. +## Quality judge + improve loop (speca#88 stage-2) + +eval here is NOT recall (the #88 direction's 重要な訂正): the checklist is not +scored on reproducing dataset bugs, but on reaching the QUALITY LEVEL of a +professional audit checklist. `speca-lean4 judge` scores every item on five +fixed axes (specificity, implementation_readiness, generality, actionability, +granularity; blind rubric in `src/speca_lean4/judge.py`) and compares the +score DISTRIBUTION against the same-rubric scores of the vendored solodit +reference ([`data/solodit_checklist.csv`](data/solodit_checklist.csv), 52 +professional audit items, provenance pinned in +[`data/solodit_checklist.meta.json`](data/solodit_checklist.meta.json)). +`speca-lean4 improve` then loops judge -> sharpen low scorers (with the +matching `data/ethereum_vulns.csv` rows as teaching material — improve input, +never an eval denominator) -> re-judge, converging only when the reference +bar is met AND the last 3 rounds plateau; an unconverged run ends honestly +with `converged: false`. `recall.py`'s 0.556 stays a side reference number, +outside the judge verdict. Full spec: [`docs/judge-loop.md`](docs/judge-loop.md). + +```bash +# LLM access is injected — no API key in this repo. --llm-cmd reads the +# prompt on stdin and writes the response on stdout, e.g. an authenticated +# Claude CLI (the real run lives in .github/workflows/judge-dispatch.yml, +# self-hosted, dispatch-only; default CI wires tests/fixtures/mock_llm.py): +speca-lean4 judge --ours outputs/01e_PARTIAL_checklist-high-angle.json \ + --llm-cmd "claude -p" --out judge_report.json + +speca-lean4 improve --ours outputs/01e_PARTIAL_checklist-high-angle.json \ + --llm-cmd "claude -p" --ref-report judge_report.json \ + --out-dir improve_run --max-rounds 6 +# -> improve_run/score_log.json (per-round progression, convergence verdict) +# improve_run/improved_01e.json (proposal; theorem_map.json stays canonical) +``` + ## Lean exporter directly ```bash diff --git a/data/solodit_checklist.csv b/data/solodit_checklist.csv new file mode 100644 index 0000000..17810ee --- /dev/null +++ b/data/solodit_checklist.csv @@ -0,0 +1,53 @@ +id,category,subcategory,question,description +SOL-AM-DOSA-1,DoS,withdrawal,"Is withdrawal pattern followed?","Prevent DOS during withdrawals by following pull-based approach" +SOL-AM-DOSA-2,DoS,minimum_amount,"Is there a minimum transaction amount?","Enforce minimum amounts to prevent dust/zero transaction spam" +SOL-AM-DOSA-3,DoS,blacklist,"How does protocol handle blacklisting tokens?","Account for USDC-like blacklisting to ensure functionality" +SOL-AM-DOSA-4,DoS,queue,"Can forcing queue processing lead to DOS?","Design queue processing resistant to spam exploitation" +SOL-AM-DOSA-5,DoS,low_decimals,"What happens with low decimal tokens?","Handle low decimal tokens to prevent rounding-to-zero DOS" +SOL-AM-DOSA-6,DoS,external_call,"Does protocol handle external interactions safely?","Robust handling of external failures to maintain integrity" +SOL-AM-DA-1,Donation,balance_reliance,"Does protocol rely on balanceOf instead of internal accounting?","Attackers can manipulate accounting by donating tokens" +SOL-AM-FrA-1,Frontrunning,create_pattern,"Are get-or-create patterns protected?","Separate creation and interaction to prevent frontrunning" +SOL-AM-FrA-2,Frontrunning,two_tx,"Are two-transaction actions safe from frontrunning?","Critical multi-tx actions must not be interferable" +SOL-AM-FrA-3,Frontrunning,dust_grief,"Can users cause others' tx to revert with dust?","Prevent dust amounts from affecting contract state" +SOL-AM-FrA-4,Frontrunning,commit_reveal,"Is commit-reveal scheme user-bound?","Two-phase commit-reveal must bind to specific users" +SOL-AM-GA-1,Griefing,state_dependency,"Is there an external function relying on changeable states?","Ensure withdrawals not disturbed by other actors" +SOL-AM-GA-2,Griefing,gas_limit,"Can operations be manipulated with precise gas?","Implement gas checks before critical operations" +SOL-AM-MA-1,Manipulation,timestamp,"Is block.timestamp used for time-sensitive ops?","Miners can manipulate timestamps; use block.number for critical timing" +SOL-AM-MA-2,Manipulation,randomness,"Is block properties used for randomness?","Use Chainlink VRF instead of predictable block properties" +SOL-AM-MA-3,Manipulation,tx_ordering,"Is logic sensitive to transaction ordering?","Implement slippage protection that reverts on bad execution" +SOL-AM-PMA-1,PriceManipulation,balance_ratio,"Is price calculated by token balance ratio?","Use oracles instead of balance ratios vulnerable to flash loans" +SOL-AM-PMA-2,PriceManipulation,spot_price,"Is price from DEX spot prices?","Use TWAP or reliable oracles instead of spot prices" +SOL-AM-ReentrancyAttack-1,Reentrancy,read_only,"Is there a view function returning stale value during interaction?","Extend reentrancy guards to view functions" +SOL-AM-ReentrancyAttack-2,Reentrancy,state_after_call,"Is there state change after external call?","Use CEI pattern or reentrancy guards" +SOL-AM-ReplayAttack-1,Replay,failed_tx,"Are failed transactions protected against replay?","Nonce-based mechanisms ensuring single execution" +SOL-AM-ReplayAttack-2,Replay,cross_chain,"Is there cross-chain replay protection?","Use chain-specific domain separators" +SOL-AM-RP-1,RugPull,admin_drain,"Can admin pull assets from protocol?","Limit admin access; enforce timelocks" +SOL-AM-SandwichAttack-1,Sandwich,slippage,"Does protocol have explicit slippage protection?","Allow users to specify minimum output amount" +SOL-AM-SybilAttack-1,Sybil,user_count,"Is mechanism depending on user count?","Do not rely on user count; vulnerable to sybil" +SOL-Basics-AC-1,AccessControl,actors,"Did you clarify all actors and interactions?","Clear understanding of actors is critical for security" +SOL-Basics-AC-2,AccessControl,missing,"Are there functions lacking access controls?","Missing access controls expose to unauthorized changes" +SOL-Basics-AC-3,AccessControl,whitelist,"Do addresses require whitelisting?","Whitelisting adds security against malicious actors" +SOL-Basics-AC-4,AccessControl,transfer,"Does protocol allow privilege transfer?","Two-step transfer adds security against unintentional changes" +SOL-Basics-AC-7,AccessControl,tx_origin,"Does contract use tx.origin?","tx.origin enables forwarded calls; use msg.sender" +SOL-Basics-AL-9,Loop,huge_array,"Is there iteration of huge array?","Block gas limit bounds operations; ensure bounded iteration" +SOL-Basics-AL-10,Loop,dos_in_loop,"Is there DOS potential in loop?","Single failure should not revert whole operation" +SOL-Basics-AL-11,Loop,msgvalue_in_loop,"Is msg.value used in loop?","msg.value consistent per tx; loop use indicates accounting error" +SOL-Basics-Math-1,Math,accuracy,"Is mathematical calculation accurate?","Verify against established rules and comments" +SOL-Basics-Math-2,Math,precision_time,"Is there precision loss in time calculations?","Precision loss leads to significant errors over time" +SOL-Basics-Math-4,Math,div_before_mul,"Is dividing done before multiplication?","Multiply before dividing to maintain precision" +SOL-Basics-Math-5,Math,rounding,"Does rounding direction matter?","Rounding direction matters for user share accounting" +SOL-Basics-Math-6,Math,div_zero,"Is there division by zero possibility?","Check denominators before division" +SOL-Basics-Math-7,Math,overflow,"Can variables overflow in Solidity >=0.8?","Variables can exceed bounds causing reverts" +SOL-Basics-Math-10,Math,inequality,"Should < or > be <= or >=?","Incorrect inequality causes unexpected edge behavior" +SOL-Basics-Math-12,Math,edge_values,"What happens for min/max values?","Confirm all edge cases where terms have min/max" +SOL-Basics-Payment-1,Payment,receiver_revert,"Can receiver revert?","Receiver contracts can deny; handle with call()" +SOL-Basics-Payment-3,Payment,force_feed,"Are there force-feeding vulnerabilities?","Selfdestruct and other mechanisms can force-feed" +SOL-Basics-Payment-4,Payment,dust,"What is minimum deposit/withdrawal?","Dust deposits lead to rounding and DOS" +SOL-Basics-Payment-5,Payment,withdrawal_pattern,"How is withdrawal handled?","Pull-based approach letting users withdraw" +SOL-Basics-Function-1,Function,input_validation,"Are inputs validated?","Validate inputs to prevent unexpected behavior" +SOL-Basics-Function-2,Function,output_validation,"Are outputs validated?","Validate outputs to prevent unexpected behavior" +SOL-Basics-Function-3,Function,frontrunnable,"Can function be front-run?","Ensure no unexpected risk if frontrun" +SOL-Basics-Function-5,Function,edge_inputs,"Can edge inputs (0 max) cause unexpected behavior?","Edge values need separate testing" +SOL-Basics-Function-6,Function,arbitrary_input,"Does function allow arbitrary user input?","Restrict low-level calls with arbitrary input" +SOL-Basics-Initialization-1,Init,state_vars,"Are important state variables initialized?","Overlooking initialization leads to critical issues" +SOL-Basics-Type-1,Type,forced_cast,"Is there forced type casting?","Forced casting doesn't revert on overflow" diff --git a/data/solodit_checklist.meta.json b/data/solodit_checklist.meta.json new file mode 100644 index 0000000..9674d9d --- /dev/null +++ b/data/solodit_checklist.meta.json @@ -0,0 +1,13 @@ +{ + "source_repo": "NyxFoundation/speca", + "source_path": "benchmarks/knowledge/solodit_checklist.csv", + "source_ref": "main", + "source_commit": "8b7da09eaf87737c1cb3b281b520a4bf71a73b55", + "source_blob_sha": "17810eef5e78f0ad939906590b712013e3ee8dc4", + "introduced_in_source_commit": "9e50ee041352ef69536d8b283c775169d5647e72", + "fetched": "2026-07-22", + "columns": ["id", "category", "subcategory", "question", "description"], + "n_rows": 52, + "role": "Reference bar for the speca#88 stage-2 quality judge (src/speca_lean4/judge.py): the judge scores these professional audit-checklist items and the generated 01e items with the same blind five-axis rubric, and the generated score distribution must be at least as good as this corpus's distribution. Calibration is on QUALITY LEVEL only — the corpus is DeFi-domain, the generated checklist is consensus-domain, and no content matching against these rows enters the verdict.", + "note": "The #88 direction comment describes the file as 53 items; the file at the pinned blob has 52 data rows (speca commit 9e50ee04's own message also says 52). Vendored byte-identical (LF, UTF-8, git blob sha above); tests/test_judge.py recomputes the blob sha from the vendored bytes." +} diff --git a/docs/judge-loop.md b/docs/judge-loop.md new file mode 100644 index 0000000..0710504 --- /dev/null +++ b/docs/judge-loop.md @@ -0,0 +1,114 @@ +# Stage-2 quality judge + improve loop (speca#88) + +Implements the eval step of the #88 confirmed direction +(https://github.com/NyxFoundation/speca/issues/88#issuecomment-5027471370): +the goal is one 01e checklist at the quality level of a professional audit +checklist — implementation-ready and general. Generation (CHK-15, plugin +PR #21) is reused as-is; this harness evaluates and improves its output. + +## eval is not recall + +The direction comment's 重要な訂正, load-bearing for this design: eval does +NOT ask whether the checklist reproduces the vuln dataset's specific bugs. +It asks whether the checklist reaches the same QUALITY LEVEL as the +reference corpus. Structurally: + +- the judge verdict is a comparison of five-axis score distributions, + computed by the same blind rubric over both corpora. No content matching + against the reference or the dataset enters the verdict anywhere + (`tests/test_judge.py` pins this: judge prompts contain no ids, no corpus + identity, no provenance fields, no dataset rows). +- `data/ethereum_vulns.csv` is the improve step's teaching material only. +- `recall.py`'s label recall (0.556) remains a side reference number and is + deliberately absent from the judge verdict. + +## The five axes + +Fixed rubric in `judge.RUBRIC`, each axis an integer 1-5 with written 1/3/5 +anchors (the axis definitions are the #88 comment's, verbatim in intent): + +1. `specificity` — a code-level check, not a spec restatement +2. `implementation_readiness` — targets surfaces where implementations + actually break (arithmetic width, bounds, resources, termination) +3. `generality` — not glued to one client's historical bug +4. `actionability` — an auditor can apply it to code as written +5. `granularity` — one auditable concern, no redundant bundling + +A judge response must be strict JSON with every axis present and in range; +anything else errors after one retry — never silently clamped or defaulted. + +## Reference bar (calibration) + +`data/solodit_checklist.csv` — 52 professional audit checklist items, +vendored byte-identical from speca `benchmarks/knowledge/solodit_checklist.csv` +(provenance, including the git blob sha, pinned in +`data/solodit_checklist.meta.json`; CI and `tests/test_judge.py` recompute +the blob sha from the vendored bytes). The corpus is DeFi-domain on purpose: +it calibrates quality level, not content. + +`meets_reference_bar(ours, reference, axis_tolerance=0.25)`: + +- our `overall_mean` >= the reference `overall_mean`, AND +- no axis mean falls more than `axis_tolerance` below its reference axis + mean (one pumped axis cannot buy the verdict). + +## The loop + +`improve_loop(props, reference, vulns, judge_fn, improve_fn, ...)`: + +1. judge every item (round 0 logged) +2. improve candidates: `overall` below the reference overall mean, or any + axis <= `low_axis` (default 3). Each candidate's improve prompt carries + (a) the item, (b) the judge critique + scores, (c) up to 3 vuln-dataset + rows selected by the item's `label` (severity-ranked fallback when the + label is outside the vendored slice) +3. deterministic guards on each rewrite: only `text`/`assertion` may change + (identity, `lean_status`, label, severity etc. are immutable by + construction); the merged property must pass `schema.validate_property`; + a client/implementation name in the rewrite is rejected (generality + lint). Rejected rewrites keep the original and are logged +4. re-judge only the changed items; append the round to the score log +5. convergence needs BOTH: the reference bar is met AND the last + `plateau_rounds` (default 3) rounds are flat within `plateau_delta` + (default 0.05). Bar-met-but-climbing keeps going; plateaued-below-bar + keeps going until `max_rounds`, then stops with `converged: false` and + `stop_reason: max_rounds_reached_without_convergence` — an unconverged or + below-bar run is reported as such, never dressed up. + +Outputs (`improve --out-dir`): `score_log.json` (per-round distributions, +bar verdicts, improvement dispositions, `history_overall_mean`) and +`improved_01e.json` (a PROPOSAL — `theorem_map.json` stays the canonical +checklist source; landing rewrites there is a reviewed, manual step). + +## LLM access is injected + +`judge.py` is pure logic over two injected callables +(`judge_fn`/`improve_fn`: prompt str -> response str). The repo holds no API +key and imports no LLM SDK. Bindings: + +- unit tests: deterministic in-process functions (all convergence and guard + behavior is tested without any LLM) +- default CI: `tests/fixtures/mock_llm.py` through the real `--llm-cmd` + subprocess seam — the wiring is exercised end to end, keyless +- real runs: `.github/workflows/judge-dispatch.yml`, dispatch-only on a + self-hosted runner with an authenticated Claude CLI (`--llm-cmd + "claude -p"`), the same pattern as speca's 03/04 workflows. Its + verification step checks artifact well-formedness only — it never asserts + the bar was met. + +## CLI + +```bash +speca-lean4 judge --ours <01e.json> [--id-prefix CHK-] --llm-cmd "claude -p" \ + [--reference data/solodit_checklist.csv | --ref-report judge_report.json] \ + [--axis-tolerance 0.25] [--out judge_report.json] [--strict] + +speca-lean4 improve --ours <01e.json> [--id-prefix CHK-] --llm-cmd "claude -p" \ + [--improve-cmd ...] [--vulns-csv data/ethereum_vulns.csv] \ + --out-dir improve_run [--max-rounds 6] [--low-axis 3] \ + [--plateau-rounds 3] [--plateau-delta 0.05] [--strict] +``` + +`--ref-report` reuses the reference scores from a previous judge report +(saves ~52 LLM calls per run); `--strict` makes below-bar (judge) or +non-convergence (improve) a non-zero exit. diff --git a/src/speca_lean4/cli.py b/src/speca_lean4/cli.py index ca6e6fe..807e06b 100644 --- a/src/speca_lean4/cli.py +++ b/src/speca_lean4/cli.py @@ -303,6 +303,141 @@ def cmd_verify_recall(args: argparse.Namespace) -> int: return 0 +def _make_llm(cmd: str | None, what: str): + from .judge import split_cmd, subprocess_llm + + if not cmd: + print( + f"error: {what} needs an LLM. Pass --llm-cmd (a command reading the " + "prompt on stdin, writing the response on stdout — e.g. 'claude -p' " + "on a runner where the Claude CLI is authenticated). This repo " + "never reads an API key itself.", + file=sys.stderr, + ) + return None + return subprocess_llm(split_cmd(cmd)) + + +def _reference_distribution(args: argparse.Namespace, judge_fn) -> tuple[dict, list, str]: + """Reference bar: reuse a previous report's reference scores when + --ref-report is given (saves ~52 LLM calls), else judge the vendored + solodit corpus now with the same blind rubric.""" + from .judge import checklist_items_from_solodit, judge_items, score_distribution + + if args.ref_report: + prev = _load_json(args.ref_report) + return prev["reference"], prev["reference_items"], prev["reference_source"] + items = checklist_items_from_solodit(args.reference) + scored = judge_items(items, judge_fn) + return score_distribution(scored), scored, str(args.reference) + + +def cmd_judge(args: argparse.Namespace) -> int: + """Quality judge (speca#88 stage-2 eval). NOT recall: the verdict compares + blind five-axis score DISTRIBUTIONS against the solodit reference bar; + content matching enters nowhere.""" + from .judge import ( + checklist_items_from_01e, format_judge_summary, judge_items, + meets_reference_bar, score_distribution, + ) + + judge_fn = _make_llm(args.llm_cmd, "judge") + if judge_fn is None: + return 2 + ours_items = checklist_items_from_01e(_load_json(args.ours), args.id_prefix) + if not ours_items: + print(f"error: no properties to judge in {args.ours} " + f"(id prefix: {args.id_prefix or 'none'})", file=sys.stderr) + return 2 + ref_dist, ref_items, ref_source = _reference_distribution(args, judge_fn) + scored = judge_items(ours_items, judge_fn) + ours_dist = score_distribution(scored) + meets, gaps = meets_reference_bar(ours_dist, ref_dist, args.axis_tolerance) + report = { + "reference_source": ref_source, + "reference": ref_dist, + "reference_items": ref_items, + "ours_source": str(args.ours), + "ours": ours_dist, + "items": scored, + "axis_tolerance": args.axis_tolerance, + "meets_reference_bar": meets, + "bar_gaps": gaps, + } + if args.out: + Path(args.out).write_text( + json.dumps(report, indent=2, ensure_ascii=False), encoding="utf-8" + ) + print(format_judge_summary(report)) + if args.strict and not meets: + print("judge --strict: below the reference bar", file=sys.stderr) + return 1 + return 0 + + +def cmd_improve(args: argparse.Namespace) -> int: + """Improve loop (speca#88 stage-2): judge -> sharpen low scorers with the + vuln dataset as teaching material -> re-judge, until the reference bar is + met AND the last rounds plateau (both required).""" + from .judge import ( + checklist_items_from_01e, format_improve_summary, improve_loop, + load_vulns, + ) + + judge_fn = _make_llm(args.llm_cmd, "improve") + if judge_fn is None: + return 2 + improve_fn = _make_llm(args.improve_cmd, "improve") if args.improve_cmd else judge_fn + + doc = _load_json(args.ours) + all_props = list(doc.get("properties", [])) + props = [ + p for p in all_props + if not args.id_prefix or str(p.get("property_id", "")).startswith(args.id_prefix) + ] + if not props: + print(f"error: no properties to improve in {args.ours} " + f"(id prefix: {args.id_prefix or 'none'})", file=sys.stderr) + return 2 + # sanity: the loop judges the same surface checklist_items_from_01e exposes + assert [p["property_id"] for p in props] == [ + i["id"] for i in checklist_items_from_01e(doc, args.id_prefix) + ] + ref_dist, _ref_items, ref_source = _reference_distribution(args, judge_fn) + + result = improve_loop( + props, ref_dist, load_vulns(args.vulns_csv), judge_fn, improve_fn, + max_rounds=args.max_rounds, low_axis=args.low_axis, + plateau_rounds=args.plateau_rounds, plateau_delta=args.plateau_delta, + axis_tolerance=args.axis_tolerance, + ) + + out_dir = Path(args.out_dir) + out_dir.mkdir(parents=True, exist_ok=True) + log = {k: v for k, v in result.items() if k != "properties"} + log["reference_source"] = ref_source + log["ours_source"] = str(args.ours) + (out_dir / "score_log.json").write_text( + json.dumps(log, indent=2, ensure_ascii=False), encoding="utf-8" + ) + improved_doc = {k: v for k, v in doc.items() if k != "properties"} + improved_doc["x_improve_note"] = ( + "proposal output of `speca-lean4 improve` (speca#88 stage-2 loop); the " + "canonical checklist source stays theorem_map.json — landing these " + "rewrites there is a reviewed, manual step" + ) + improved_doc["properties"] = result["properties"] + (out_dir / "improved_01e.json").write_text( + json.dumps(improved_doc, indent=2, ensure_ascii=False), encoding="utf-8" + ) + print(format_improve_summary(result)) + print(f"wrote {out_dir / 'score_log.json'} and {out_dir / 'improved_01e.json'}") + if args.strict and not result["converged"]: + print("improve --strict: loop did not converge", file=sys.stderr) + return 1 + return 0 + + def build_parser() -> argparse.ArgumentParser: p = argparse.ArgumentParser(prog="speca-lean4", description=__doc__) sub = p.add_subparsers(dest="command", required=True) @@ -385,9 +520,78 @@ def build_parser() -> argparse.ArgumentParser: "or rules claiming coverage via non-emitted properties", ) r.set_defaults(func=cmd_verify_recall) + + j = sub.add_parser( + "judge", + help="LLM-as-judge quality eval of a 01e checklist (speca#88 stage-2): " + "five-axis blind scoring calibrated against the vendored solodit " + "reference bar. NOT recall — no content matching in the verdict.", + ) + j.add_argument("--ours", required=True, help="the 01e JSON to judge (e.g. 01e_PARTIAL_checklist-high-angle.json)") + j.add_argument("--id-prefix", help="only judge properties whose property_id starts with this (e.g. CHK-)") + _add_judge_common_args(j) + j.add_argument("--out", help="write the full JSON judge report here") + j.add_argument( + "--strict", action="store_true", + help="exit non-zero when the score distribution is below the reference bar", + ) + j.set_defaults(func=cmd_judge) + + i = sub.add_parser( + "improve", + help="judge -> sharpen low scorers (vuln dataset rows as teaching " + "material) -> re-judge, until reference-bar met AND plateaued " + "(both required); logs per-round score progression", + ) + i.add_argument("--ours", required=True, help="the 01e JSON whose properties get improved") + i.add_argument("--id-prefix", help="only loop over properties whose property_id starts with this (e.g. CHK-)") + _add_judge_common_args(i) + i.add_argument( + "--improve-cmd", + help="separate LLM command for the improve step (default: same as --llm-cmd)", + ) + i.add_argument( + "--vulns-csv", default=str(_REPO_ROOT / "data" / "ethereum_vulns.csv"), + help="vuln dataset slice used as improve teaching material, never as an " + "eval denominator (default: data/ethereum_vulns.csv)", + ) + i.add_argument("--out-dir", required=True, help="write score_log.json + improved_01e.json here") + i.add_argument("--max-rounds", type=int, default=6, help="hard cap on improve rounds (default 6)") + i.add_argument("--low-axis", type=int, default=3, help="an item with any axis <= this is an improve candidate (default 3)") + i.add_argument("--plateau-rounds", type=int, default=3, help="rounds that must be flat to call 頭打ち (default 3)") + i.add_argument("--plateau-delta", type=float, default=0.05, help="max overall-mean gain still counted as flat (default 0.05)") + i.add_argument( + "--strict", action="store_true", + help="exit non-zero when the loop ends without convergence", + ) + i.set_defaults(func=cmd_improve) return p +def _add_judge_common_args(sp: argparse.ArgumentParser) -> None: + sp.add_argument( + "--reference", default=str(_REPO_ROOT / "data" / "solodit_checklist.csv"), + help="reference checklist CSV for the calibration bar " + "(default: data/solodit_checklist.csv, vendored from speca)", + ) + sp.add_argument( + "--ref-report", + help="reuse the reference scores from a previous `judge --out` report " + "instead of re-judging the reference corpus", + ) + sp.add_argument( + "--llm-cmd", + help="LLM adapter command: reads one prompt on stdin, writes the " + "response on stdout (e.g. 'claude -p'). Required; this repo holds " + "no API key", + ) + sp.add_argument( + "--axis-tolerance", type=float, default=0.25, + help="how far one axis mean may fall below the reference axis mean " + "while still passing (default 0.25)", + ) + + def _add_recall_data_args(sp: argparse.ArgumentParser) -> None: sp.add_argument( "--vulns-csv", default=str(_REPO_ROOT / "data" / "ethereum_vulns.csv"), diff --git a/src/speca_lean4/judge.py b/src/speca_lean4/judge.py new file mode 100644 index 0000000..2b329b0 --- /dev/null +++ b/src/speca_lean4/judge.py @@ -0,0 +1,582 @@ +"""Stage-2 quality judge + improve loop (speca#88 confirmed direction). + +eval here is NOT recall. The #88 direction comment ("重要な訂正") is explicit: +the goal is not to reproduce the vulnerability dataset's specific bugs, but to +reach the SAME QUALITY LEVEL as a professional audit checklist. So: + +- eval = LLM-as-judge scoring on five fixed axes (below), calibrated against + the vendored solodit reference checklist (`data/solodit_checklist.csv`): + the judge scores the reference corpus and the generated 01e corpus with the + SAME blind rubric, and the generated score distribution must be at least as + good as the reference distribution. No content matching against either the + reference or the dataset enters the verdict anywhere. +- the vuln dataset (`data/ethereum_vulns.csv`) is the IMPROVE-STEP TEACHING + MATERIAL only — never an eval denominator. (`recall.py`'s label recall is a + side reference number, deliberately outside the judge verdict.) + +Five axes (1-5 each, fixed rubric in `RUBRIC`): + specificity — code-level check, not a spec restatement + implementation_readiness — targets surfaces where implementations really + break (arithmetic width/bounds/resources/termination) + generality — not glued to one client's historical bug + actionability — an auditor can apply it to code as written + granularity — one auditable concern, no redundant bundling + +Loop (matches the #88 comment verbatim): + 1. generate — reuse the existing emit-01e / CHK-15 output (NOT re-implemented) + 2. judge — score every item on the five axes + 3. improve — low scorers get (a) the item, (b) the judge critique, + (c) matching vuln-dataset rows, and are sharpened + 4. re-judge — repeat 2-3 + 5. converge — stop only when BOTH hold: the score distribution meets the + reference bar AND the last `plateau_rounds` rounds are flat + (頭打ち). Neither condition alone stops the loop; a + `max_rounds` cap ends an unconverged run honestly + (`converged: false`, reason recorded). Per-round score + progression is logged. + +LLM access is INJECTED (`judge_fn` / `improve_fn`: prompt str -> response +str). This module never reads an API key and never imports an LLM SDK: unit +tests inject deterministic mocks; the CLI wires a subprocess command (e.g. a +self-hosted authenticated `claude -p`) via `subprocess_llm`. +""" + +from __future__ import annotations + +import csv +import json +import re +import statistics +import subprocess +from pathlib import Path +from typing import Any, Callable + +from .schema import validate_property + +_REPO_ROOT = Path(__file__).resolve().parents[2] +DEFAULT_REFERENCE_CSV = _REPO_ROOT / "data" / "solodit_checklist.csv" +DEFAULT_VULNS_CSV = _REPO_ROOT / "data" / "ethereum_vulns.csv" + +LLMFn = Callable[[str], str] + +AXES = ( + "specificity", + "implementation_readiness", + "generality", + "actionability", + "granularity", +) +SCORE_MIN, SCORE_MAX = 1, 5 + +# Improve may only rewrite the checklist surface of a property; everything +# else (identity, provenance, lean_status, label, severity, reachability...) +# is immutable, so an "improvement" can never quietly upgrade its own honesty +# metadata. +MUTABLE_FIELDS = ("text", "assertion") + +# Deterministic generality lint: an improved item must not hard-code a client +# or implementation name lifted from the evidence rows (that would optimize +# the generality axis's exact failure mode). +_CLIENT_NAMES = ( + "lighthouse", "prysm", "teku", "nimbus", "lodestar", "grandine", + "geth", "erigon", "nethermind", "besu", "reth", "blst", +) +_CLIENT_RE = re.compile( + r"\b(" + "|".join(_CLIENT_NAMES) + r")\b", re.IGNORECASE +) + +RUBRIC = """Score ONE audit-checklist item. Such an item tells a security +auditor what to inspect in the implementation source code of a protocol. + +Score five axes, each an integer 1-5. Anchors: + +specificity — is it a code-level check, not a specification restatement? + 1: restates a spec/theorem sentence in prose; nothing points at code. + 3: names the code area, but the condition to check stays abstract. + 5: names the exact code-level condition (field, arithmetic operation, + boundary, comparison set) that must hold. + +implementation_readiness — does it target a surface where implementations +actually break (arithmetic width, overflow/underflow, bounds/indexing, +resource caps, termination, type fidelity, boundary conditions)? + 1: an abstract property no concrete implementation would ever fail. + 3: mentions a real failure surface but does not pin the failure mode. + 5: pins a concrete failure mode on a concrete surface (e.g. "u64 value + above 2^53 in a lossy numeric type", "index used before bounds check"). + +generality — does it apply beyond one specific historical incident? + 1: only re-describes one bug in one codebase; useless elsewhere. + 3: generalizes the incident but keeps incidental specifics. + 5: any implementation of this protocol area can be audited against it. + +actionability — can an auditor apply it to code as written? + 1: the auditor must reformulate it before it is checkable. + 3: checkable, but where to look / what failure looks like is left implicit. + 5: says what to locate and what the violation looks like; directly usable. + +granularity — is it one auditable concern at auditable width? + 1: several unrelated checks bundled, or a vague catch-all. + 3: mostly one concern, with some bundling or overlap. + 5: exactly one concern, neither trivially narrow nor a grab-bag. + +Return STRICT JSON only (no markdown, no surrounding prose): +{"scores": {"specificity": n, "implementation_readiness": n, "generality": n, +"actionability": n, "granularity": n}, "critique": "<=60 words naming the weakest axes and why"}""" + + +class JudgeError(RuntimeError): + """A judge/improve LLM response could not be used (after retries).""" + + +# --------------------------------------------------------------- item loading + +def checklist_items_from_01e(doc: Any, id_prefix: str | None = None) -> list[dict[str, str]]: + """Normalize emitted 01e properties to blind judge items. + + Only the checklist surface (`text` + `assertion`) is exposed to the judge: + provenance fields (x_dataset_evidence and friends) never reach the prompt, + so the verdict cannot reward dataset-content matching, and the judge + cannot tell a generated item from a reference item by shape. + """ + props = doc.get("properties", []) if isinstance(doc, dict) else list(doc) + items = [] + for p in props: + pid = str(p.get("property_id", "")) + if id_prefix and not pid.startswith(id_prefix): + continue + items.append({ + "id": pid, + "check": str(p.get("text", "")), + "detail": str(p.get("assertion", "")), + }) + return items + + +def checklist_items_from_solodit(csv_path: str | Path = DEFAULT_REFERENCE_CSV) -> list[dict[str, str]]: + """Normalize the vendored solodit reference rows to the same blind shape.""" + with open(csv_path, encoding="utf-8-sig", newline="") as fh: + rows = list(csv.DictReader(fh)) + return [ + { + "id": str(r.get("id", "")), + "check": str(r.get("question", "")), + "detail": str(r.get("description", "")), + } + for r in rows + ] + + +# ------------------------------------------------------------------- judging + +def build_judge_prompt(item: dict[str, str]) -> str: + """Rubric + the item's checklist surface. Deliberately blind: no ids, no + corpus identity, no provenance — identical framing for reference and + generated items so the calibration is fair.""" + return ( + f"{RUBRIC}\n\n" + f"Item to score:\n" + f"CHECK: {item['check']}\n" + f"DETAIL: {item['detail']}\n" + ) + + +def _extract_json(text: str) -> dict[str, Any]: + """First JSON object anywhere in `text` (LLMs love to wrap JSON in prose).""" + dec = json.JSONDecoder() + for m in re.finditer(r"\{", text): + try: + obj, _ = dec.raw_decode(text[m.start():]) + except json.JSONDecodeError: + continue + if isinstance(obj, dict): + return obj + raise JudgeError(f"no JSON object in response: {text[:200]!r}") + + +def parse_judge_response(text: str) -> dict[str, Any]: + """Validate a judge response into {"scores": {axis: int}, "critique": str}. + + Every axis must be present and an integer in [1, 5] — a missing or + out-of-range axis is an error, never silently clamped or defaulted. + """ + obj = _extract_json(text) + raw = obj.get("scores") + if not isinstance(raw, dict): + raise JudgeError(f"response has no 'scores' object: {obj!r}") + scores: dict[str, int] = {} + for ax in AXES: + v = raw.get(ax) + if isinstance(v, bool) or not isinstance(v, int): + raise JudgeError(f"axis {ax!r} missing or not an integer: {v!r}") + if not SCORE_MIN <= v <= SCORE_MAX: + raise JudgeError(f"axis {ax!r} out of range [1,5]: {v}") + scores[ax] = v + critique = obj.get("critique") + if not isinstance(critique, str) or not critique.strip(): + raise JudgeError("response has no non-empty 'critique' string") + return {"scores": scores, "critique": critique.strip()} + + +def judge_item(item: dict[str, str], judge_fn: LLMFn, retries: int = 1) -> dict[str, Any]: + last: Exception | None = None + for _ in range(retries + 1): + try: + parsed = parse_judge_response(judge_fn(build_judge_prompt(item))) + return { + "id": item["id"], + "scores": parsed["scores"], + "overall": round(statistics.mean(parsed["scores"].values()), 3), + "critique": parsed["critique"], + } + except JudgeError as exc: + last = exc + raise JudgeError(f"item {item['id']}: {last}") + + +def judge_items(items: list[dict[str, str]], judge_fn: LLMFn, retries: int = 1) -> list[dict[str, Any]]: + if not items: + raise JudgeError("no items to judge") + return [judge_item(it, judge_fn, retries) for it in items] + + +# ----------------------------------------------------- distributions and bar + +def score_distribution(scored: list[dict[str, Any]]) -> dict[str, Any]: + overalls = [s["overall"] for s in scored] + return { + "n": len(scored), + "axis_means": { + ax: round(statistics.mean(s["scores"][ax] for s in scored), 3) + for ax in AXES + }, + "overall_mean": round(statistics.mean(overalls), 3), + "overall_median": round(statistics.median(overalls), 3), + "overall_min": round(min(overalls), 3), + } + + +def meets_reference_bar( + ours: dict[str, Any], reference: dict[str, Any], axis_tolerance: float = 0.25 +) -> tuple[bool, list[str]]: + """同等以上: our overall mean >= the reference overall mean, AND no axis + mean falls more than `axis_tolerance` below its reference axis mean (so a + single pumped axis cannot buy the verdict). Distribution-level only — + content similarity plays no part.""" + gaps: list[str] = [] + if ours["overall_mean"] < reference["overall_mean"]: + gaps.append( + f"overall_mean {ours['overall_mean']} < reference {reference['overall_mean']}" + ) + for ax in AXES: + lo = reference["axis_means"][ax] - axis_tolerance + if ours["axis_means"][ax] < lo: + gaps.append( + f"{ax} mean {ours['axis_means'][ax]} < reference " + f"{reference['axis_means'][ax]} - tolerance {axis_tolerance}" + ) + return (not gaps), gaps + + +def plateaued(history: list[float], rounds: int = 3, delta: float = 0.05) -> bool: + """頭打ち: over the last `rounds` recorded rounds, no round improved on the + earliest of that window by more than `delta`. Needs at least `rounds` + entries — a fresh run can never claim a plateau.""" + if len(history) < rounds: + return False + window = history[-rounds:] + return max(window) - window[0] <= delta + + +# ------------------------------------------------------------------- improve + +def select_low_items( + scored: list[dict[str, Any]], reference: dict[str, Any], low_axis: int = 3 +) -> list[dict[str, Any]]: + """An item needs improvement if its overall is below the reference overall + mean, or any single axis is at/below `low_axis`.""" + bar = reference["overall_mean"] + return [ + s for s in scored + if s["overall"] < bar or min(s["scores"].values()) <= low_axis + ] + + +_SEV_RANK = {"Critical": 0, "High": 1, "Medium": 2, "Low": 3} + + +def load_vulns(csv_path: str | Path = DEFAULT_VULNS_CSV) -> list[dict[str, str]]: + with open(csv_path, encoding="utf-8-sig", newline="") as fh: + return list(csv.DictReader(fh)) + + +def select_evidence( + label: str, vulns: list[dict[str, str]], n: int = 3 +) -> list[dict[str, str]]: + """Teaching-material rows for one item's failure class: same dataset + `label` first; if the label has no rows (e.g. fork-choice is outside the + vendored consensus slice), fall back to Critical/High rows of any label so + the improver still sees how real clients break. Deterministic order.""" + same = [v for v in vulns if v.get("label") == label] + pool = same or [v for v in vulns if v.get("severity") in ("Critical", "High")] or list(vulns) + pool = sorted(pool, key=lambda v: (_SEV_RANK.get(v.get("severity", ""), 9), v.get("id", ""))) + keep = ("id", "severity", "title", "label", "root_cause", "attack_path") + return [{k: v.get(k, "") for k in keep} for v in pool[:n]] + + +def build_improve_prompt( + prop: dict[str, Any], scored: dict[str, Any], evidence: list[dict[str, str]] +) -> str: + ev_lines = "\n".join( + f"- [{e['id']}] {e['severity']} {e['label']} / {e['root_cause']} " + f"(trigger: {e['attack_path']}): {e['title']}" + for e in evidence + ) + return ( + "You are sharpening ONE audit-checklist item so a security auditor can " + "apply it directly to implementation source code.\n\n" + "Current item:\n" + f"TEXT: {prop.get('text', '')}\n" + f"ASSERTION: {prop.get('assertion', '')}\n\n" + f"Judge scores (1-5): {json.dumps(scored['scores'])}\n" + f"Judge critique: {scored['critique']}\n\n" + "Real failure evidence from the vulnerability dataset — use the failure " + "CLASS (arithmetic width, bounds/indexing, resource caps, termination, " + "type fidelity), NOT the specific incident:\n" + f"{ev_lines}\n\n" + "Rewrite the item to raise the weak axes. Rules:\n" + "- Keep the same underlying invariant; sharpen it to the code-level " + "condition and concrete failure mode an implementation would hit.\n" + "- Stay general: NEVER name a specific client or implementation " + "(e.g. a client name from the evidence) in the rewritten item.\n" + "- TEXT: one imperative, code-level, audit-ready checklist sentence.\n" + "- ASSERTION: a compact machine-readable condition sketch.\n" + "Return STRICT JSON only: {\"text\": \"...\", \"assertion\": \"...\"}" + ) + + +def apply_improvement(prop: dict[str, Any], response_text: str) -> tuple[dict[str, Any] | None, str]: + """Validate an improve response against `prop`. Returns (new_prop, reason); + new_prop is None when the improvement is rejected (original kept). + + Guards (all deterministic): + - only MUTABLE_FIELDS are taken from the response; at least one must be a + non-empty string; + - the merged property must still pass schema.validate_property; + - the generality lint: no client/implementation name may enter the item; + - every immutable field is byte-identical afterwards by construction. + """ + try: + obj = _extract_json(response_text) + except JudgeError as exc: + return None, f"rejected: {exc}" + changes: dict[str, str] = {} + for k in MUTABLE_FIELDS: + v = obj.get(k) + if isinstance(v, str) and v.strip(): + changes[k] = v.strip() + if not changes: + return None, "rejected: response contains no usable mutable field (text/assertion)" + ignored = sorted(set(obj) - set(MUTABLE_FIELDS)) + for v in changes.values(): + m = _CLIENT_RE.search(v) + if m: + return None, f"rejected: client name {m.group(0)!r} in rewritten item (generality lint)" + new_prop = dict(prop) + new_prop.update(changes) + problems = validate_property(new_prop) + if problems: + return None, f"rejected: merged property fails schema: {problems}" + reason = "accepted" + if ignored: + reason += f" (ignored non-mutable keys: {', '.join(ignored)})" + return new_prop, reason + + +# ---------------------------------------------------------------------- loop + +def improve_loop( + props: list[dict[str, Any]], + reference: dict[str, Any], + vulns: list[dict[str, str]], + judge_fn: LLMFn, + improve_fn: LLMFn, + *, + max_rounds: int = 6, + low_axis: int = 3, + plateau_rounds: int = 3, + plateau_delta: float = 0.05, + axis_tolerance: float = 0.25, + evidence_n: int = 3, + retries: int = 1, +) -> dict[str, Any]: + """Judge -> improve -> re-judge until convergence. + + Convergence needs BOTH: `meets_reference_bar` AND `plateaued` over the + last `plateau_rounds` rounds. Bar-met-but-still-climbing keeps going; + plateaued-below-bar keeps going until `max_rounds`, then stops with + `converged: false` and the reason recorded — never dressed up as success. + + Returns {"rounds": [...], "history_overall_mean": [...], "converged": + bool, "stop_reason": str, "properties": final props}. + """ + if not props: + raise JudgeError("no properties to improve") + props = [dict(p) for p in props] + by_id = {str(p.get("property_id", "")): p for p in props} + if len(by_id) != len(props): + raise JudgeError("duplicate or missing property_id among input properties") + + def _judge_all(only_ids: set[str] | None, prev: dict[str, dict] | None) -> dict[str, dict]: + out: dict[str, dict] = {} + for pid, p in by_id.items(): + if only_ids is not None and pid not in only_ids and prev is not None: + out[pid] = prev[pid] + continue + item = {"id": pid, "check": str(p.get("text", "")), "detail": str(p.get("assertion", ""))} + out[pid] = judge_item(item, judge_fn, retries) + return out + + scored = _judge_all(None, None) + dist = score_distribution(list(scored.values())) + history = [dist["overall_mean"]] + meets, gaps = meets_reference_bar(dist, reference, axis_tolerance) + rounds: list[dict[str, Any]] = [{ + "round": 0, + "distribution": dist, + "meets_reference_bar": meets, + "bar_gaps": gaps, + "n_improve_candidates": 0, + "improvements": [], + "items": sorted(scored.values(), key=lambda s: s["id"]), + }] + + converged = False + stop_reason = "" + for rnd in range(1, max_rounds + 1): + meets, _ = meets_reference_bar(dist, reference, axis_tolerance) + if meets and plateaued(history, plateau_rounds, plateau_delta): + converged = True + stop_reason = "reference_bar_met_and_plateaued" + break + + low = select_low_items(list(scored.values()), reference, low_axis) + improvements: list[dict[str, str]] = [] + changed: set[str] = set() + for s in sorted(low, key=lambda s: s["id"]): + pid = s["id"] + prop = by_id[pid] + evidence = select_evidence(str(prop.get("label", "")), vulns, evidence_n) + new_prop, reason = apply_improvement( + prop, improve_fn(build_improve_prompt(prop, s, evidence)) + ) + improvements.append({"id": pid, "result": reason}) + if new_prop is not None and any( + new_prop.get(k) != prop.get(k) for k in MUTABLE_FIELDS + ): + by_id[pid] = new_prop + changed.add(pid) + + scored = _judge_all(changed, scored) + dist = score_distribution(list(scored.values())) + history.append(dist["overall_mean"]) + meets, gaps = meets_reference_bar(dist, reference, axis_tolerance) + rounds.append({ + "round": rnd, + "distribution": dist, + "meets_reference_bar": meets, + "bar_gaps": gaps, + "n_improve_candidates": len(low), + "improvements": improvements, + "items": sorted(scored.values(), key=lambda s: s["id"]), + }) + else: + meets, _ = meets_reference_bar(dist, reference, axis_tolerance) + if meets and plateaued(history, plateau_rounds, plateau_delta): + converged = True + stop_reason = "reference_bar_met_and_plateaued" + else: + stop_reason = "max_rounds_reached_without_convergence" + + return { + "reference": reference, + "params": { + "max_rounds": max_rounds, + "low_axis": low_axis, + "plateau_rounds": plateau_rounds, + "plateau_delta": plateau_delta, + "axis_tolerance": axis_tolerance, + }, + "rounds": rounds, + "history_overall_mean": history, + "converged": converged, + "stop_reason": stop_reason, + "properties": [by_id[str(p["property_id"])] for p in props], + } + + +# ------------------------------------------------------------ LLM subprocess + +def split_cmd(cmd: str) -> list[str]: + """Split an --llm-cmd string portably. POSIX shlex eats Windows path + backslashes, so on nt we split in non-POSIX mode and strip quotes.""" + import os + import shlex + if os.name == "nt": + return [t.strip('"') for t in shlex.split(cmd, posix=False)] + return shlex.split(cmd) + + +def subprocess_llm(cmd: list[str], timeout: int = 600) -> LLMFn: + """LLM adapter: run `cmd`, prompt on stdin, response on stdout. + + This is the ONLY place an actual LLM binding exists, and it is still just + a subprocess: e.g. `claude -p` on a self-hosted runner where the CLI is + already authenticated. No API key is read or forwarded here. + """ + def call(prompt: str) -> str: + proc = subprocess.run( + cmd, input=prompt, capture_output=True, text=True, + encoding="utf-8", timeout=timeout, + ) + if proc.returncode != 0: + raise JudgeError( + f"llm command {' '.join(cmd)!r} failed (rc={proc.returncode}): " + f"{(proc.stderr or '')[-500:]}" + ) + return proc.stdout + return call + + +# ---------------------------------------------------------------- formatting + +def format_judge_summary(report: dict[str, Any]) -> str: + ref, ours = report["reference"], report["ours"] + lines = [ + f"reference bar ({report['reference_source']}, n={ref['n']}): " + f"overall mean {ref['overall_mean']}, axes {ref['axis_means']}", + f"ours ({report['ours_source']}, n={ours['n']}): " + f"overall mean {ours['overall_mean']}, axes {ours['axis_means']}", + f"meets reference bar (axis tolerance {report['axis_tolerance']}): " + f"{report['meets_reference_bar']}", + ] + for g in report["bar_gaps"]: + lines.append(f" GAP: {g}") + for s in report["items"]: + lines.append(f" {s['id']}: overall {s['overall']} {s['scores']}") + return "\n".join(lines) + + +def format_improve_summary(result: dict[str, Any]) -> str: + lines = [ + f"improve loop: {len(result['rounds'])} round(s), converged={result['converged']} " + f"({result['stop_reason']})", + f"overall-mean progression: {result['history_overall_mean']}", + ] + for r in result["rounds"]: + lines.append( + f" round {r['round']}: overall {r['distribution']['overall_mean']} " + f"meets_bar={r['meets_reference_bar']} " + f"improved {sum(1 for i in r['improvements'] if i['result'].startswith('accepted'))}" + f"/{r['n_improve_candidates']} candidates" + ) + return "\n".join(lines) diff --git a/tests/fixtures/mock_llm.py b/tests/fixtures/mock_llm.py new file mode 100644 index 0000000..608cf1e --- /dev/null +++ b/tests/fixtures/mock_llm.py @@ -0,0 +1,47 @@ +"""Deterministic stand-in for the --llm-cmd adapter (CI runs with NO API key). + +Reads one prompt on stdin, writes one response on stdout — the same contract +`judge.subprocess_llm` expects from e.g. `claude -p`. Judge prompts get a +fixed five-axis score derived (deterministically) from the item text hash so +distributions are stable but non-degenerate; improve prompts get a sharpened +text/assertion rewrite. +""" + +from __future__ import annotations + +import hashlib +import json +import re +import sys + + +def main() -> int: + # the adapter contract is UTF-8 on both pipes regardless of locale + sys.stdin.reconfigure(encoding="utf-8") + sys.stdout.reconfigure(encoding="utf-8") + prompt = sys.stdin.read() + if "sharpening ONE audit-checklist item" in prompt: + m = re.search(r"^TEXT: (.*)$", prompt, re.MULTILINE) + base = (m.group(1).strip() if m else "the checked invariant").rstrip(".") + print(json.dumps({ + "text": f"{base} — verify the exact uint64 arithmetic, bounds checks " + "and rejection path on the decode-to-comparison route", + "assertion": "forall f in decoded_fields: width(f) == spec_width(f) " + "and bounds_checked(f) before use(f)", + })) + return 0 + # judge prompt: deterministic per-item scores in 3..5 keyed off the CHECK line + m = re.search(r"^CHECK: (.*)$", prompt, re.MULTILINE) + seed = hashlib.sha256((m.group(1) if m else prompt).encode()).digest() + axes = ["specificity", "implementation_readiness", "generality", + "actionability", "granularity"] + scores = {ax: 3 + seed[i] % 3 for i, ax in enumerate(axes)} + print(json.dumps({ + "scores": scores, + "critique": "mock: deterministic scores for CI wiring only", + })) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/test_judge.py b/tests/test_judge.py new file mode 100644 index 0000000..c3ec4e3 --- /dev/null +++ b/tests/test_judge.py @@ -0,0 +1,536 @@ +"""Tests for the speca#88 stage-2 quality judge + improve loop. + +Everything here runs WITHOUT an LLM: the pure logic (prompt construction, +response parsing, distribution math, bar verdict, plateau/convergence, the +improve guards) is exercised with deterministic injected functions, and the +CLI wiring with the `tests/fixtures/mock_llm.py` subprocess stand-in. The +design point under test throughout: eval is a QUALITY-distribution +comparison, never content matching (not recall). +""" + +from __future__ import annotations + +import hashlib +import json +import sys +from pathlib import Path + +import pytest + +from speca_lean4.judge import ( + AXES, + JudgeError, + apply_improvement, + build_improve_prompt, + build_judge_prompt, + checklist_items_from_01e, + checklist_items_from_solodit, + improve_loop, + judge_item, + judge_items, + meets_reference_bar, + parse_judge_response, + plateaued, + score_distribution, + select_evidence, + select_low_items, + split_cmd, +) + +_ROOT = Path(__file__).resolve().parents[1] +_FIX = Path(__file__).resolve().parent / "fixtures" +_DATA = _ROOT / "data" + + +def _scores(v: int) -> dict[str, int]: + return {ax: v for ax in AXES} + + +def _judge_json(v: int, critique: str = "flat") -> str: + return json.dumps({"scores": _scores(v), "critique": critique}) + + +def _dist(v: float) -> dict: + return { + "n": 1, + "axis_means": {ax: v for ax in AXES}, + "overall_mean": v, + "overall_median": v, + "overall_min": v, + } + + +_PROP = { + "property_id": "CHK-T-01", + "text": "Slashing comparisons must use exact uint64 fields", + "assertion": "forall f in slashing_fields: exact_uint64(f)", + "type": "invariant", + "severity": "HIGH", + "covers": "process_slashings", + "reachability": { + "classification": "external-reachable", + "entry_points": ["CallbackHandler"], + "attacker_controlled": True, + "bug_bounty_scope": "in-scope", + }, + "bug_bounty_eligible": True, + "exploitability": "external-attack", + "lean_status": "descends-from-proved", + "label": "beacon-chain:slashing", +} + + +def _prop(pid: str, text: str = "check something concrete", label: str = "beacon-chain:slashing") -> dict: + p = dict(_PROP) + p["property_id"] = pid + p["text"] = text + p["label"] = label + return p + + +# ------------------------------------------------------------ prompt hygiene + +def test_judge_prompt_is_blind_and_axis_complete(): + item = {"id": "CHK-X-01", "check": "the check", "detail": "the assertion"} + prompt = build_judge_prompt(item) + for ax in AXES: + assert ax in prompt + assert "the check" in prompt and "the assertion" in prompt + # blind: no item id, no corpus identity, no dataset mention -> the verdict + # cannot reward content matching or source recognition (eval != recall) + assert "CHK-X-01" not in prompt + for leak in ("solodit", "ethereum_vulns", "ethereum-vuln-dataset", "recall", "01e"): + assert leak not in prompt.lower(), leak + + +def test_reference_and_generated_items_share_one_prompt_shape(): + sol = checklist_items_from_solodit(_DATA / "solodit_checklist.csv")[0] + gen = {"id": "CHK-A", "check": "c", "detail": "d"} + p1, p2 = build_judge_prompt(sol), build_judge_prompt(gen) + # identical framing apart from the item content itself + assert p1.split("Item to score:")[0] == p2.split("Item to score:")[0] + + +def test_01e_items_expose_only_the_checklist_surface(): + doc = {"properties": [dict(_PROP, x_dataset_evidence="SECRET-EVIDENCE")]} + items = checklist_items_from_01e(doc) + assert items == [{ + "id": "CHK-T-01", + "check": _PROP["text"], + "detail": _PROP["assertion"], + }] + assert "SECRET-EVIDENCE" not in build_judge_prompt(items[0]) + + +def test_01e_id_prefix_filter(): + doc = {"properties": [_prop("CHK-A-01"), _prop("PROP-lean-1")]} + assert [i["id"] for i in checklist_items_from_01e(doc, "CHK-")] == ["CHK-A-01"] + assert len(checklist_items_from_01e(doc)) == 2 + + +# ------------------------------------------------------------------ parsing + +def test_parse_judge_response_strict_json(): + parsed = parse_judge_response(_judge_json(4, "ok")) + assert parsed["scores"] == _scores(4) + assert parsed["critique"] == "ok" + + +def test_parse_judge_response_json_embedded_in_prose(): + parsed = parse_judge_response("Sure! Here is my score:\n" + _judge_json(3) + "\nHope this helps.") + assert parsed["scores"]["specificity"] == 3 + + +@pytest.mark.parametrize("bad", [ + "no json at all", + json.dumps({"scores": {ax: 4 for ax in AXES if ax != "granularity"}, "critique": "x"}), + json.dumps({"scores": dict(_scores(4), specificity=0), "critique": "x"}), + json.dumps({"scores": dict(_scores(4), specificity=6), "critique": "x"}), + json.dumps({"scores": dict(_scores(4), specificity=True), "critique": "x"}), + json.dumps({"scores": dict(_scores(4), specificity=4.5), "critique": "x"}), + json.dumps({"scores": _scores(4), "critique": " "}), + json.dumps({"scores": _scores(4)}), +]) +def test_parse_judge_response_rejects(bad): + with pytest.raises(JudgeError): + parse_judge_response(bad) + + +def test_judge_item_retries_then_fails_honestly(): + calls = [] + + def flaky(prompt): + calls.append(prompt) + return "garbage" if len(calls) == 1 else _judge_json(5) + + s = judge_item({"id": "a", "check": "c", "detail": "d"}, flaky, retries=1) + assert s["overall"] == 5.0 and len(calls) == 2 + + with pytest.raises(JudgeError, match="always-bad"): + judge_item({"id": "always-bad", "check": "c", "detail": "d"}, + lambda p: "garbage", retries=1) + + +def test_judge_items_empty_is_an_error(): + with pytest.raises(JudgeError): + judge_items([], lambda p: _judge_json(4)) + + +# ------------------------------------------------- distribution + bar verdict + +def test_score_distribution_math(): + scored = [ + {"id": "a", "scores": _scores(3), "overall": 3.0, "critique": "x"}, + {"id": "b", "scores": _scores(5), "overall": 5.0, "critique": "x"}, + ] + d = score_distribution(scored) + assert d["n"] == 2 + assert d["overall_mean"] == 4.0 + assert d["overall_median"] == 4.0 + assert d["overall_min"] == 3.0 + assert d["axis_means"] == {ax: 4.0 for ax in AXES} + + +def test_meets_reference_bar_equal_passes(): + ok, gaps = meets_reference_bar(_dist(4.0), _dist(4.0)) + assert ok and gaps == [] + + +def test_meets_reference_bar_overall_below_fails(): + ok, gaps = meets_reference_bar(_dist(3.9), _dist(4.0)) + assert not ok and any("overall_mean" in g for g in gaps) + + +def test_meets_reference_bar_axis_tolerance(): + ours = _dist(4.2) + ours["axis_means"] = dict(ours["axis_means"], generality=3.8) + ok, _ = meets_reference_bar(ours, _dist(4.0), axis_tolerance=0.25) + assert ok # 3.8 >= 4.0 - 0.25 + ours["axis_means"] = dict(ours["axis_means"], generality=3.7) + ok, gaps = meets_reference_bar(ours, _dist(4.0), axis_tolerance=0.25) + assert not ok and any("generality" in g for g in gaps) + + +def test_one_pumped_axis_cannot_buy_the_verdict(): + ours = _dist(4.5) # overall above the bar... + ours["axis_means"] = dict(_dist(4.5)["axis_means"], actionability=3.0) + ok, gaps = meets_reference_bar(ours, _dist(4.0)) + assert not ok and any("actionability" in g for g in gaps) + + +def test_plateaued(): + assert not plateaued([4.0]) # too short to claim 頭打ち + assert not plateaued([4.0, 4.0]) + assert plateaued([4.0, 4.0, 4.0]) + assert plateaued([3.0, 4.0, 4.0, 4.04]) # window is the LAST 3 + assert not plateaued([4.0, 4.0, 4.2]) # still climbing + assert not plateaued([3.0, 3.5, 4.0]) + assert plateaued([4.2, 4.0, 4.1]) # dip-and-recover is flat + + +# ------------------------------------------------------------------- improve + +def test_select_low_items(): + ref = _dist(4.0) + a = {"id": "a", "scores": _scores(5), "overall": 5.0, "critique": "x"} + b = {"id": "b", "scores": _scores(4), "overall": 4.0, "critique": "x"} # at bar, no low axis + c = {"id": "c", "scores": dict(_scores(5), generality=3), "overall": 4.6, "critique": "x"} + d = {"id": "d", "scores": _scores(4), "overall": 3.9, "critique": "x"} + low = select_low_items([a, b, c, d], ref, low_axis=3) + assert [s["id"] for s in low] == ["c", "d"] + + +def test_select_evidence_label_match_then_fallback(): + vulns = [ + {"id": "V3", "severity": "High", "label": "beacon-chain:slashing", + "root_cause": "integer_overflow_underflow", "attack_path": "malicious_block", "title": "t3"}, + {"id": "V1", "severity": "Critical", "label": "beacon-chain:slashing", + "root_cause": "type_confusion", "attack_path": "malicious_block", "title": "t1"}, + {"id": "V2", "severity": "Critical", "label": "beacon-chain:justification-and-finality", + "root_cause": "consensus_divergence", "attack_path": "crafted_state", "title": "t2"}, + {"id": "V4", "severity": "Low", "label": "beacon-chain:slashing", + "root_cause": "x", "attack_path": "y", "title": "t4"}, + ] + ev = select_evidence("beacon-chain:slashing", vulns, n=2) + assert [e["id"] for e in ev] == ["V1", "V3"] # severity then id, capped + # label with no rows: falls back to Critical/High rows of any label + ev = select_evidence("fork-choice", vulns, n=3) + assert [e["id"] for e in ev] == ["V1", "V2", "V3"] + assert set(ev[0]) == {"id", "severity", "title", "label", "root_cause", "attack_path"} + + +def test_evidence_selection_is_deterministic_on_real_data(): + from speca_lean4.judge import load_vulns + vulns = load_vulns(_DATA / "ethereum_vulns.csv") + assert select_evidence("beacon-chain:slashing", vulns) == \ + select_evidence("beacon-chain:slashing", vulns) + + +def test_improve_prompt_carries_item_critique_and_evidence(): + scored = {"id": "CHK-T-01", "scores": dict(_scores(4), specificity=2), + "overall": 3.6, "critique": "too abstract"} + ev = [{"id": "V1", "severity": "Critical", "title": "u64 as float", "label": "l", + "root_cause": "integer_overflow_underflow", "attack_path": "malicious_block"}] + prompt = build_improve_prompt(_PROP, scored, ev) + assert _PROP["text"] in prompt and _PROP["assertion"] in prompt # (a) the item + assert "too abstract" in prompt # (b) the critique + assert "V1" in prompt and "u64 as float" in prompt # (c) dataset rows + assert "NEVER name a specific client" in prompt + + +def test_apply_improvement_accepts_and_keeps_immutables(): + new, reason = apply_improvement(_PROP, json.dumps({ + "text": "Exact uint64 comparison on every slashing field from decode to compare", + "assertion": "forall f: width(f)==u64 and not lossy(f)", + "lean_status": "proved", # attempted upgrade must be ignored + "severity": "CRITICAL", + })) + assert new is not None + assert reason.startswith("accepted") + assert "ignored non-mutable keys" in reason + assert new["lean_status"] == "descends-from-proved" # untouched + assert new["severity"] == "HIGH" # untouched + assert new["property_id"] == _PROP["property_id"] + assert new["text"].startswith("Exact uint64") + + +@pytest.mark.parametrize("resp,frag", [ + ("not json", "rejected"), + (json.dumps({"other": "x"}), "no usable mutable field"), + (json.dumps({"text": " "}), "no usable mutable field"), + (json.dumps({"text": "Reject the Lighthouse-style cursor reuse"}), "generality lint"), + (json.dumps({"assertion": "as prysm does"}), "generality lint"), +]) +def test_apply_improvement_rejections(resp, frag): + new, reason = apply_improvement(_PROP, resp) + assert new is None and frag in reason + + +# ---------------------------------------------------------------------- loop + +def test_loop_converges_only_when_bar_met_AND_plateaued(): + """Bar is met from round 1, but the loop must still run until the last 3 + rounds are flat — bar alone never stops it.""" + ref = _dist(4.0) + + def judge_fn(prompt): + # stateless: a sharpened item scores 5, an unsharpened one 3 + check = prompt.split("CHECK: ")[1].splitlines()[0] + return _judge_json(5 if check.startswith("sharper text") else 3) + + def improve_fn(prompt): + orig = prompt.split("TEXT: ")[1].splitlines()[0] + return json.dumps({"text": f"sharper text: {orig}", + "assertion": "width(f)==u64"}) + + props = [_prop("CHK-A-01", "text a"), _prop("CHK-B-01", "text b")] + res = improve_loop(props, ref, [], judge_fn, improve_fn, max_rounds=6) + assert res["converged"] is True + assert res["stop_reason"] == "reference_bar_met_and_plateaued" + # round0 3.0 -> improved to 5.0, then frozen until the 3-round window is flat + assert res["history_overall_mean"] == [3.0, 5.0, 5.0, 5.0] + assert [r["round"] for r in res["rounds"]] == [0, 1, 2, 3] + # bar was met from round 1 on, yet the loop kept going to round 3 + assert res["rounds"][1]["meets_reference_bar"] is True + # improved text landed in the final properties + assert all(p["text"].startswith("sharper text") for p in res["properties"]) + + +def test_loop_does_not_stop_on_plateau_below_bar(): + """Plateaued-but-below-bar must run to max_rounds and end unconverged — + the honest outcome, never dressed up.""" + ref = _dist(4.5) + res = improve_loop( + [_prop("CHK-A-01")], ref, [], + judge_fn=lambda p: _judge_json(3), + improve_fn=lambda p: json.dumps({"text": "still weak but different"}), + max_rounds=4, + ) + assert res["converged"] is False + assert res["stop_reason"] == "max_rounds_reached_without_convergence" + assert res["history_overall_mean"] == [3.0] * 5 + assert len(res["rounds"]) == 5 + assert all(not r["meets_reference_bar"] for r in res["rounds"]) + + +def test_loop_judges_blind_and_improves_with_evidence(): + """eval != recall, structurally: judge prompts never contain dataset rows; + improve prompts do.""" + judge_prompts, improve_prompts = [], [] + vulns = [{"id": "VULN-X1", "severity": "Critical", "label": "beacon-chain:slashing", + "root_cause": "integer_overflow_underflow", + "attack_path": "malicious_block", "title": "evidence row"}] + + def judge_fn(p): + judge_prompts.append(p) + return _judge_json(3) + + def improve_fn(p): + improve_prompts.append(p) + return json.dumps({"text": "sharper checklist text"}) + + improve_loop([_prop("CHK-A-01")], _dist(4.5), vulns, judge_fn, improve_fn, + max_rounds=2) + assert improve_prompts, "no improve round ran" + assert all("VULN-X1" not in p for p in judge_prompts) + assert all("VULN-X1" in p for p in improve_prompts) + + +def test_loop_rejected_improvement_keeps_original_and_is_logged(): + res = improve_loop( + [_prop("CHK-A-01", "original text")], _dist(4.5), [], + judge_fn=lambda p: _judge_json(3), + improve_fn=lambda p: json.dumps({"text": "do it like Lighthouse does"}), + max_rounds=2, + ) + assert res["properties"][0]["text"] == "original text" + results = [i["result"] for r in res["rounds"] for i in r["improvements"]] + assert results and all("generality lint" in x for x in results) + + +def test_loop_logs_score_progression_per_round(): + res = improve_loop( + [_prop("CHK-A-01")], _dist(4.5), [], + judge_fn=lambda p: _judge_json(4), + improve_fn=lambda p: json.dumps({"text": "x" * 30}), + max_rounds=3, + ) + assert len(res["history_overall_mean"]) == len(res["rounds"]) + for r in res["rounds"]: + assert set(r) >= {"round", "distribution", "meets_reference_bar", + "bar_gaps", "n_improve_candidates", "improvements", "items"} + assert r["distribution"]["overall_mean"] == res["history_overall_mean"][r["round"]] + + +def test_loop_duplicate_property_id_is_an_error(): + with pytest.raises(JudgeError): + improve_loop([_prop("CHK-A-01"), _prop("CHK-A-01")], _dist(4.0), [], + lambda p: _judge_json(4), lambda p: "{}") + + +# ------------------------------------------------- vendored solodit reference + +def test_solodit_vendored_provenance_matches_meta(): + """The vendored bytes must still be the pinned speca blob: recompute the + git blob sha from the file so silent edits/CRLF churn cannot hide.""" + meta = json.loads((_DATA / "solodit_checklist.meta.json").read_text(encoding="utf-8")) + raw = (_DATA / "solodit_checklist.csv").read_bytes() + blob_sha = hashlib.sha1(b"blob %d\x00" % len(raw) + raw).hexdigest() + assert blob_sha == meta["source_blob_sha"] + assert b"\r" not in raw, "CRLF crept into the vendored reference" + items = checklist_items_from_solodit(_DATA / "solodit_checklist.csv") + assert len(items) == meta["n_rows"] == 52 + assert all(i["id"] and i["check"] for i in items) + + +def test_solodit_loader_shape(): + items = checklist_items_from_solodit(_DATA / "solodit_checklist.csv") + assert items[0]["id"] == "SOL-AM-DOSA-1" + assert set(items[0]) == {"id", "check", "detail"} + + +# ---------------------------------------------------------------- CLI wiring + +def _mock_cmd() -> str: + return f'"{sys.executable}" "{_FIX / "mock_llm.py"}"' + + +def test_split_cmd(): + parts = split_cmd(_mock_cmd()) + assert parts[0] == sys.executable + assert parts[1] == str(_FIX / "mock_llm.py") + assert split_cmd("claude -p --model haiku") == ["claude", "-p", "--model", "haiku"] + + +@pytest.fixture +def chk_01e(tmp_path) -> Path: + from speca_lean4.cli import main + + out = tmp_path / "01e_lean.json" + rc = main([ + "emit-01e", + "--scope", str(_FIX / "bug_bounty_scope.sample.json"), + "--health-json", str(_FIX / "theorem_health.sample.json"), + "--out", str(out), + ]) + assert rc == 0 + return out + + +def test_cli_judge_end_to_end_with_mock(chk_01e, tmp_path, capsys): + from speca_lean4.cli import main + + out = tmp_path / "judge_report.json" + rc = main([ + "judge", "--ours", str(chk_01e), "--id-prefix", "CHK-", + "--llm-cmd", _mock_cmd(), "--out", str(out), + ]) + assert rc == 0 + report = json.loads(out.read_text(encoding="utf-8")) + assert report["ours"]["n"] == 15 # the CHK-15 checklist + assert report["reference"]["n"] == 52 # the solodit bar + assert len(report["items"]) == 15 + assert len(report["reference_items"]) == 52 + assert isinstance(report["meets_reference_bar"], bool) + for s in report["items"]: + assert set(s["scores"]) == set(AXES) + assert "reference bar" in capsys.readouterr().out + + +def test_cli_judge_without_llm_cmd_fails_with_guidance(chk_01e, capsys): + from speca_lean4.cli import main + + rc = main(["judge", "--ours", str(chk_01e)]) + assert rc == 2 + assert "API key" in capsys.readouterr().err + + +def test_cli_improve_end_to_end_with_mock(chk_01e, tmp_path): + from speca_lean4.cli import main + + # reuse the reference scores via --ref-report to skip re-judging solodit + report = tmp_path / "judge_report.json" + assert main(["judge", "--ours", str(chk_01e), "--id-prefix", "CHK-", + "--llm-cmd", _mock_cmd(), "--out", str(report)]) == 0 + out_dir = tmp_path / "improve_run" + rc = main([ + "improve", "--ours", str(chk_01e), "--id-prefix", "CHK-", + "--llm-cmd", _mock_cmd(), "--ref-report", str(report), + "--out-dir", str(out_dir), "--max-rounds", "3", + ]) + assert rc == 0 + log = json.loads((out_dir / "score_log.json").read_text(encoding="utf-8")) + assert log["rounds"] and log["history_overall_mean"] + assert isinstance(log["converged"], bool) + assert log["stop_reason"] + assert log["reference"]["n"] == 52 + improved = json.loads((out_dir / "improved_01e.json").read_text(encoding="utf-8")) + props = improved["properties"] + assert len(props) == 15 + assert "x_improve_note" in improved + # immutables survived the loop; only text/assertion may differ + orig = {p["property_id"]: p for p in + json.loads(chk_01e.read_text(encoding="utf-8"))["properties"] + if p["property_id"].startswith("CHK-")} + for p in props: + o = orig[p["property_id"]] + for k in o: + if k not in ("text", "assertion"): + assert p[k] == o[k], (p["property_id"], k) + + +def test_cli_improve_strict_flags_nonconvergence(chk_01e, tmp_path, capsys): + from speca_lean4.cli import main + + report = tmp_path / "judge_report.json" + assert main(["judge", "--ours", str(chk_01e), "--id-prefix", "CHK-", + "--llm-cmd", _mock_cmd(), "--out", str(report)]) == 0 + out_dir = tmp_path / "improve_run" + rc = main([ + "improve", "--ours", str(chk_01e), "--id-prefix", "CHK-", + "--llm-cmd", _mock_cmd(), "--ref-report", str(report), + "--out-dir", str(out_dir), "--max-rounds", "1", "--strict", + ]) + # one round can never satisfy the 3-round plateau half of convergence + assert rc == 1 + assert "did not converge" in capsys.readouterr().err From 3f0b99f5ec546d3cc7a30105ed4f05dfca077008 Mon Sep 17 00:00:00 2001 From: sururu-k <2009hirotake@gmail.com> Date: Wed, 22 Jul 2026 21:00:41 +0900 Subject: [PATCH 2/3] feat: retry transient LLM-adapter failures with backoff MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Observed on the first real run (local authenticated claude -p, sonnet): one intermittent rc=1 with empty stderr killed a 67-call judge run at item 20, and an immediate same-second retry also failed. judge_item's retries now cover adapter failures as well as bad responses, with a --retry-wait pause between attempts (CLI defaults: --retries 2, --retry-wait 5). An item still failing after the retries aborts the run — never silently skipped, so a mass-refusing or dead adapter cannot produce a thin-but-green report. --- src/speca_lean4/cli.py | 15 +++++++++++++-- src/speca_lean4/judge.py | 27 ++++++++++++++++++++------- tests/test_judge.py | 16 ++++++++++++++++ 3 files changed, 49 insertions(+), 9 deletions(-) diff --git a/src/speca_lean4/cli.py b/src/speca_lean4/cli.py index 807e06b..c4ccf5a 100644 --- a/src/speca_lean4/cli.py +++ b/src/speca_lean4/cli.py @@ -328,7 +328,7 @@ def _reference_distribution(args: argparse.Namespace, judge_fn) -> tuple[dict, l prev = _load_json(args.ref_report) return prev["reference"], prev["reference_items"], prev["reference_source"] items = checklist_items_from_solodit(args.reference) - scored = judge_items(items, judge_fn) + scored = judge_items(items, judge_fn, args.retries, args.retry_wait) return score_distribution(scored), scored, str(args.reference) @@ -350,7 +350,7 @@ def cmd_judge(args: argparse.Namespace) -> int: f"(id prefix: {args.id_prefix or 'none'})", file=sys.stderr) return 2 ref_dist, ref_items, ref_source = _reference_distribution(args, judge_fn) - scored = judge_items(ours_items, judge_fn) + scored = judge_items(ours_items, judge_fn, args.retries, args.retry_wait) ours_dist = score_distribution(scored) meets, gaps = meets_reference_bar(ours_dist, ref_dist, args.axis_tolerance) report = { @@ -410,6 +410,7 @@ def cmd_improve(args: argparse.Namespace) -> int: max_rounds=args.max_rounds, low_axis=args.low_axis, plateau_rounds=args.plateau_rounds, plateau_delta=args.plateau_delta, axis_tolerance=args.axis_tolerance, + retries=args.retries, retry_wait=args.retry_wait, ) out_dir = Path(args.out_dir) @@ -590,6 +591,16 @@ def _add_judge_common_args(sp: argparse.ArgumentParser) -> None: help="how far one axis mean may fall below the reference axis mean " "while still passing (default 0.25)", ) + sp.add_argument( + "--retries", type=int, default=2, + help="attempts per item beyond the first, covering bad responses AND " + "transient adapter failures (default 2); an item still failing " + "after that aborts the run — never silently skipped", + ) + sp.add_argument( + "--retry-wait", type=float, default=5.0, + help="seconds between attempts, letting rate-limit blips pass (default 5)", + ) def _add_recall_data_args(sp: argparse.ArgumentParser) -> None: diff --git a/src/speca_lean4/judge.py b/src/speca_lean4/judge.py index 2b329b0..eb11aee 100644 --- a/src/speca_lean4/judge.py +++ b/src/speca_lean4/judge.py @@ -48,6 +48,7 @@ import re import statistics import subprocess +import time from pathlib import Path from typing import Any, Callable @@ -217,9 +218,17 @@ def parse_judge_response(text: str) -> dict[str, Any]: return {"scores": scores, "critique": critique.strip()} -def judge_item(item: dict[str, str], judge_fn: LLMFn, retries: int = 1) -> dict[str, Any]: +def judge_item( + item: dict[str, str], judge_fn: LLMFn, retries: int = 1, retry_wait: float = 0.0 +) -> dict[str, Any]: + """`retries` covers BOTH bad responses and transient adapter failures + (e.g. a real CLI intermittently exiting non-zero mid-run); `retry_wait` + seconds between attempts lets rate-limit blips pass. After the retries + the error surfaces — an unscorable item is never silently skipped.""" last: Exception | None = None - for _ in range(retries + 1): + for attempt in range(retries + 1): + if attempt and retry_wait > 0: + time.sleep(retry_wait) try: parsed = parse_judge_response(judge_fn(build_judge_prompt(item))) return { @@ -233,10 +242,12 @@ def judge_item(item: dict[str, str], judge_fn: LLMFn, retries: int = 1) -> dict[ raise JudgeError(f"item {item['id']}: {last}") -def judge_items(items: list[dict[str, str]], judge_fn: LLMFn, retries: int = 1) -> list[dict[str, Any]]: +def judge_items( + items: list[dict[str, str]], judge_fn: LLMFn, retries: int = 1, retry_wait: float = 0.0 +) -> list[dict[str, Any]]: if not items: raise JudgeError("no items to judge") - return [judge_item(it, judge_fn, retries) for it in items] + return [judge_item(it, judge_fn, retries, retry_wait) for it in items] # ----------------------------------------------------- distributions and bar @@ -408,6 +419,7 @@ def improve_loop( axis_tolerance: float = 0.25, evidence_n: int = 3, retries: int = 1, + retry_wait: float = 0.0, ) -> dict[str, Any]: """Judge -> improve -> re-judge until convergence. @@ -433,7 +445,7 @@ def _judge_all(only_ids: set[str] | None, prev: dict[str, dict] | None) -> dict[ out[pid] = prev[pid] continue item = {"id": pid, "check": str(p.get("text", "")), "detail": str(p.get("assertion", ""))} - out[pid] = judge_item(item, judge_fn, retries) + out[pid] = judge_item(item, judge_fn, retries, retry_wait) return out scored = _judge_all(None, None) @@ -540,8 +552,9 @@ def call(prompt: str) -> str: ) if proc.returncode != 0: raise JudgeError( - f"llm command {' '.join(cmd)!r} failed (rc={proc.returncode}): " - f"{(proc.stderr or '')[-500:]}" + f"llm command {' '.join(cmd)!r} failed (rc={proc.returncode}); " + f"stderr tail: {(proc.stderr or '')[-500:]} " + f"stdout tail: {(proc.stdout or '')[-200:]}" ) return proc.stdout return call diff --git a/tests/test_judge.py b/tests/test_judge.py index c3ec4e3..2c69ded 100644 --- a/tests/test_judge.py +++ b/tests/test_judge.py @@ -171,6 +171,22 @@ def flaky(prompt): lambda p: "garbage", retries=1) +def test_judge_item_retries_transient_adapter_failures_too(): + """A real adapter (e.g. `claude -p`) can exit non-zero intermittently + mid-run; that must be retried like a bad response, not kill the run.""" + calls = [] + + def flaky_adapter(prompt): + calls.append(prompt) + if len(calls) == 1: + raise JudgeError("llm command failed (rc=1)") + return _judge_json(4) + + s = judge_item({"id": "a", "check": "c", "detail": "d"}, flaky_adapter, + retries=1, retry_wait=0.0) + assert s["overall"] == 4.0 and len(calls) == 2 + + def test_judge_items_empty_is_an_error(): with pytest.raises(JudgeError): judge_items([], lambda p: _judge_json(4)) From 24ba8a5c00c8a13dfcd61d64b31caacdfee9e641 Mon Sep 17 00:00:00 2001 From: sururu-k <2009hirotake@gmail.com> Date: Wed, 22 Jul 2026 21:05:32 +0900 Subject: [PATCH 3/3] feat: treat a hung LLM adapter as a retryable failure Second real-run lesson (local claude -p): one adapter call hung for 19+ minutes; subprocess.run's TimeoutExpired then escaped judge_item's retry net entirely and killed the run. subprocess_llm now converts the timeout into JudgeError (kill + retry like any transient failure) and the CLI exposes --llm-timeout (default 600s) so a flaky adapter recycles fast. --- src/speca_lean4/cli.py | 18 +++++++++++++----- src/speca_lean4/judge.py | 15 +++++++++++---- tests/test_judge.py | 9 +++++++++ 3 files changed, 33 insertions(+), 9 deletions(-) diff --git a/src/speca_lean4/cli.py b/src/speca_lean4/cli.py index c4ccf5a..0e66cc6 100644 --- a/src/speca_lean4/cli.py +++ b/src/speca_lean4/cli.py @@ -303,7 +303,7 @@ def cmd_verify_recall(args: argparse.Namespace) -> int: return 0 -def _make_llm(cmd: str | None, what: str): +def _make_llm(cmd: str | None, what: str, timeout: int = 600): from .judge import split_cmd, subprocess_llm if not cmd: @@ -315,7 +315,7 @@ def _make_llm(cmd: str | None, what: str): file=sys.stderr, ) return None - return subprocess_llm(split_cmd(cmd)) + return subprocess_llm(split_cmd(cmd), timeout) def _reference_distribution(args: argparse.Namespace, judge_fn) -> tuple[dict, list, str]: @@ -341,7 +341,7 @@ def cmd_judge(args: argparse.Namespace) -> int: meets_reference_bar, score_distribution, ) - judge_fn = _make_llm(args.llm_cmd, "judge") + judge_fn = _make_llm(args.llm_cmd, "judge", args.llm_timeout) if judge_fn is None: return 2 ours_items = checklist_items_from_01e(_load_json(args.ours), args.id_prefix) @@ -384,10 +384,13 @@ def cmd_improve(args: argparse.Namespace) -> int: load_vulns, ) - judge_fn = _make_llm(args.llm_cmd, "improve") + judge_fn = _make_llm(args.llm_cmd, "improve", args.llm_timeout) if judge_fn is None: return 2 - improve_fn = _make_llm(args.improve_cmd, "improve") if args.improve_cmd else judge_fn + improve_fn = ( + _make_llm(args.improve_cmd, "improve", args.llm_timeout) + if args.improve_cmd else judge_fn + ) doc = _load_json(args.ours) all_props = list(doc.get("properties", [])) @@ -601,6 +604,11 @@ def _add_judge_common_args(sp: argparse.ArgumentParser) -> None: "--retry-wait", type=float, default=5.0, help="seconds between attempts, letting rate-limit blips pass (default 5)", ) + sp.add_argument( + "--llm-timeout", type=int, default=600, + help="per-call adapter timeout in seconds; a hung adapter process is " + "killed and the call retried like any transient failure (default 600)", + ) def _add_recall_data_args(sp: argparse.ArgumentParser) -> None: diff --git a/src/speca_lean4/judge.py b/src/speca_lean4/judge.py index eb11aee..6f26c88 100644 --- a/src/speca_lean4/judge.py +++ b/src/speca_lean4/judge.py @@ -546,10 +546,17 @@ def subprocess_llm(cmd: list[str], timeout: int = 600) -> LLMFn: already authenticated. No API key is read or forwarded here. """ def call(prompt: str) -> str: - proc = subprocess.run( - cmd, input=prompt, capture_output=True, text=True, - encoding="utf-8", timeout=timeout, - ) + try: + proc = subprocess.run( + cmd, input=prompt, capture_output=True, text=True, + encoding="utf-8", timeout=timeout, + ) + except subprocess.TimeoutExpired as exc: + # surface as JudgeError so judge_item's retries cover a hung + # adapter process the same as a non-zero exit + raise JudgeError( + f"llm command {' '.join(cmd)!r} hit the {timeout}s timeout" + ) from exc if proc.returncode != 0: raise JudgeError( f"llm command {' '.join(cmd)!r} failed (rc={proc.returncode}); " diff --git a/tests/test_judge.py b/tests/test_judge.py index 2c69ded..3c05419 100644 --- a/tests/test_judge.py +++ b/tests/test_judge.py @@ -451,6 +451,15 @@ def _mock_cmd() -> str: return f'"{sys.executable}" "{_FIX / "mock_llm.py"}"' +def test_subprocess_llm_timeout_is_a_retryable_judge_error(): + from speca_lean4.judge import subprocess_llm + + fn = subprocess_llm([sys.executable, "-c", "import time; time.sleep(30)"], + timeout=1) + with pytest.raises(JudgeError, match="timeout"): + fn("prompt") + + def test_split_cmd(): parts = split_cmd(_mock_cmd()) assert parts[0] == sys.executable