From 639f6ae9880182a4d10fe8aab3e1bac404783d18 Mon Sep 17 00:00:00 2001 From: greenthree <1395214327@qq.com> Date: Tue, 4 Aug 2026 20:06:04 +0800 Subject: [PATCH] Add aggregate constraint validation --- CHANGELOG.md | 7 + README.md | 4 +- SKILL.md | 9 +- compat/probhub-skill/package.json | 4 +- package-lock.json | 4 +- package.json | 2 +- probhub/__init__.py | 2 +- probhub/reporting.py | 30 ++ probhub/statement_consistency.py | 525 +++++++++++++++++++++-- references/aggregate-limit-derivation.md | 259 +++++++++++ references/verification-modes.md | 7 + references/workspace-schema-v1.md | 2 + scripts/check_release.py | 1 + tests/test_generations.py | 2 +- tests/test_npm_packages.py | 58 ++- tests/test_process_control.py | 8 +- tests/test_report.py | 18 +- tests/test_statement_consistency.py | 261 +++++++++++ 18 files changed, 1158 insertions(+), 45 deletions(-) create mode 100644 references/aggregate-limit-derivation.md diff --git a/CHANGELOG.md b/CHANGELOG.md index 10d18a1..0534de7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,13 @@ ## [Unreleased] +## [0.6.5] - 2026-08-04 + +- Schema v1 题面—Validator 约束对账新增多组数据累计约束检查：保守识别 LaTeX 求和、中文“所有测试用例之和”表述，以及 Validator 中直接 `+=` / `acc = acc + term` 累加和后续 `ensuref` 上限；统一规范化为 `sum:n`、`sum:len:s`、`sum:n+m` 等主体。 +- lint 对累计约束的题面缺失、Validator 缺失和确定数值不一致给出非阻断 warning；动态边界与“检测到多测和单组规模但未发现累计上限”保留结构化人工复核信息，不自动推导正确上限，也不把启发式结果当作证明。 +- `probhub report` 的 JSON、终端和 Markdown 输出新增累计约束状态与 matched / statement-only / Validator-only / dynamic 计数；新能力仅进入 Workspace Schema v1，Legacy 保持冻结兼容。 +- Agent Skill 新增多组数据上限推导契约：`T_max` 在 5 至 100000 间按同文件测试需求、逐组固定成本和 I/O 选择；高测试需求且满足复杂度条件时以 `sum(n_i) <= 10N` 为候选，再用联合最坏数据和三倍 TL 余量校准。题面累计上限未在 Validator 匹配、数值冲突或动态不可核对时阻断封题；即使自动匹配，也要求人工确认累加器宽度、初始化、逐组一次累计和最终拒绝逻辑。 + ## [0.6.3] - 2026-08-02 - Unix 内存限制 helper 改为隔离 Python 的内联 `-c` 启动，保留 `RLIMIT_AS`、状态管道、信号复位、session/process group 与 fail-closed 语义，同时避免 WSL 从 Windows 挂载目录逐次读取 helper 文件的冷启动开销。 diff --git a/README.md b/README.md index 039b3ea..95db042 100644 --- a/README.md +++ b/README.md @@ -25,6 +25,7 @@ ProbHub 会在这条流程中提供： - standard、custom checker、浮点比较和 interactive 四类常见评测场景； - AC、WA、TLE、MLE、OLE、RE、FAIL 等结果和完整进程树清理； - 可复现的数据生成、差分测试、反例重放和错解击杀矩阵； +- 题面与 Validator 的范围对账、多组数据累计总量的静态复核提示，以及按复杂度、测试需求和资源余量推导 `T` 与累计上限的 Agent 指引； - Typst 全卷排版、单题 PDF、DOMjudge ZIP 和交付前验包； - Windows 与 Ubuntu 双平台 CI 验证。 @@ -168,7 +169,8 @@ Agent 和 WebUI 都会调用同一套 Core。只有需要手动排查或编排 |---|---| | `probhub doctor` | 检查安装环境 | | `probhub ui` | 启动 WebUI | -| `probhub lint L01` | 检查目录、配置和题面结构 | +| `probhub lint L01` | 检查目录、配置、题面结构和约束对账 | +| `probhub report L01` | 查看数据画像、错解击杀和累计约束状态 | | `probhub judge L01` | 编译并运行 Validator、标程、暴力和错解 | | `probhub stress L01 --rounds 1000 --seed 12345` | 用随机小数据对拍 | | `probhub seal L01 --no-cache` | 验证并冻结当前题目版本 | diff --git a/SKILL.md b/SKILL.md index 4dd3f2e..eb8a7f3 100644 --- a/SKILL.md +++ b/SKILL.md @@ -158,13 +158,17 @@ probhub build L01 --skip-judge 1. 读取 `.probhub/workspace.yaml`，确认稳定 ID、目录和正式题序。 2. 读取所选题目的 `probhub.yaml`、`problem.md`、`code/` 与 `data/`。 -3. 只修改规范源文件；不要修改生成物来“修复”结果。 +3. 只修改规范源文件；不要修改生成物来“修复”结果。创作、修改或审查含 `T` 的多组数据题时，先读取 `references/aggregate-limit-derivation.md`，在定稿题面和 Validator 前推导并记录 `T_max`、累计规模代理与资源校准结论。 4. 修改后执行： ```powershell probhub lint ``` + 多组数据题还必须读取 `probhub --json lint ` 的 `constraint_reconciliation.aggregate_constraints`。题面声明累计上限时，任何对应的 `statement_only`、`aggregate_constraint_mismatch` 或 `dynamic` 都是 Agent 封题阻断，不能因为 Core 仍返回非阻断 warning 就忽略。直接写法应达到 `state: matched`；若 Validator 使用函数封装、宏或其他静态分析不支持的等价实现，必须人工读代码确认并在验证记录中说明，不能把未识别状态冒充自动通过。 + + 即使结果为 `matched`，也要人工确认 Validator 使用足够宽的累加类型、在多测循环前初始化、对每组目标量恰好累计一次，并在读取全部相关输入后用 `ensuref` 或等价检查限制为题面同一上限。只看到变量名或同一常量不算“确实限制”。发现题面有总量承诺但 Validator 没有实际执行这些步骤时，先修 Validator 并重跑 lint/Judge，再进入 seal。 + 5. 开发代码或数据时执行： ```powershell @@ -202,6 +206,7 @@ probhub build L01 --skip-judge - 现有题面来源不得擅自改意，只修正格式；Idea 题应自行完成约束、算法与简洁题面。 - 输入格式中的数据范围使用中文括号，紧跟变量第一次出现处，例如：`输入一个整数 $T$（$1\le T\le 100$）。` +- 多组数据题除单组范围外，必须按 `references/aggregate-limit-derivation.md` 推导 `T_max` 与累计规模：`T_max` 候选限制在 `5..100000`；测试需求较大、算法至少线性、各组独立且工作量条件成立时，以 `sum(n_i) <= 10*N` 为默认候选，再用联合最坏数据和 `accepted_max_time * 3 <= TL` 校准。若算法复杂度需要累计输入受限，应在题面明确写出总点数、总边数或字符串总长度上界，并在 Validator 中使用足够宽的累加类型逐组累计后校验。题面已有累计上限时，Validator 中的实际累计和拒绝逻辑是封题必查项，不得只依赖 lint 退出码或变量名匹配。 - 题面写法守则： - 任务目标必须在题目描述阶段即可读懂，不得推迟到输入输出格式甚至样例才首次出现；关键定义、对象、操作在就近位置解释。 - 数据范围必须覆盖输入中每个量的完整前提：下界、字符集、互异性、是否保证有解、是否保证成树/连通等；浮点输出题写明误差判定标准，而不是只写"保留若干位小数"。 @@ -217,7 +222,7 @@ probhub build L01 --skip-judge - Checker/Interactor 必须使用附带的 DOMjudge/testlib 协议；交互题按需设置 `judge.interactive.idle_limit` 和 `transcript_limit`。Core 负责本地编译以及生成 `output_validators/validate/`，不得手工维护该生成目录。 - 数据严格放在 `data/sample` 和 `data/secret`，每个 `.in` 必须有同名 `.ans`。 - 样例 `.ans` 必须由配置顺序中的首个 accepted 精确复现；只归一 CRLF/CR 为 LF，尾空格、缺少尾换行和其他字节差异仍失败。Custom Checker 的非唯一输出语义不能替代这条样例不变量；交互题明确不适用。 -- 题面只能有一个 H1，必需 H2 依次为题目描述、输入格式、输出格式且内容非空；提示位于输出之后，样例输入/输出只来自 `data/sample`。lint 的约束对账始终是 `analysis_state: partial` 的人工复核报告，启发式 mismatch 只能 warning，不能作为自动正确性证明。 +- 题面只能有一个 H1，必需 H2 依次为题目描述、输入格式、输出格式且内容非空；提示位于输出之后，样例输入/输出只来自 `data/sample`。lint 的约束对账会保守识别直接 LaTeX/中文累计上限与 Validator 直接累加器，并在多测但未发现累计上限时提示复核；结果始终是 `analysis_state: partial`，启发式 mismatch 只能 warning，不能替代复杂度分析或正确性证明。 - secret 数据优先通过 `data.recipes` 配方生成（`probhub gen`）：生成器 + 精确 args 可复现同一字节，手工数据显式 `manual: true`；没有配方的测试点 lint 会给 warning。配方格式见 `references/workspace-schema-v1.md`。 - 为定向卡错解和复杂度数据配置 `data.groups` 与结构化 `solutions.*[].expected`；实现或审查时读取 `references/data-groups-expectations.md`。要求错解必须 WA 时显式写 `status: WA`，不得用偶然 RE/TLE 代替。 - 慢参考解可在第二及后续 accepted 上配置 `run_on: [groups]`；多个组取并集，sample 始终执行。首个 accepted 禁止缩域；局部 accepted 必须显式写 `expected.groups`，且期望和 target 覆盖不得超出运行域。该字段只影响本地 Judge，不影响 stress 或 DOMjudge 包。 diff --git a/compat/probhub-skill/package.json b/compat/probhub-skill/package.json index e041f85..d25ae42 100644 --- a/compat/probhub-skill/package.json +++ b/compat/probhub-skill/package.json @@ -1,6 +1,6 @@ { "name": "probhub-skill", - "version": "0.6.3", + "version": "0.6.5", "description": "Lightweight ProbHub command package that delegates to the complete probhub package.", "main": "bin/init.js", "bin": { @@ -32,7 +32,7 @@ "node": ">=18" }, "dependencies": { - "probhub": "0.6.3" + "probhub": "0.6.5" }, "files": [ "bin/*.js", diff --git a/package-lock.json b/package-lock.json index d403f41..d4c0042 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "probhub", - "version": "0.6.3", + "version": "0.6.5", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "probhub", - "version": "0.6.3", + "version": "0.6.5", "license": "MIT", "bin": { "probhub": "bin/probhub.js", diff --git a/package.json b/package.json index 8b852ff..9a556ef 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "probhub", - "version": "0.6.3", + "version": "0.6.5", "description": "基于大语言模型 (LLM Agent) 和现代排版框架构建的 ACM/ICPC 自动化出题工作流。", "main": "bin/init.js", "bin": { diff --git a/probhub/__init__.py b/probhub/__init__.py index 9675499..4d0e809 100644 --- a/probhub/__init__.py +++ b/probhub/__init__.py @@ -1,3 +1,3 @@ """ProbHub deterministic contest-problem build core.""" -__version__ = "0.6.3" +__version__ = "0.6.5" diff --git a/probhub/reporting.py b/probhub/reporting.py index 64e99f5..beb7ffd 100644 --- a/probhub/reporting.py +++ b/probhub/reporting.py @@ -492,6 +492,23 @@ def _problem_report(root, workspace, entry, position, lint_result): "ungrouped_secret_cases": ungrouped_secret, "targeted_secret_cases": len(targeted_secret_cases), "recipes": recipes, + "aggregate_constraints": constraint_report.get("aggregate_constraints") or { + "analysis_state": "partial", + "multi_case_detected": False, + "state": "not_detected", + "matched": [], + "statement_only": [], + "validator_only": [], + "dynamic": [], + "statement_constraints": [], + "validator_constraints": [], + "summary": { + "matched": 0, + "statement_only": 0, + "validator_only": 0, + "dynamic": 0, + }, + }, "calibration": _calibration_profile(calibration), "solution_verification": (lint_result or {}).get("solution_verification") or {}, "kill_matrix": _kill_matrix(config, groups, cases, calibration), @@ -619,6 +636,11 @@ def render_markdown_report(report): f"targeted {recipes['targeted']}/{recipes['total']}；near-boundary {recipes['near_boundary']}/{recipes['total']}", f"- 校准：{problem['calibration']['state']}；primary accepted TL 余量 " f"{_format_headroom(problem['calibration']['primary_headroom'])}；`target_guarantee: false`", + f"- 累计约束：{problem['aggregate_constraints']['state']}；" + f"matched {problem['aggregate_constraints']['summary']['matched']}；" + f"statement-only {problem['aggregate_constraints']['summary']['statement_only']}；" + f"Validator-only {problem['aggregate_constraints']['summary']['validator_only']}；" + f"dynamic {problem['aggregate_constraints']['summary']['dynamic']}", "", ]) if problem["groups"]: @@ -692,6 +714,14 @@ def render_text_report(report): f"near-boundary={recipes['near_boundary']}/{recipes['total']} " f"analysis={recipes['analysis_state']}" ) + aggregate = problem["aggregate_constraints"] + lines.append( + f" 累计约束: {aggregate['state']} " + f"matched={aggregate['summary']['matched']} " + f"statement-only={aggregate['summary']['statement_only']} " + f"validator-only={aggregate['summary']['validator_only']} " + f"dynamic={aggregate['summary']['dynamic']}" + ) if problem["groups"]: lines.append(" 数据组:") for group in problem["groups"]: diff --git a/probhub/statement_consistency.py b/probhub/statement_consistency.py index 516c691..80286fb 100644 --- a/probhub/statement_consistency.py +++ b/probhub/statement_consistency.py @@ -33,6 +33,13 @@ _CPP_RAW_STRING_OPEN = re.compile( r'(?:u8|u|U|L)?R"(?P[^ ()\\\t\r\n]{0,16})\(' ) +_AGGREGATE_PREFIX = "sum:" +_CHINESE_AGGREGATE = re.compile( + r"(?:所有|全部)(?:测试用例|测试数据|测试组|组数据)(?:中|内|中的|内的|的)?\s*" + r"(?P.+?)\s*(?:之和|总和)\s*" + r"(?P不超过|至多|不大于|小于等于|不小于|至少|大于等于)\s*" + r"(?P[^，。；;]+)" +) def _decimal_text(value): @@ -141,6 +148,69 @@ def _canonical_subject(raw): return "" +def _strip_testcase_index(raw): + value = re.sub( + r"(?P[A-Za-z][A-Za-z0-9]*)\s*_\s*\{\s*i\s*\}", + r"\g", + raw, + ) + return re.sub( + r"(?P[A-Za-z][A-Za-z0-9]*)\s*_\s*i\b", + r"\g", + value, + ) + + +def _split_direct_sum(raw): + value = _strip_balanced_outer_parentheses(raw.strip()) + depth = 0 + start = 0 + parts = [] + for index, character in enumerate(value): + if character in "({[": + depth += 1 + elif character in ")}]": + depth -= 1 + if depth < 0: + return [] + elif character == "+" and depth == 0: + parts.append(value[start:index].strip()) + start = index + 1 + if depth != 0: + return [] + parts.append(value[start:].strip()) + return parts if all(parts) else [] + + +def _canonical_aggregate_term(raw): + value = raw.strip().strip("$` ") + value = value.replace("\\left", "").replace("\\right", "") + value = re.sub(r"\\(?:big|Big|bigg|Bigg)[lrm]?", "", value) + value = value.replace("\\,", "").strip() + value = _strip_testcase_index(value) + length_words = re.fullmatch( + r"(?:字符串\s*)?\$?\s*([A-Za-z][A-Za-z0-9_]*)\s*\$?\s*的长度", + value, + ) + if length_words: + return f"len:{length_words.group(1).casefold()}" + return _canonical_subject(value) + + +def _canonical_aggregate_subject(raw): + value = raw.strip().strip("$` ") + value = re.sub(r"^(?:的|每组的?)\s*", "", value) + value = re.sub(r"\s*的\s*$", "", value) + value = re.sub(r"\s*(?:、|，|,|与|和)\s*", "+", value) + parts = _split_direct_sum(value) + canonical = [_canonical_aggregate_term(part) for part in parts] + if not canonical or any( + not item or item.startswith(_AGGREGATE_PREFIX) for item in canonical + ): + return "" + return _AGGREGATE_PREFIX + "+".join(canonical) + + def _statement_subjects(raw): value = raw.strip() pieces = re.split(r"\s*[,，]\s*", value) @@ -223,6 +293,7 @@ def _constraint_item( "direct": boundary["type"] == "number", "kind": kind, "origin": origin, + "aggregate": subject_normalized.startswith(_AGGREGATE_PREFIX), "path": str(path), "line": int(line), "raw": raw.strip(), @@ -278,7 +349,11 @@ def _constraints_for_relation( normalized_operator = _operator_for_subject(operator, subject_on_left) return [ _constraint_item( - source="statement" if origin == "input_format" else "validator", + source=( + "statement" + if origin in {"input_format", "input_aggregate"} + else "validator" + ), subject=subject, subject_normalized=canonical, operator=normalized_operator, @@ -362,6 +437,81 @@ def _inline_math_expressions(line): return [line] if re.search(r"(?:<=|>=|<|>|≤|≥|\\le|\\ge)", line) else [] +def _aggregate_statement_constraint( + subject_raw, + operator, + boundary_raw, + *, + path, + line, + raw, +): + subject = _canonical_aggregate_subject(subject_raw) + if not subject: + return None + boundary_text = boundary_raw.strip().strip("$` ").strip("，。；;:") + boundary = _parse_statement_operand(boundary_text) + if boundary["type"] == "unknown": + boundary = {"type": "dynamic", "raw": boundary_text} + return _constraint_item( + source="statement", + subject=subject_raw.strip(), + subject_normalized=subject, + operator=operator, + boundary=boundary, + path=path, + line=line, + raw=raw, + kind="integer", + origin="input_aggregate", + ) + + +def _extract_statement_aggregates(line, *, path, line_number): + constraints = [] + for expression in _inline_math_expressions(line): + normalized = _normalize_statement_expression(expression) + match = re.fullmatch( + r"\\sum\s*_\s*\{[^{}]*\}\s*" + r"\^\s*(?:\{\s*[Tt]\s*\}|[Tt])\s*(?P.+?)\s*" + r"(?P<=|>=|<|>)\s*(?P.+)", + normalized, + ) + if match: + item = _aggregate_statement_constraint( + match.group("term"), + match.group("operator"), + match.group("boundary"), + path=path, + line=line_number, + raw=line, + ) + if item: + constraints.append(item) + + relation_operators = { + "不超过": "<=", + "至多": "<=", + "不大于": "<=", + "小于等于": "<=", + "不小于": ">=", + "至少": ">=", + "大于等于": ">=", + } + for match in _CHINESE_AGGREGATE.finditer(line): + item = _aggregate_statement_constraint( + match.group("term"), + relation_operators[match.group("relation")], + match.group("boundary"), + path=path, + line=line_number, + raw=line, + ) + if item: + constraints.append(item) + return constraints + + def extract_statement_constraints(parsed, path): input_sections = [ item for item in parsed.get("section_occurrences", []) if item.get("key") == "input" @@ -384,6 +534,9 @@ def extract_statement_constraints(parsed, path): origin="input_format", operand_parser=_parse_statement_operand, )) + constraints.extend( + _extract_statement_aggregates(line, path=path, line_number=line_number) + ) return _deduplicate_constraints(constraints) @@ -483,6 +636,25 @@ def blank(start, end): return "".join(output) +def _mask_cpp_preprocessor(text): + """Blank preprocessor directives while preserving offsets and line breaks.""" + + output = [] + continued = False + for line in text.splitlines(keepends=True): + directive = continued or line.lstrip().startswith("#") + if directive: + output.append("".join( + character if character in {"\n", "\r"} else " " + for character in line + )) + continued = line.rstrip("\r\n").rstrip().endswith("\\") + else: + output.append(line) + continued = False + return "".join(output) + + def _call_arguments(text, open_parenthesis): arguments = [] current_start = open_parenthesis + 1 @@ -583,16 +755,99 @@ def _raw_source(text, start, end): return text[start:end + 1].strip() -def extract_validator_constraints(text, path, diagnostics=None): +def _validator_aggregate_subject(raw, aliases): + parts = _split_direct_sum(_strip_cpp_casts(raw.strip())) + terms = [] + kinds = [] + for part in parts: + subjects = _validator_subject(part, aliases) + if len(subjects) != 1: + return None + _display, canonical, kind = subjects[0] + if canonical.startswith(_AGGREGATE_PREFIX): + return None + terms.append(canonical) + kinds.append(kind) + if not terms: + return None + return { + "canonical": _AGGREGATE_PREFIX + "+".join(terms), + "kind": "integer" if all(kind == "integer" for kind in kinds) else "unknown", + } + + +def _register_validator_accumulators(stripped, aliases): + scan_text = _mask_cpp_strings(stripped) + assignments = [] + patterns = ( + re.compile(r"\b(?P[A-Za-z_]\w*)\s*\+=\s*(?P[^;]+);"), + re.compile( + r"\b(?P[A-Za-z_]\w*)\s*=\s*(?P=acc)\s*\+\s*(?P[^;]+);" + ), + ) + for pattern in patterns: + assignments.extend(pattern.finditer(scan_text)) + assignments.sort(key=lambda item: item.start()) + + accumulator_terms = {} + for match in assignments: + aggregate = _validator_aggregate_subject(match.group("term"), aliases) + if not aggregate: + continue + accumulator = match.group("acc").casefold() + terms = accumulator_terms.setdefault(accumulator, []) + for term in aggregate["canonical"][len(_AGGREGATE_PREFIX):].split("+"): + if term not in terms: + terms.append(term) + aliases[accumulator] = { + "subject": f"sum({'+'.join(terms)})", + "canonical": _AGGREGATE_PREFIX + "+".join(terms), + "kind": aggregate["kind"], + } + + +def _validator_testcase_variables(stripped): + variables = set() + for match, _method, arguments, _end in _iter_named_calls( + stripped, _READ_CALLS, receiver="inf" + ): + assigned = _assigned_variable(stripped, match.start()) + label = _cpp_string_literal(arguments[2]) if len(arguments) >= 3 else None + canonical = _canonical_subject(label or assigned or "") + if assigned and canonical in {"t", "tests", "testcases", "test_count"}: + variables.add(assigned) + return variables + + +def _validator_has_multicase_loop(stripped): + scan_text = _mask_cpp_strings(_mask_cpp_preprocessor(stripped)) + return any( + re.search( + rf"(?:for\s*\([^;]*;[^;]*(?:<|<=)\s*{re.escape(variable)}\b|" + rf"while\s*\(\s*{re.escape(variable)}\s*--\s*\))", + scan_text, + ) + for variable in _validator_testcase_variables(stripped) + ) + + +def extract_validator_constraints( + text, + path, + diagnostics=None, + *, + aggregate_context=False, +): diagnostics = diagnostics if diagnostics is not None else [] stripped = _strip_cpp_comments(text) + analysis_text = _mask_cpp_preprocessor(stripped) aliases = {} constraints = [] - read_calls = list(_iter_named_calls(stripped, _READ_CALLS, receiver="inf")) + read_calls = list(_iter_named_calls(analysis_text, _READ_CALLS, receiver="inf")) for match, method, arguments, end in read_calls: if len(arguments) < 2: continue - assigned = _assigned_variable(stripped, match.start()) + assigned = _assigned_variable(analysis_text, match.start()) label = _cpp_string_literal(arguments[2]) if len(arguments) >= 3 else None subject = label or assigned if not subject: @@ -601,7 +856,7 @@ def extract_validator_constraints(text, path, diagnostics=None): if not canonical: continue kind = _READ_CALLS[method] - line = stripped.count("\n", 0, match.start()) + 1 + line = analysis_text.count("\n", 0, match.start()) + 1 raw = _raw_source(text, match.start(), end) if assigned: aliases[assigned.casefold()] = { @@ -641,7 +896,10 @@ def extract_validator_constraints(text, path, diagnostics=None): item["bound"] = bound constraints.append(item) - for match, _method, arguments, end in _iter_named_calls(stripped, {"ensuref"}): + if aggregate_context or _validator_has_multicase_loop(stripped): + _register_validator_accumulators(analysis_text, aliases) + + for match, _method, arguments, end in _iter_named_calls(analysis_text, {"ensuref"}): if not arguments: continue condition = re.sub( @@ -650,7 +908,7 @@ def extract_validator_constraints(text, path, diagnostics=None): r"\1", arguments[0], ) - line = stripped.count("\n", 0, match.start()) + 1 + line = analysis_text.count("\n", 0, match.start()) + 1 raw = _raw_source(text, match.start(), end) if "||" in condition: diagnostics.append({ @@ -804,13 +1062,30 @@ def _unmatched_copy(item, reason): return {**item, "reconciliation": reason} -def reconcile_constraints(statement_constraints, validator_constraints): +def _constraint_group_subject(subject): + if not subject.startswith(_AGGREGATE_PREFIX): + return subject + terms = subject[len(_AGGREGATE_PREFIX):].split("+") + return _AGGREGATE_PREFIX + "+".join(sorted(terms)) + + +def reconcile_constraints( + statement_constraints, + validator_constraints, + *, + multi_case_detected=False, + aggregate_review_candidate=False, +): statement_groups = defaultdict(list) validator_groups = defaultdict(list) for item in statement_constraints: - statement_groups[(item["subject_normalized"], item["bound"])].append(item) + statement_groups[ + (_constraint_group_subject(item["subject_normalized"]), item["bound"]) + ].append(item) for item in validator_constraints: - validator_groups[(item["subject_normalized"], item["bound"])].append(item) + validator_groups[ + (_constraint_group_subject(item["subject_normalized"]), item["bound"]) + ].append(item) matched = [] statement_only = [] @@ -840,7 +1115,7 @@ def reconcile_constraints(statement_constraints, validator_constraints): validator_item = validator_items[match_index] matched.append({ "subject": statement_item["subject"], - "subject_normalized": key[0], + "subject_normalized": statement_item["subject_normalized"], "bound": key[1], "confidence": "high" if not statement_item["dynamic"] else "medium", "dynamic": statement_item["dynamic"] or validator_item["dynamic"], @@ -867,18 +1142,35 @@ def reconcile_constraints(statement_constraints, validator_constraints): statement_item = remaining_statement[0] validator_item = remaining_validator[0] high_confidence_mismatches += 1 + aggregate = key[0].startswith(_AGGREGATE_PREFIX) + diagnostic_subject = statement_item["subject_normalized"] diagnostics.append({ - "code": "constraint_mismatch", + "code": ( + "aggregate_constraint_mismatch" + if aggregate + else "constraint_mismatch" + ), "severity": "warning", "message": ( - f"statement/Validator constraint mismatch for {key[0]} {key[1]}: " + f"statement/Validator {'aggregate ' if aggregate else ''}constraint " + f"mismatch for {diagnostic_subject} {key[1]}: " f"{statement_item['normalized']} vs {validator_item['normalized']}" ), - "subject": key[0], + "subject": diagnostic_subject, "bound": key[1], "confidence": "high", "statement": statement_item, "validator": validator_item, + **( + {"statement_limit": statement_item["value"]} + if aggregate and statement_item.get("direct") + else {} + ), + **( + {"validator_limit": validator_item["value"]} + if aggregate and validator_item.get("direct") + else {} + ), }) statement_only.append(_unmatched_copy(statement_item, "numeric_mismatch")) validator_only.append(_unmatched_copy(validator_item, "numeric_mismatch")) @@ -897,38 +1189,83 @@ def reconcile_constraints(statement_constraints, validator_constraints): for item in statement_only: if item["reconciliation"] == "numeric_mismatch": continue + aggregate = item["subject_normalized"].startswith(_AGGREGATE_PREFIX) diagnostics.append({ - "code": "constraint_statement_only", - "severity": "info", - "message": f"statement-only constraint: {item['normalized']}", + "code": ( + "aggregate_constraint_statement_only" + if aggregate + else "constraint_statement_only" + ), + "severity": "warning" if aggregate else "info", + "message": ( + f"statement-only {'aggregate ' if aggregate else ''}constraint: " + f"{item['normalized']}" + ), "subject": item["subject_normalized"], "bound": item["bound"], "evidence": item, + **( + {"statement_limit": item["value"]} + if aggregate and item.get("direct") + else {} + ), }) for item in validator_only: if item["reconciliation"] == "numeric_mismatch": continue + aggregate = item["subject_normalized"].startswith(_AGGREGATE_PREFIX) diagnostics.append({ - "code": "constraint_validator_only", - "severity": "info", - "message": f"Validator-only constraint: {item['normalized']}", + "code": ( + "aggregate_constraint_validator_only" + if aggregate + else "constraint_validator_only" + ), + "severity": "warning" if aggregate else "info", + "message": ( + f"Validator-only {'aggregate ' if aggregate else ''}constraint: " + f"{item['normalized']}" + ), "subject": item["subject_normalized"], "bound": item["bound"], "evidence": item, + **( + {"validator_limit": item["value"]} + if aggregate and item.get("direct") + else {} + ), }) - dynamic_count = sum( - item["dynamic"] for item in [*statement_constraints, *validator_constraints] + all_constraints = [*statement_constraints, *validator_constraints] + aggregate_dynamic = [ + item + for item in all_constraints + if item["dynamic"] and item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + nonaggregate_dynamic_count = sum( + item["dynamic"] + for item in all_constraints + if not item["subject_normalized"].startswith(_AGGREGATE_PREFIX) ) - if dynamic_count: + dynamic_count = len(aggregate_dynamic) + nonaggregate_dynamic_count + if nonaggregate_dynamic_count: diagnostics.append({ "code": "constraint_dynamic_bounds", "severity": "info", "message": ( - f"{dynamic_count} dynamic bound(s) were retained as partial evidence; " + f"{nonaggregate_dynamic_count} dynamic bound(s) were retained as partial evidence; " "no semantic mismatch warning is inferred from them" ), }) + if aggregate_dynamic: + diagnostics.append({ + "code": "aggregate_constraint_dynamic", + "severity": "info", + "message": ( + f"{len(aggregate_dynamic)} dynamic aggregate bound(s) were retained " + "for manual review" + ), + "evidence": aggregate_dynamic, + }) if matched and not statement_only and not validator_only and not dynamic_count: confidence = "high" elif matched: @@ -945,8 +1282,56 @@ def reconcile_constraints(statement_constraints, validator_constraints): "manual review is still required" ), }) + aggregate_statement = [ + item + for item in statement_constraints + if item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + aggregate_validator = [ + item + for item in validator_constraints + if item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + aggregate_matched = [ + item + for item in matched + if item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + aggregate_statement_only = [ + item + for item in statement_only + if item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + aggregate_validator_only = [ + item + for item in validator_only + if item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + ] + aggregate_evidence = bool(aggregate_statement or aggregate_validator) + if aggregate_evidence and not ( + aggregate_statement_only or aggregate_validator_only or aggregate_dynamic + ): + aggregate_state = "matched" + elif aggregate_evidence or (multi_case_detected and aggregate_review_candidate): + aggregate_state = "requires_review" + else: + aggregate_state = "not_detected" + if not aggregate_evidence and multi_case_detected and aggregate_review_candidate: + diagnostics.append({ + "code": "aggregate_constraint_review_required", + "severity": "info", + "message": ( + "multiple test cases and per-case scale variables were detected, but no " + "direct aggregate constraint was found; manually review T times the " + "per-case bound and the intended total input budget" + ), + }) requires_review = bool( - statement_only or validator_only or dynamic_count or no_evidence + statement_only + or validator_only + or dynamic_count + or no_evidence + or aggregate_state == "requires_review" ) return { "analysis_state": "partial", @@ -963,6 +1348,27 @@ def reconcile_constraints(statement_constraints, validator_constraints): "diagnostics": diagnostics, "statement_constraints": list(statement_constraints), "validator_constraints": list(validator_constraints), + "aggregate_constraints": { + "analysis_state": "partial", + "scope": ( + "Direct statement sums and direct C++ accumulator assignments only; " + "this does not infer a correct total limit or prove loop semantics." + ), + "multi_case_detected": bool(multi_case_detected), + "state": aggregate_state, + "matched": aggregate_matched, + "statement_only": aggregate_statement_only, + "validator_only": aggregate_validator_only, + "dynamic": aggregate_dynamic, + "statement_constraints": aggregate_statement, + "validator_constraints": aggregate_validator, + "summary": { + "matched": len(aggregate_matched), + "statement_only": len(aggregate_statement_only), + "validator_only": len(aggregate_validator_only), + "dynamic": len(aggregate_dynamic), + }, + }, "summary": { "matched": len(matched), "statement_only": len(statement_only), @@ -973,15 +1379,82 @@ def reconcile_constraints(statement_constraints, validator_constraints): } +def _input_section_text(parsed): + sections = [ + item for item in parsed.get("section_occurrences", []) if item.get("key") == "input" + ] + if not sections: + return "" + section = sections[0] + return "\n".join( + line + for line_number, line in iter_unfenced_lines(parsed["raw"]) + if section["start_line"] <= line_number <= section["end_line"] + ) + + +def _aggregate_review_context( + parsed, + statement_constraints, + validator_text, + validator_constraints, +): + aggregate_evidence = any( + item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + for item in [*statement_constraints, *validator_constraints] + ) + input_text = _input_section_text(parsed) + statement_mentions_cases = bool(re.search( + r"(?:测试用例|测试数据|测试组|组数据|test\s+cases?)", + input_text, + re.IGNORECASE, + )) + statement_mentions_count = bool(re.search( + r"(?:\$\s*[Tt]\s*\$|\b(?:test_count|testcases|tests|[Tt])\b)", + input_text, + )) + + stripped = _strip_cpp_comments(validator_text) + validator_mentions_loop = _validator_has_multicase_loop(stripped) + multi_case_detected = bool( + aggregate_evidence + or (statement_mentions_cases and statement_mentions_count) + or validator_mentions_loop + ) + control_subjects = {"t", "tests", "testcases", "test_count"} + aggregate_review_candidate = any( + not item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + and item["subject_normalized"] not in control_subjects + for item in [*statement_constraints, *validator_constraints] + ) + return multi_case_detected, aggregate_review_candidate + + def analyze_constraint_consistency(parsed, statement_path, validator_text, validator_path): statement_constraints = extract_statement_constraints(parsed, statement_path) extraction_diagnostics = [] + statement_has_aggregate = any( + item["subject_normalized"].startswith(_AGGREGATE_PREFIX) + for item in statement_constraints + ) validator_constraints = extract_validator_constraints( validator_text, validator_path, diagnostics=extraction_diagnostics, + aggregate_context=statement_has_aggregate, + ) + multi_case_detected, aggregate_review_candidate = _aggregate_review_context( + parsed, + statement_constraints, + validator_text, + validator_constraints, + ) + result = reconcile_constraints( + statement_constraints, + validator_constraints, + multi_case_detected=multi_case_detected, + aggregate_review_candidate=aggregate_review_candidate, ) - result = reconcile_constraints(statement_constraints, validator_constraints) result["diagnostics"] = [*extraction_diagnostics, *result["diagnostics"]] if extraction_diagnostics: result["requires_review"] = True diff --git a/references/aggregate-limit-derivation.md b/references/aggregate-limit-derivation.md new file mode 100644 index 0000000..2e61aa7 --- /dev/null +++ b/references/aggregate-limit-derivation.md @@ -0,0 +1,259 @@ +# 多组数据上限推导 + +本文定义 Agent 为多组数据题推导 `T_max` 与累计规模上限的执行契约。它用于创作新题、修改复杂度或限制、补强正式数据和封题审查。 + +本文不是 Core Schema。不要向 `probhub.yaml` 虚构复杂度或推导字段，不要声称 lint 能证明算法复杂度，也不要让 Core 自动改写题面或 Validator。Core 的累计约束对账只提供保守的静态证据，最终上限仍由 Agent 的证明、数据需求和资源校准共同决定。 + +## 目录 + +1. [术语与目标](#1-术语与目标) +2. [推导前必须冻结的事实](#2-推导前必须冻结的事实) +3. [`T_max` 推导](#3-t_max-推导) +4. [累计规模与 `10N` 规则](#4-累计规模与-10n-规则) +5. [多参数与特殊复杂度](#5-多参数与特殊复杂度) +6. [联合边界数据与资源校准](#6-联合边界数据与资源校准) +7. [题面和 Validator 落地](#7-题面和-validator-落地) +8. [验证记录与完成条件](#8-验证记录与完成条件) + +## 1. 术语与目标 + +- `T`：一个输入文件内的实际测试组数。 +- `T_max`：题面允许的 `T` 上界。通常写成 `1 <= T <= T_max`。 +- `N`：主规模变量的单组上界，例如 `n_i <= N`。 +- `K`：累计规模相对于一个最大规模用例的倍率。 +- `C(n)`：intended accepted 处理一组规模 `n` 的工作量模型。 +- `F`：每组不随主规模变化的固定成本，如清空固定大表、容器构造和输出一行。 +- `large_case_equivalents`：计划在同一输入中共存的用例规模之和除以 `N`。 + +累计约束只控制一次程序运行，也就是一个 `.in` 文件。DOMjudge 的不同测试文件分别启动和计时；不要把其他文件的测试组数量或规模累加到本文件的需求中。 + +正确上限必须同时满足： + +1. 能容纳题目语义和数据设计需要在同一输入中出现的测试组合。 +2. 能在题面中清楚声明，并由 Validator 精确执行。 +3. intended accepted、Validator 和特殊 Judge 在最坏合法输入上保留规定的时间、内存和输出余量。 + +复杂度只能产生候选上限。没有达到候选联合边界的实测，不得把推导记录为 `accepted`。 + +## 2. 推导前必须冻结的事实 + +先阅读公开题面、`probhub.yaml`、primary accepted、Validator、数据组和资源限制，并记录： + +1. 每个单组规模变量的合法范围，如 `n <= N`、`m <= M`、字符串长度 `len <= L`。 +2. intended accepted 的时间和空间复杂度证明；再对照实际源码检查循环、排序、图遍历、预处理和清空逻辑。 +3. 各组是否独立处理。若实现把全部组收集后统一排序、离线处理或共享增长状态，应按整体算法重新建模。 +4. 每组固定成本 `F`，特别检查 `memset(O(U))`、重建大表、初始化大容器、固定输出和协议交互。 +5. 需要在同一输入中共存的边界、定向、随机和近上界行为类型，以及各自所需规模。 +6. TL、ML、OL 和校准平台。只在本机校准时继续声明 `target_guarantee: false`。 + +无法从证明和源码得到一致的复杂度模型时，停止自动推导，记录 `decision: needs_review`。不能根据变量名、循环数量或自然语言 Big-O 猜一个上限后继续 seal。 + +## 3. `T_max` 推导 + +### 3.1 候选范围 + +对于使用 `T` 的多组数据题，默认实际范围是： + +```text +1 <= T <= T_max +5 <= T_max <= 100000 +``` + +`T_max` 至少为 5，不表示每份输入必须满足 `T >= 5`。题目语义明确要求其他 `T` 下界时才改动左端点。 + +先计算 `T_need`：一个合法输入中计划同时容纳的独立测试组数量，并取 `max(5, T_need)`。常用候选如下；可以选择范围内其他整数，但必须说明理由。 + +| `T_max` | 典型用途 | +|---:|---| +| 5、10 | 单组很重，主要容纳少量近上界结构 | +| 20、50、100 | 普通多测，兼顾边界、定向和若干大用例 | +| 1000、10000 | 需要大量小用例覆盖状态、数值或短串分类 | +| 100000 | 单组极轻、输入短、确实需要高批量，且 I/O 与固定成本已实测 | + +选择不小于 `T_need` 的最小合理候选。不要因为允许的最大值是 `100000` 就默认使用它。若 `T_need > 100000`，拆分正式测试文件或重新设计输入，不继续放大题面上限。 + +### 3.2 必须计入的成本 + +至少审核： + +```text +total_work = sum(per_case_work_i) + T * F + input_io + output_io +``` + +- 用 `T=T_max` 的最小合法组验证 `T_max * F`、解析和输出成本。 +- 检查最小合法组在 `T=T_max` 时的总输入、总输出是否仍有界。 +- 检查累计主规模打满后，能否继续用最小组补到 `T=T_max`；若可以，这通常是固定成本和主工作量同时最大的候选。 +- Validator、Checker 和 Interactor 也要按 `T_max` 计入逐组成本，不能只测 accepted。 + +候选不满足资源余量时，降低 `T_max`、降低累计规模、优化实现或调整单组上界。提高 TL 是最后选择，且会使原有 TLE 错解证据失效。 + +## 4. 累计规模与 `10N` 规则 + +### 4.1 单主规模 + +设每组 `n_i <= N`，各组由 intended accepted 独立处理，并且 `C(n)/n` 在合法范围内单调不减。若声明： + +```text +sum(n_i) <= K * N +``` + +则： + +```text +sum(C(n_i)) <= C(N) / N * sum(n_i) <= K * C(N) +``` + +所以 `sum(n_i) <= 10 * N` 表示一次运行最多约十个最大规模用例的算法工作量。该结论适用于常见的 `O(n)`、`O(n log n)`、`O(n^2)` 等每组独立算法，但必须验证 `C(n)/n` 条件与固定成本；不能只看到“`O(n)` 及以上”字样就机械使用 `10N`。 + +### 4.2 选择 `K` + +列出计划在同一输入中共存的主要用例及相对规模，计算： + +```text +large_case_equivalents = sum(n_j / N) +``` + +再选择候选： + +| 同文件测试需求 | 候选 `K` | +|---|---:| +| 一个极限主体，其他均为小边界 | 1 或 3 | +| 普通的大中小与定向组合 | 5 | +| 至少约 6 个独立近上界行为，或等价规模超过 `5N` | 10 | + +大量最小用例主要影响 `T_max` 和 `T * F`，不能仅凭原始组数把 `K` 提升到 10。 + +当测试需求较大、算法至少线性、每组独立且工作量条件成立时，默认候选使用： + +```text +sum(n_i) <= 10 * N +``` + +超过 `10N` 不自动批准。优先把不同近上界行为放入不同正式测试文件；只有题目语义要求它们在一次运行中共存，并且新的联合边界校准通过时，才人工评估更大倍率。 + +最后检查 `T_max` 与累计约束能否共同成立。若每组 `n_i >= n_min`，应满足： + +```text +T_max * n_min <= K * N +``` + +否则题面虽然写了 `T <= T_max`，实际不存在 `T=T_max` 的合法输入。若 `K > T_max`，则 `sum(n_i) <= K*N` 在单组上界下可能完全冗余；应降低 `K`，或明确说明还有其他规模变量使该限制仍有作用。需要约 `K` 个最大规模用例时，也要保证 `T_max >= K`。 + +## 5. 多参数与特殊复杂度 + +选择能控制真实工作量的可加代理，而不是强制所有题都写 `sum n`。 + +| 题目或复杂度 | 推荐限制与检查 | +|---|---| +| 数组、序列、字符串，`O(n)` 及以上 | `sum(n_i) <= K * N` | +| 图，`O(n+m)` | 分别限制 `sum(n_i) <= K*N`、`sum(m_i) <= K*M` | +| `O(nm)`，且 `n <= N`、`m <= M` | 分别限制两维累计量，并验证 `sum(n_i*m_i) <= K*N*M` 的工作量界 | +| 每组包含多个字符串或容器 | 限制所有元素或字符串的总长度 | +| 查询复杂度依赖 `n+q` | 分别限制总 `n`、总 `q`，或使用清楚的总 `n+q` 代理 | +| 每组有 `O(U)` 固定清空或预处理 | 除累计主规模外，用 `T_max` 显式控制 `T*U` | +| `O(1)`/`O(log n)` 且 `n` 只是数值 | 主要限制 `T`、输入字节和输出量，不使用无意义的 `sum n` | +| 各组不独立或代理不满足单调条件 | 显式定义 `W(case)`，人工审核 `sum W(case_i)` 或整体复杂度 | + +例如在 `O(nm)` 中，若 `m_i <= M` 且 `sum(n_i) <= K*N`，已有： + +```text +sum(n_i*m_i) <= M * sum(n_i) <= K*N*M +``` + +分别限制两维仍更容易表达输入容量和排除畸形分布。若复杂度还依赖权值范围、字符集、位数或状态空间，把对应参数加入模型，不能隐藏在 `n` 中。 + +## 6. 联合边界数据与资源校准 + +为最终候选 `(T_max, K)` 增加正式、可复现的数据组，至少覆盖： + +1. 累计量恰好等于上限，Validator 接受。 +2. 累计量超过上限 1，Validator 拒绝。该负例可作为 Validator fixture，不必进入正式 secret。 +3. `K` 个最大规模且结构最坏的用例，不能只把随机数据放大。 +4. `T=T_max` 个最小合法用例，覆盖固定成本、I/O 和输出量。 +5. 累计规模打满后用最小组补到 `T=T_max` 的真实可行联合边界。 +6. 大小混合用例，以及能暴露 32 位累加溢出的组合。 + +把最坏合法输入放入专用数据组，例如 `aggregate_max`，然后运行无缓存 Judge。候选默认必须满足： + +```text +accepted_max_time * 3 <= TL +``` + +同时确认： + +- accepted 的内存和输出不越界； +- Validator 与适用的 Checker/Interactor 有明确余量； +- 预期 WA/TLE/MLE/OLE 的目标宿命仍稳定成立； +- 本地校准仍标记 `target_guarantee: false`，正式 TL 在目标 Linux/DOMjudge 复核。 + +失败时按顺序处理：优化 accepted 或 Validator；降低 `T_max`；把 `K` 从 10 降为 5/3；调整单组上界；最后才评估提高 TL。任何限制、代码或数据变化后，重跑受影响的 Judge、stress 和 seal。 + +## 7. 题面和 Validator 落地 + +题面应同时声明单组范围、`T_max` 和每个必要累计上限。避免只写“数据总量不超过限制”而不给出变量与数值。 + +Validator 必须： + +1. 用足够宽的类型保存累计量，通常为 64 位整数。 +2. 在多测循环前初始化累加器。 +3. 每组对目标量恰好累计一次。 +4. 在读取相关字段后执行上限检查。 +5. 用 `ensuref` 或等价逻辑保证等于上限时接受、超过上限时拒绝。 +6. 对多个累计量分别检查，不能用一个弱代理替代题面中的全部承诺。 + +运行： + +```powershell +probhub --json lint +``` + +读取 `constraint_reconciliation.aggregate_constraints`。直接写法应达到 `state: matched`。对应约束出现 `statement_only`、`aggregate_constraint_mismatch` 或 `dynamic` 时阻断 seal；函数封装、宏或复杂等价实现未被静态分析识别时，人工读 Validator 并记录证据，不能伪称自动匹配。 + +`matched` 只证明静态形状和值能对账，不证明推导出的上限合理，也不证明累加器控制流正确。仍要完成本节的人工检查和第 6 节的边界执行。 + +## 8. 验证记录与完成条件 + +在任务验证记录中保存，不写入 `probhub.yaml`： + +```yaml +aggregate_limit_derivation: + test_count: + lower_bound: 1 + proposed_max: 100000 + test_need: 24000 + fixed_cost_reviewed: true + jointly_reachable: true + measures: + - name: n + per_case_max: 200000 + intended_complexity: O(n log n) + independent_cases: true + demand_class: extensive + large_case_equivalents: 7.4 + multiplier: 10 + proposed_sum_limit: 2000000 + calibration: + group: aggregate_max + aggregate_max_time: 0.54 + time_limit: 2.0 + headroom_passed: true + target_guarantee: false + validator_reconciliation: matched + decision: accepted +``` + +`decision` 只允许： + +- `accepted`：复杂度、测试需求、联合边界校准和 Validator 执行全部通过。 +- `needs_revision`：候选资源超限、测试容量不足或题面/Validator 不一致，需要修改。 +- `needs_review`：无法证明工作量代理、各组不独立或静态分析无法覆盖且人工审查未完成。 + +进入 seal 前确认： + +- `5 <= T_max <= 100000`，且实际 `T` 下界没有被误写； +- `T_need`、`T*F`、输入和输出预算已有依据； +- `T_max` 与所有累计约束存在可达到的联合边界，没有不可行或完全冗余的限制； +- `K=10` 只在高测试需求、适用复杂度和校准通过时使用； +- 等于上限接受、超过上限拒绝、`T_max` 最小组和联合最坏组均已执行； +- `constraint_reconciliation.aggregate_constraints` 已审阅； +- 验证记录为 `decision: accepted`，无未解决的校准 warning 或人工复核项。 diff --git a/references/verification-modes.md b/references/verification-modes.md index 4ff58dd..5586be3 100644 --- a/references/verification-modes.md +++ b/references/verification-modes.md @@ -62,6 +62,13 @@ 9. 负责整场正式交付时，在所有题目均为有效 sealed revision 后执行一次多 ID `build --no-cache`，再运行 `status`、深度 `verify-package` 和最终 PDF QA。 10. 最终交接必须区分已自动验证、已人工/Agent 审查、未验证和剩余风险；不得用“未发现问题”替代通过条件。 +多组数据累计约束属于三种模式共享的封题门槛。创作、修改或审查含 `T` 的题目时，先完整执行 `references/aggregate-limit-derivation.md`：推导的 `T_max` 必须在 `5..100000`，测试需求较大时的 `sum(n_i) <= 10*N` 只能作为满足复杂度条件后的候选，并且必须通过联合最坏数据与 `accepted_max_time * 3 <= TL` 校准。题面声明 `sum n`、总长度、总点数或总边数等累计上限时： + +- 必须读取 `probhub --json lint ` 的 `constraint_reconciliation.aggregate_constraints`；对应约束出现 `statement_only`、`aggregate_constraint_mismatch` 或 `dynamic` 时，不得因为 lint 仍为 warning 就继续 seal； +- 直接写法应得到 `state: matched`；静态分析不支持的函数封装、宏或复杂表达式必须由主 Agent 人工复核并记录证据，不能伪称自动匹配； +- `matched` 只证明直接语句形状和值可以对账。主 Agent 仍要确认使用足够宽的累加类型、累加器在循环前初始化、每组目标量恰好累计一次，并在读取完相关输入后执行与题面同值的 `ensuref` 或等价拒绝逻辑； +- 缺少实际累计或拒绝逻辑时，修复 Validator 并重新运行 lint、Judge 和受影响的 seal。变量名含 `sum`、错误位置的检查或只在错误分支执行的比较都不算通过。 + 模式不能削弱现有 Core 门禁。快速模式必须配置可用的 stress 链路，并使用固定 seed 完成 100 轮对拍；不得删除已有 `stress` 配置、减少到 100 轮以下或虚构跳过参数来绕过 `seal`。 ## 3. 快速模式 diff --git a/references/workspace-schema-v1.md b/references/workspace-schema-v1.md index 29c7d31..1b7b813 100644 --- a/references/workspace-schema-v1.md +++ b/references/workspace-schema-v1.md @@ -272,6 +272,8 @@ source hash 会递归覆盖 `code/` 下全部普通源码与辅助文本，包 `statement.source` 和 `judge.validator` 必须解析为题目目录内的普通非符号链接文件。lint 的 `constraint_reconciliation` 会保留题面输入范围与 Validator `readInt/readLong/readDouble/readStrictDouble/ensuref` 直接字面量的 path/line/raw 证据，并固定声明 `analysis_state: partial`。它不是完整 Markdown/C++ 语义分析：只有唯一同名变量的确定数值差异给 warning，动态、析取、歧义或不支持结构只要求人工复核，永不改变 lint 的 `ok` 或退出码。 +对多组数据，`aggregate_constraints` 还会保守识别 `$\sum_{i=1}^{T} n_i\le 2\times 10^5$`、`所有测试用例中的 n 之和不超过 2×10^5` 等直接题面表述，以及 Validator 中 `sum_n += n` / `sum_n = sum_n + n`、`sum_len += s.size()` 后由 `ensuref` 检查的直接累加器。主体规范化为 `sum:n`、`sum:len:s` 或 `sum:n+m`，并报告 `matched`、`statement_only`、`validator_only`、`dynamic` 与 `state`。题面缺失、Validator 缺失和确定数值不一致为非阻断 warning；检测到多测和单组规模、但没有直接累计约束时只提示人工复核。Core 不解析宏、函数封装、数组归约或任意 C++/自然语言表达式，也不会自动推导正确总量；出题人仍必须人工检查 `T × 单组上界`、算法复杂度和累加类型是否安全。 + 当前 Schema v1 不支持可执行的 `constraints` 单一事实源。未来 Token、临时 C++ header、缓存/hash、WebUI round-trip 和构建快照的完整评估见 [`constraints-schema-evaluation.md`](constraints-schema-evaluation.md)；在该设计落地前，不要向 `probhub.yaml` 添加未知 `constraints` 字段或宣称题面与 Validator 已自动同步。 非交互题的 `data/sample/*.ans` 还必须由配置顺序中的首个 accepted 精确复现。`probhub sample-check` 与完整 Judge 都只归一 CRLF/裸 CR 为 LF，尾空格、缺少尾换行等差异仍失败；Custom Checker 接受非唯一输出不能绕过正式样例答案一致性。交互题对此检查明确不适用。 diff --git a/scripts/check_release.py b/scripts/check_release.py index fae1b52..524fa20 100644 --- a/scripts/check_release.py +++ b/scripts/check_release.py @@ -203,6 +203,7 @@ def validate_pack_inventories(*, dry_run=True, destination=None): "references/cli.md", "references/lib.typ", "references/main.typ", "references/problems.typ", "references/usts.png", "references/testlib.h", "references/installation.md", + "references/aggregate-limit-derivation.md", "references/verification-modes.md", } missing = sorted(required_main - main_paths) diff --git a/tests/test_generations.py b/tests/test_generations.py index 92442f5..a498c10 100644 --- a/tests/test_generations.py +++ b/tests/test_generations.py @@ -296,7 +296,7 @@ def test_generation_uses_checkpoints_and_is_content_addressed(self): def test_artifact_builder_changes_create_new_generations(self): cases = ( - (("probhub_version",), "0.6.3"), + (("probhub_version",), "0.6.5"), (("typst_version",), "0.14.3"), (("pypdf_version",), "6.15.0"), (("template_hash",), "template-two"), diff --git a/tests/test_npm_packages.py b/tests/test_npm_packages.py index e559b9e..617e0fe 100644 --- a/tests/test_npm_packages.py +++ b/tests/test_npm_packages.py @@ -100,6 +100,58 @@ def test_release_metadata_gate_passes_for_the_source_tree(self): self.assertEqual(result.returncode, 0, result.stderr) self.assertTrue(json.loads(result.stdout)["ok"]) + def test_skill_requires_aggregate_validator_enforcement_review(self): + skill = (ROOT / "SKILL.md").read_text(encoding="utf-8") + verification = (ROOT / "references/verification-modes.md").read_text( + encoding="utf-8" + ) + for marker in ( + "constraint_reconciliation.aggregate_constraints", + "statement_only", + "aggregate_constraint_mismatch", + "足够宽的累加类型", + "每组目标量恰好累计一次", + "ensuref", + ): + with self.subTest(marker=marker): + self.assertIn(marker, skill) + self.assertIn(marker, verification) + + def test_skill_routes_and_covers_aggregate_limit_derivation(self): + skill = (ROOT / "SKILL.md").read_text(encoding="utf-8") + verification = (ROOT / "references/verification-modes.md").read_text( + encoding="utf-8" + ) + reference_path = ROOT / "references/aggregate-limit-derivation.md" + reference = reference_path.read_text(encoding="utf-8") + + self.assertIn("references/aggregate-limit-derivation.md", skill) + self.assertIn("references/aggregate-limit-derivation.md", verification) + release_check = (ROOT / "scripts/check_release.py").read_text(encoding="utf-8") + self.assertIn("references/aggregate-limit-derivation.md", release_check) + + scenarios = { + "test count range": ("1 <= T <= T_max", "5 <= T_max <= 100000"), + "linear high-demand default": ("C(n)/n", "sum(n_i) <= 10 * N"), + "joint feasibility": ("T_max * n_min <= K * N", "T_max >= K"), + "n log n": ("O(n log n)", "large_case_equivalents"), + "quadratic": ("O(n^2)", "K * C(N)"), + "graph": ("O(n+m)", "sum(m_i) <= K*M"), + "two-dimensional": ("O(nm)", "sum(n_i*m_i) <= K*N*M"), + "fixed per-case cost": ("T * F", "T*U"), + "high test count": ("100000", "input_io + output_io"), + "runtime calibration": ("accepted_max_time * 3 <= TL", "target_guarantee: false"), + "decision record": ("aggregate_limit_derivation:", "decision: accepted"), + "joint decision record": ("jointly_reachable: true", "decision: needs_review"), + } + for scenario, markers in scenarios.items(): + with self.subTest(scenario=scenario): + for marker in markers: + self.assertIn(marker, reference) + + self.assertIn("本文不是 Core Schema", reference) + self.assertIn("decision: needs_review", reference) + def test_npm_pack_json_accepts_legacy_and_current_single_package_shapes(self): from scripts import check_release @@ -147,7 +199,7 @@ def completed(stdout=""): require_head_tag=True, require_clean=True, ) - self.assertEqual(metadata["tag"], "v0.6.3") + self.assertEqual(metadata["tag"], "v0.6.5") with ( patch("scripts.check_release.shutil.which", return_value="git"), @@ -251,7 +303,7 @@ def test_node_entrypoints_cannot_be_shadowed_by_workspace_module(self): check=False, ) self.assertEqual(version.returncode, 0, version.stderr) - self.assertEqual(version.stdout.strip(), "0.6.3") + self.assertEqual(version.stdout.strip(), "0.6.5") installed = subprocess.run( [ @@ -279,7 +331,7 @@ def test_node_entrypoints_cannot_be_shadowed_by_workspace_module(self): marker = json.loads( (target / ".probhub-version.json").read_text(encoding="utf-8") ) - self.assertEqual(marker["version"], "0.6.3") + self.assertEqual(marker["version"], "0.6.5") def test_dependency_installer_requires_explicit_system_python_consent(self): from probhub import install_deps diff --git a/tests/test_process_control.py b/tests/test_process_control.py index bbeebc7..2c799e8 100644 --- a/tests/test_process_control.py +++ b/tests/test_process_control.py @@ -760,8 +760,8 @@ def run_command(self, root, code, **limits): cwd=root, ) - def wait_until_dead(self, pid): - deadline = time.time() + 5 + def wait_until_dead(self, pid, timeout=5): + deadline = time.time() + timeout while process_alive(pid) and time.time() < deadline: time.sleep(0.05) self.assertFalse(process_alive(pid), f"child process {pid} survived") @@ -1002,7 +1002,9 @@ def test_external_force_cancel_kills_detached_descendant(self): child_pid = int(pid_file.read_text(encoding="utf-8")) known_pids = snapshot_process_tree(proc.pid) terminate_external_process_tree(proc, known_pids) - self.wait_until_dead(child_pid) + # Under full-suite load taskkill may return before Windows has + # finished tearing down the detached process object. + self.wait_until_dead(child_pid, timeout=10) finally: if proc.poll() is None: terminate_external_process_tree(proc) diff --git a/tests/test_report.py b/tests/test_report.py index 0c0ccd5..a5d3308 100644 --- a/tests/test_report.py +++ b/tests/test_report.py @@ -32,12 +32,15 @@ def create_workspace(self, root): (problem / "problem.md").write_text( "# Report Problem\n\n" "## 题目描述\n\n求值。\n\n" - "## 输入格式\n\n输入整数 $n$（$1\\le n\\le 100$）。\n\n" + "## 输入格式\n\n第一行输入测试用例数 $T$。每组输入整数 $n$（$1\\le n\\le 100$）。\n\n" + "所有测试用例中的 $n$ 之和不超过 $100$。\n\n" "## 输出格式\n\n输出 $n$。\n", encoding="utf-8", ) (problem / "code/validator.cpp").write_text( - 'int main(){ inf.readInt(1, 100, "n"); }\n', encoding="utf-8" + 'int main(){ int T = inf.readInt(1, 10, "T"); int n = inf.readInt(1, 100, "n"); ' + 'long long sum_n = 0; sum_n += n; ensuref(sum_n <= 100, "sum"); }\n', + encoding="utf-8", ) (problem / "code/std.cpp").write_text("int main(){}\n", encoding="utf-8") (problem / "code/wrong.cpp").write_text("int main(){}\n", encoding="utf-8") @@ -218,6 +221,8 @@ def test_report_summarizes_tests_groups_recipes_headroom_and_kills(self): self.assertEqual(item["recipes"]["random"], 2) self.assertEqual(item["recipes"]["targeted"], 1) self.assertEqual(item["calibration"]["primary_headroom"], 5.0) + self.assertEqual(item["aggregate_constraints"]["state"], "matched") + self.assertEqual(item["aggregate_constraints"]["summary"]["matched"], 1) row = item["kill_matrix"]["rows"][0] self.assertEqual(row["cells"]["killer"]["state"], "killed") self.assertEqual(row["cells"]["random"]["state"], "not-targeted") @@ -247,10 +252,17 @@ def test_report_is_byte_for_byte_read_only_and_cli_supports_all_formats(self): self.assertIn("ProbHub 工作区报告", outputs["text"]) self.assertIn("击杀矩阵", outputs["text"]) self.assertIn("near-boundary=0/3", outputs["text"]) + self.assertIn("累计约束: matched", outputs["text"]) self.assertIn("# ProbHub 工作区报告", outputs["markdown"]) self.assertIn("| 题号 | ID |", outputs["markdown"]) self.assertIn("near-boundary 0/3", outputs["markdown"]) - self.assertEqual(json.loads(outputs["json"])["schema_version"], 1) + self.assertIn("累计约束：matched", outputs["markdown"]) + json_report = json.loads(outputs["json"]) + self.assertEqual(json_report["schema_version"], 1) + self.assertEqual( + json_report["problems"][0]["aggregate_constraints"]["state"], + "matched", + ) self.assertEqual(self.snapshot(root), before) def test_missing_recipes_and_targeted_groups_are_structured_warnings(self): diff --git a/tests/test_statement_consistency.py b/tests/test_statement_consistency.py index 0c3f4ab..6f4f1c9 100644 --- a/tests/test_statement_consistency.py +++ b/tests/test_statement_consistency.py @@ -547,6 +547,267 @@ def test_zero_constraint_evidence_requires_review_with_stable_fields(self): for item in report["diagnostics"] )) + def test_latex_aggregate_constraint_matches_validator_accumulator(self): + statement = VALID_STATEMENT.replace( + "Input.", + r"第一行输入测试用例数 $T$。对每组输入整数 $n_i$。" + "\n\n" + r"保证 $\sum_{i=1}^{T} n_i \le 2\times 10^5$。", + ) + validator = r'''int main() { + int T = inf.readInt(1, 10000, "T"); + long long sum_n = 0; + for (int tc = 0; tc < T; ++tc) { + int n = inf.readInt(1, 200000, "n"); + sum_n += n; + } + ensuref(sum_n <= 200000, "sum of n is too large"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertTrue(result["ok"], result) + self.assertTrue(aggregate["multi_case_detected"]) + self.assertEqual(aggregate["state"], "matched") + self.assertEqual(aggregate["summary"]["matched"], 1) + match = aggregate["matched"][0] + self.assertEqual(match["subject_normalized"], "sum:n") + self.assertEqual(match["normalized"], "sum:n <= 200000") + self.assertEqual(match["validator"]["origin"], "ensuref") + self.assertFalse(any( + diagnostic["code"].startswith("aggregate_constraint_") + for diagnostic in result["diagnostics"] + )) + + def test_chinese_aggregate_and_string_length_accumulators_match(self): + statement = VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$。每组输入整数 $n$ 和字符串 $s$。\n\n" + "所有测试数据的 $n$ 之和不超过 $2\\times 10^5$，" + "所有测试用例中的字符串 $s$ 的长度之和不超过 $10^6$。", + ) + validator = r'''int main() { + int T = inf.readInt(1, 10000, "T"); + long long total_n = 0, total_len = 0; + while (T--) { + int n = inf.readInt(1, 200000, "n"); + string s = inf.readToken("[a-z]+", "s"); + total_n = total_n + n; + total_len += s.size(); + } + ensuref(total_n <= 200000, "sum n"); + ensuref(total_len <= 1000000, "sum len"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "matched") + self.assertEqual( + {item["subject_normalized"] for item in aggregate["matched"]}, + {"sum:n", "sum:len:s"}, + ) + + def test_aggregate_sum_of_two_per_case_dimensions_matches(self): + statement = VALID_STATEMENT.replace( + "Input.", + r"第一行输入测试用例数 $T$。每组输入整数 $n_i,m_i$。" + "\n\n" + r"保证 $\sum_{i=1}^{T}(n_i+m_i) \le 4\times 10^5$。", + ) + validator = r'''int main() { + int T = inf.readInt(1, 10000, "T"); + long long sum_nm = 0; + for (int tc = 0; tc < T; ++tc) { + int n = inf.readInt(1, 200000, "n"); + int m = inf.readInt(1, 200000, "m"); + sum_nm += m + n; + } + ensuref(sum_nm <= 400000, "sum n + m"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "matched") + self.assertEqual( + aggregate["matched"][0]["subject_normalized"], + "sum:n+m", + ) + + def test_aggregate_statement_only_validator_only_and_mismatch_are_warnings(self): + cases = ( + ( + "statement_only", + VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$。每组输入整数 $n$。\n\n" + "所有测试用例中的 $n$ 之和不超过 $200000$。", + ), + 'int T = inf.readInt(1, 10, "T"); int n = inf.readInt(1, 200000, "n");\n', + "aggregate_constraint_statement_only", + ), + ( + "validator_only", + VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$。每组输入整数 $n$。", + ), + 'int T = inf.readInt(1, 10, "T"); long long sum_n = 0; ' + 'for (int tc = 0; tc < T; ++tc) { int n = inf.readInt(1, 200000, "n"); ' + 'sum_n += n; } ensuref(sum_n <= 200000, "sum");\n', + "aggregate_constraint_validator_only", + ), + ( + "mismatch", + VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$。每组输入整数 $n$。\n\n" + "所有测试用例中的 $n$ 之和不超过 $200000$。", + ), + 'int T = inf.readInt(1, 10, "T"); int n = inf.readInt(1, 200000, "n"); ' + 'long long sum_n = 0; sum_n += n; ensuref(sum_n <= 199999, "sum");\n', + "aggregate_constraint_mismatch", + ), + ) + for name, statement, validator, expected_code in cases: + with self.subTest(name=name), tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + codes = {item["code"] for item in result["diagnostics"]} + + self.assertTrue(result["ok"], result) + self.assertEqual(aggregate["state"], "requires_review") + self.assertIn(expected_code, codes) + diagnostic = next( + item for item in result["diagnostics"] if item["code"] == expected_code + ) + self.assertEqual(diagnostic["severity"], "warning") + + def test_dynamic_aggregate_bound_is_retained_for_review(self): + statement = VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$ 和上限 $K$。每组输入整数 $n$。\n\n" + "所有测试用例中的 $n$ 之和不超过 $K$。", + ) + validator = r'''int main() { + int T = inf.readInt(1, 10, "T"); + int K = inf.readInt(1, 200000, "K"); + int n = inf.readInt(1, 200000, "n"); + long long sum_n = 0; + sum_n += n; + ensuref(sum_n <= K, "sum"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "requires_review") + self.assertEqual(aggregate["summary"]["dynamic"], 2) + self.assertTrue(any( + item["code"] == "aggregate_constraint_dynamic" + for item in result["diagnostics"] + )) + + def test_multicase_without_aggregate_constraint_requests_manual_review(self): + statement = VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$（$1\\le T\\le 100$）。" + "每组输入整数 $n$（$1\\le n\\le 200000$）。", + ) + validator = r'''int main() { + int T = inf.readInt(1, 100, "T"); + for (int tc = 0; tc < T; ++tc) { + inf.readInt(1, 200000, "n"); + } + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "requires_review") + self.assertTrue(aggregate["multi_case_detected"]) + self.assertTrue(any( + item["code"] == "aggregate_constraint_review_required" + for item in result["diagnostics"] + )) + + def test_single_case_and_cpp_non_code_do_not_create_aggregate_evidence(self): + statement = VALID_STATEMENT.replace( + "Input.", "输入整数 $n$（$1\\le n\\le 200000$）。" + ) + validator = r'''int main() { + int n = inf.readInt(1, 200000, "n"); + // sum_n += n; + const char *text = "sum_n += n; ensuref(sum_n <= 1, aggregate)"; + long long sum_n = 0; + sum_n += n; + ensuref(sum_n <= 200000, "single-case sum"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "not_detected") + self.assertFalse(aggregate["multi_case_detected"]) + self.assertEqual(aggregate["statement_constraints"], []) + self.assertEqual(aggregate["validator_constraints"], []) + self.assertFalse(any( + item["code"].startswith("aggregate_constraint_") + for item in result["diagnostics"] + )) + + def test_preprocessor_accumulator_is_not_treated_as_executable_code(self): + statement = VALID_STATEMENT.replace( + "Input.", + "第一行输入测试用例数 $T$（$1\\le T\\le 100$）。" + "每组输入整数 $n$（$1\\le n\\le 200000$）。", + ) + validator = r'''#define ADD_N() sum_n += n + int main() { + int T = inf.readInt(1, 100, "T"); + long long sum_n = 0; + for (int tc = 0; tc < T; ++tc) { + int n = inf.readInt(1, 200000, "n"); + ADD_N(); + } + ensuref(sum_n <= 200000, "sum"); + } + ''' + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) + self.create_workspace(root, statement=statement, validator=validator) + result = self.lint(root) + aggregate = result["constraint_reconciliation"]["aggregate_constraints"] + + self.assertEqual(aggregate["state"], "requires_review") + self.assertEqual(aggregate["validator_constraints"], []) + self.assertTrue(any( + item["code"] == "aggregate_constraint_review_required" + for item in result["diagnostics"] + )) + def test_falsey_non_mapping_statement_config_is_rejected(self): for value in ([], "", 0, False): with self.subTest(value=value), tempfile.TemporaryDirectory() as temp: