diff --git a/research/t37-log-coverage-seed86/CERTIFICATE.json b/research/t37-log-coverage-seed86/CERTIFICATE.json new file mode 100644 index 0000000000..20560bc6e4 --- /dev/null +++ b/research/t37-log-coverage-seed86/CERTIFICATE.json @@ -0,0 +1,17 @@ +{ + "coverage_sha256": "b5fa760daf68386f0f833ddeac78089827aa131bc6fcea8788e356ba58af0249", + "rejected_control_names_sha256": "5366ce50d5ba4a70393bea3407241e206ef6f6d805049a38347ec4189c17f807", + "frozen_native_predicate_lines": [194, 196], + "native_omissions_accepted_by_frozen_component": [ + "native/barch.log", + "native/barch-controls.log", + "native/layer-end-controls.log", + "native/native.log", + "native/ledgers.log", + "native/local-replay.log", + "native/wrappers.log", + "native/phases.log" + ], + "native_content_changes_observed_without_rejection": 8, + "synthetic_cold_log_count": 35 +} diff --git a/research/t37-log-coverage-seed86/CLAIM.md b/research/t37-log-coverage-seed86/CLAIM.md new file mode 100644 index 0000000000..0688dffabe --- /dev/null +++ b/research/t37-log-coverage-seed86/CLAIM.md @@ -0,0 +1,75 @@ +# T37 execution-log coverage claim + +Claimed 2026-10-13 17:24 UTC. OS-random seed 86 selects verification +engineering under the user's 85-94 mapping. Cycle began 17:17:25 UTC; +verification and handoff start by 17:47:25 UTC; finish by 17:57:25 UTC. +Base main: `2921874911956718fcaaaf9396fe8267b3cfa9f0`, fetched and confirmed +fast-forwarded from CrocSwap. Prior checkout and branches are preserved. +Branch: `research/cycle04-seed86-t37-log-coverage`. + +Three candidates were considered: + +1. Check all T37 stage logs, including the eight native logs whose existence + is not checked by the frozen final binder. Chosen. +2. Audit receipt scalar types in isolation. Deferred; type checks belong to + the concrete stage-evidence admission boundary in the chosen scope. +3. Reduce repeated source hashing. Rejected without a demonstrated bottleneck. + +Exact object: the four stage indexes and 34 logs in +`research/community-frontier942-audit/t37-replay.tar.gz`, produced by +Jonathan Capalbo's selected PR942 T37 construction and its pinned U8 ancestry. +Hypothesis: a portable supplementary evidence check can reject every omitted +log, including native omissions that the frozen native-stage predicates do +not inspect, while accepting the unchanged archived stage evidence. + +Method: inspect the actual producers and final binder; bind their exact source +bytes; verify complete ordered indexes, exact integer success codes, required +log presence and each digest that the producer records. Demonstrate the +native omission boundary using the unmodified source predicates, with a +clearly stated component-level scope. Exhaust all single-log omissions and +run changed-log, sequence, type and source-pin controls. Do not equate a +receipt or a log with authenticated execution or a full theorem proof. + +Deliverable: a small standard-library checker, reproducible archive audit and +exact control receipt, source pins, scope/credit/license documentation and +handoff. No mathematical improvement is proposed. The optimistic effect on +the complete selected invoice and kappa is zero. No stronger supplier or +kappa is assumed. No selected record, source package, or upstream file changes. + +Coordination: immediately before this claim, checked all 753 open PR bodies +through #1058, recent repository comments and pinned issues. No pinned issue +or matching active claim exists, so this claim is local. Relevant existing +work includes #865's PR799 evidence contract, #851's bridge coverage, #991's +different T37 witness/payload controls and #1006's owner-audit bitmap speedup. +None covers this current T37 log inventory. The review ledger and retained +negative scopes were read; no closed mathematical search is reopened. + +Stopping rule: finish the declared archive and control census; if useful +evidence or relevant checks fail, preserve the patch and an honest handoff. +At most one focused PR; refresh metadata and overlap before submission. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +New files are Apache-2.0; predecessor notices and source licenses remain. + +## Completed result, 2026-10-13 17:42 UTC + +Published one focused PR: https://github.com/CrocSwap/integer-mult-bounds/pull/1073 +and attached it to the originating chat. The archive passes at 34 logs, +26 producer-recorded digests and eight native presence-only logs. All 80 +declared negative controls reject. The original native-stage source slice +admits all eight native-log omissions; native content changes deliberately +remain accepted by the supplementary checker while changing its observation. +This is scoped evidence-coverage work, not a mathematical counterexample. + +Both tested Python runtimes, optimized workers, relocated minimal closure, +public CLI controls, 25 selected-record tests, three replay-coverage tests and +the selected-record check pass. Full receipt SHA-256 is +`e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0`. +Final overlap checked 739 open PRs through #1072 and recent comments. +Refreshed upstream `abdc6a7002abdbcd9e21bfc5e1a795784deacfdf` retains all +12 consumed/context pins. No pinned sprint issue exists, and neither requested +Codex label is available. This is the claim's single result update. + +No full supplier or invoice replay, full make verify, Linux CI result or new +kappa is asserted. Selected sources, prior branches and upstream are unchanged. +Verification and handoff began by 17:30 UTC, before the reserved final interval. diff --git a/research/t37-log-coverage-seed86/README.md b/research/t37-log-coverage-seed86/README.md new file mode 100644 index 0000000000..8561483c3b --- /dev/null +++ b/research/t37-log-coverage-seed86/README.md @@ -0,0 +1,143 @@ +# T37 execution-log coverage + +The selected T37 archive contains 34 stage logs. The frozen native-stage +admission predicates read `native/STEPS.json`, check its eight stage names and +compare each exit code with zero. They do not inspect the eight native logs. +This package supplies a supplementary, read-only coverage check for the four +execution indexes and every corresponding log. It changes no selected files. + +The exact result is limited to evidence admission. The replay below executes +the original three source statements at `final_binding.py:194-196`, with no +rewrites, against the archived native index. Each of the eight native-log +deletions leaves those predicates passing. The new check rejects all eight. +This is a component-level counterexample to log completeness. The complete +original final binder is not executed by this package, and no counterexample +to the mathematical construction is claimed. + +## Reproduce + +From the repository root, with Python 3.11 or newer and no third-party packages: + +```sh +rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/verify.py +``` + +Expected output: + +```text +PASS_T37_LOG_COVERAGE_CONTROLS 34 logs; 80 rejections; 8 native omissions admitted by frozen slice +``` + +The verifier checks five immutable source/archive SHA-256 pins, derives the +stage order from the three actual producer programs, copies only the indexes +and logs into a temporary directory, and runs the complete declared controls. +It compares the canonical coverage and ordered control-name digests with +`CERTIFICATE.json`. Canonical JSON uses sorted keys and separators `,` and `:`. +The temporary directory is removed. The committed archive stays unchanged. +The source pins apply to immutable inputs, not to regenerated gzip containers. + +Append `--out /new/path/receipt.json` to write the full report, including every +log digest and control name. Its parent must exist. Output is created only +after success, with exclusive creation; existing files are not overwritten. +Both ordinary and optimized Python execute all new checks. The original +native predicates are explicitly compiled with assertions enabled. + +The public CLI controls exercise source drift, safe output handling, missing +logs, an escaping symlink, a minimal relocated checkout with spaces, and full +receipt equality between ordinary and optimized workers: + +```sh +rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/test_cli.py +``` + +Expected: `PASS_T37_LOG_CLI_CONTROLS` with receipt SHA-256 +`e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0`. +The test driver uses assertions and rejects optimized execution itself. + +For a completed T37 replay directory: + +```sh +rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/audit.py --work /path/to/t37/replay +``` + +For the archived reuse mode, the success line is: + +```text +PASS_T37_STAGE_LOG_COVERAGE 34 logs; 26 producer digests; 8 presence-only +``` + +The actual producer also supports a cold-baseline mode. That mode requires its +additional first stage and log, giving 35 logs and 27 producer digest checks. +The control suite exercises that branch with a synthetic log, explicitly not +with a cold supplier execution. `audit.py` checks the fixed T37 log contract; +it does not establish source identity, inspect the rest of the replay, or +substitute for `make frontier942-verify`. + +## Coverage and limits + +| Layer | Logs | Producer-recorded digests checked | +|---|---:|---:| +| Top-level T37, reused baseline | 13 | 13 | +| Native U8 | 8 | 0 | +| Discovery | 6 | 6 | +| Strict replay | 7 | 7 | +| Total | 34 | 26 | + +All four ordered indexes must be complete and have integer zero exit codes. +Every expected log must be a regular file contained in the replay directory. +An empty log is valid; the actual `build-parent.log` is empty. There is no +heuristic success-text check. + +The 80 negative controls cover every single-log omission, every changed log +with a producer-recorded digest, and five mutations of each index: omission +of its final stage, reversal, failure status 1, boolean false and floating zero. +The verifier restores and rechecks the original evidence after the mutations. +All 34 archived logs must be accounted for. This finite census is complete for +that declared class; arbitrary multi-file changes are outside the census. + +The eight native logs have no producer-recorded digests. The checker records +their current hashes but does not claim to validate those bytes against an +earlier commitment. Eight native-content changes deliberately remain accepted +while changing the observed hashes. This positive limitation control prevents +claiming stronger coverage than the format supplies. A forged self-consistent +receipt is not authenticated execution. Archive integrity, receipt consistency, +fresh execution and mathematical proof are separate claims. + +No new kappa, supplier improvement, cost reduction, or broad search result is +proposed. The selected conditional value remains +`1661960547713947/1000000000000000000`. The optimistic change to the complete +selected cost invoice is zero. The all-size/compiler, realization, hosting, +precision/tape, analytic and bit-interface assumptions remain. No full +supplier replay, invoice recomputation, Lean proof or Linux CI is claimed here. + +## Sources and credit + +The base is `2921874911956718fcaaaf9396fe8267b3cfa9f0`. The reviewed source +head is `1960cfa919a0945d0ca4cb14ea96237000037903`, PR942, integrated in +`3825dc0ea1317629864ebeb6929719cc4bbf525f`. `SOURCES.json` distinguishes the +five consumed inputs from historical context pins. Context pins describe the +base commit only; a later change to the moving selected pointer does not +invalidate this fixed archive audit. + +Jonathan Capalbo supplied the T37 construction, producers and final binder. +Chafik Boukhalfa supplied the T21 construction, and Hao Yan supplied the T16 +and independent owner-audit lineage. The native producer is retained through +the PR869/870 U8 work and Jeremy Kothe's PR799 X4 ancestry. Its notices retain +NewBArch, ColdWitness/icekylinx and the earlier factory, gauge and controller +credits. Douglas Colkitt supplied the maintainer coverage wrapper and archived +review. Lucas, @ljste, supplied the preceding ancestor audit. Stephen Shore, +@nightangelflowerwin-ops, supplied PR865's source-versioned coverage work, and +Adem Vessell supplied PR851's bridge controls. Their packages and notices +remain unchanged. + +This scope extends the evidence-coverage idea from #865 to the current T37 log +inventory. It does not repeat #991's alternate owner schedule and payload +controls, #1006's bitmap owner audit, or the T37 arithmetic audits #1051/#1052. +The local `CLAIM.md` records the random assignment, coordination scan, rejected +candidates and fixed stopping rule. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance in design, +implementation, analysis and documentation. No independent human review is +claimed. New files are Apache-2.0 under the repository root license. The source +predicate slice is executed from the pinned original file; predecessor +copyright, license and AI-assistance notices remain in force. diff --git a/research/t37-log-coverage-seed86/SOURCES.json b/research/t37-log-coverage-seed86/SOURCES.json new file mode 100644 index 0000000000..b77c6bad32 --- /dev/null +++ b/research/t37-log-coverage-seed86/SOURCES.json @@ -0,0 +1,23 @@ +{ + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "selected_kappa": "1661960547713947/1000000000000000000", + "selected_source_head": "1960cfa919a0945d0ca4cb14ea96237000037903", + "integration_commit": "3825dc0ea1317629864ebeb6929719cc4bbf525f", + "runtime": "Python 3.11 or newer, standard library only", + "consumed_sha256": { + "research/community-frontier942-audit/t37-replay.tar.gz": "48285025105210b56a32d3d4d57a21b7591760acc709d38073e4dca339eb06fe", + "research/complex-t37-owners/verify.py": "4d880a6237c2f5d4f4e08374e2a4ddbe7bdcc972fe4ee0e879e9a547754f5fd0", + "research/complex-t37-owners/replay.py": "7834f469861df4a8ed82550762e7d1640123f547a715b55a937dea0cb381cedd", + "research/complex-t37-owners/final_binding.py": "61e8a8856ebc36feee11cbf6e60f2ace3b9b89195c3282f565a651488cf947f7", + "research/complex-t21-owners/vendor/pr870/construction/barch/reproduce_barch.py": "19bc970aa6af25ab0e7fa96fb65c64dd0c5243976d8f2cb733cba839155482c1" + }, + "context_sha256_at_base_only": { + "certificates/selected-result.json": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3", + "research/complex-t37-owners/DEPENDENCY-PINS.json": "0160ea2677cc9ceeb0f861dc2774d470a27cbaa58b8fd6c064cf0683d18f3e87", + "research/complex-t37-owners/MANIFEST.json": "38907d05fddac9be6bf7a7aff47fae43114a055d2259cead5651a08f9b983820", + "research/complex-t37-owners/NOTICE.md": "78887899d460a21fc6bf6e6021fea7f6864a93e079b639e7c92d4dc77ca30c1e", + "scripts/verify_frontier942.py": "27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7", + "docs/research/community-batch952-review.md": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + } +} diff --git a/research/t37-log-coverage-seed86/VALIDATION.json b/research/t37-log-coverage-seed86/VALIDATION.json new file mode 100644 index 0000000000..4131bbd00e --- /dev/null +++ b/research/t37-log-coverage-seed86/VALIDATION.json @@ -0,0 +1,53 @@ +{ + "verified_at_utc": "2026-10-13T17:36:15Z", + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "pre_submission_upstream": "abdc6a7002abdbcd9e21bfc5e1a795784deacfdf", + "pre_submission_consumed_and_context_pins": "All 12 remain byte-identical on refreshed main", + "pre_submission_overlap": "739 open PR bodies checked through #1072 at 17:41 UTC, plus recent coordination comments; no matching T37 log-coverage scope. Neither codex nor codex-automation label exists.", + "platform": "macOS 26.5.2 arm64", + "runtimes": [ + "CPython 3.11.15, Clang 22.1.3", + "CPython 3.14.8, Clang 21.0.0 clang-2100.1.1.101" + ], + "dependencies": "Python standard library only", + "implementation_sha256": { + "audit.py": "629cb5535e470596e4e69b706179bc83c0b099226cd97788bcecee33feb3db9e", + "verify.py": "9f072f56a9744a0dc488c46432adddeccf6c66aadb796fbacaa0548805c36eb4", + "test_cli.py": "f32762774369d983c341e1c6d0371db4431d0f471cef092fb28ae85ba73a3c9a", + "SOURCES.json": "ea2909baee224375a67908a7de861518c0d18f5c5e0f01731557380e4aec2485", + "CERTIFICATE.json": "e53a9cb25e44b5f01f620375f53a0c00f2dc567e907532d2e0808fd9140420c2" + }, + "commands": [ + "rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/verify.py", + "rtk proxy python3 -I -B -O research/t37-log-coverage-seed86/verify.py", + "rtk proxy python3.11 -I -B research/t37-log-coverage-seed86/test_cli.py", + "rtk proxy python3 -I -B research/t37-log-coverage-seed86/test_cli.py", + "rtk proxy python3.11 -I -B -m unittest discover -s tests -p 'test_selected*.py'", + "rtk proxy python3.11 -I -B -m unittest discover -s tests -p 'test_replay_coverage.py'", + "rtk proxy python3.11 -I -B scripts/verify_selected_result.py" + ], + "results": { + "archive_log_count": 34, + "producer_digest_checks": 26, + "native_presence_only_logs": 8, + "negative_controls_rejected": 80, + "native_omissions_accepted_by_original_source_component": 8, + "native_content_mutations_accepted_but_digest_changed": 8, + "full_receipt_sha256": "e834d7037dee9071f14b0c0a3194c84c8f036d1160ca512f84d2a578992170c0", + "receipt_identical_across_runtimes_optimized_and_relocated": true, + "cli_source_pin_output_safety_missing_log_symlink_controls": "PASS", + "existing_selected_tests_passed": 25, + "existing_replay_coverage_tests_passed": 3, + "selected_record_check": "PASS", + "context_pins_at_recorded_base": "PASS" + }, + "initial_failure_and_resolution": "The first archive projection rejected the macOS /var temporary path because it resolves through /private/var. Resolving the temporary root before containment comparison fixed the checker itself. Both runtime replays then passed without altering source evidence.", + "not_executed": [ + "complete original T37 final binder", + "native supplier reconstruction or cold ancestry replay", + "full invoices, exact moments or outer assembly", + "full make verify", + "Linux CI or formal multiplication proof" + ], + "scope": "Supplementary stage/log evidence admission. No execution authentication, mathematical counterexample, supplier cost improvement or new kappa. Selected sources and upstream remain unchanged. Substantial OpenAI Codex assistance; Apache-2.0." +} diff --git a/research/t37-log-coverage-seed86/audit.py b/research/t37-log-coverage-seed86/audit.py new file mode 100644 index 0000000000..209409a7dd --- /dev/null +++ b/research/t37-log-coverage-seed86/audit.py @@ -0,0 +1,92 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Supplementary T37 stage/log coverage, not a supplier or execution proof. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +The fixed stage orders come from Jonathan Capalbo's PR942 and its U8 producer. +""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path + + +TOP = ( + 'ancestry-coverage', 'baseline799-binding', 'u8-native', 'prepare', + 'frozen-construction', 'independent-owners', 'build-parent', 'check-parent', + 'independent-price', 'discovery', 'strict', 'payload-controls', 'final-binding', +) +NATIVE = ( + 'barch', 'barch-controls', 'layer-end-controls', 'native', 'ledgers', + 'local-replay', 'wrappers', 'phases', +) +COMMON = ('bind', 'emit', 'audit', 'invoice', 'assembly') +INDEXES = { + 'STAGES.json': ('name', TOP), + 'native/STEPS.json': ('step', NATIVE), + 'discovery/STAGES.json': ('name', COMMON + ('freeze',)), + 'strict/STAGES.json': ('name', COMMON + ('admission-controls', 'bit-controls')), +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def file_at(work, name): + path = (work / name).resolve() + require(path.is_relative_to(work) and path.is_file(), 'Missing or escaping file: ' + name) + return path + + +def check(work): + """Check a completed T37 directory without running or changing its contents.""" + work = Path(work).resolve() + logs = {} + for relative, (key, expected) in INDEXES.items(): + index = file_at(work, relative) + stages = json.loads(index.read_bytes()) + require(type(stages) is list and all(type(s) is dict for s in stages), + 'Invalid stage index: ' + relative) + names = tuple(s.get(key) for s in stages) + allowed = (expected,) + if relative == 'STAGES.json': + allowed += (('baseline799-cold',) + expected,) + require(names in allowed, 'Stage sequence differs: ' + relative) + for stage in stages: + name = (Path(relative).parent / (stage[key] + '.log')).as_posix() + require(type(stage.get('exit_code')) is int and stage['exit_code'] == 0, + 'Stage did not record integer success: ' + name) + digest = sha256(file_at(work, name).read_bytes()).hexdigest() + bound = relative != 'native/STEPS.json' + if bound: + require(stage.get('log_sha256') == digest, 'Stage log digest differs: ' + name) + logs[name] = {'sha256': digest, 'producer_digest_checked': bound} + return { + 'status': 'PASS_T37_STAGE_LOG_COVERAGE', + 'stage_indexes': len(INDEXES), + 'logs': logs, + 'producer_digest_checks': sum(v['producer_digest_checked'] for v in logs.values()), + 'presence_only_logs': sum(not v['producer_digest_checked'] for v in logs.values()), + 'scope': 'Ordered successful stage records and log coverage only. Native log ' + 'digests are observations, not producer commitments. No supplier replay, ' + 'execution authentication, mathematical acceptance or new kappa.', + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--work', type=Path, required=True) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = check(args.work) + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + stream.write(json.dumps(result, sort_keys=True, indent=2) + '\n') + print(result['status'], len(result['logs']), 'logs;', + result['producer_digest_checks'], 'producer digests;', + result['presence_only_logs'], 'presence-only') + + +if __name__ == '__main__': + main() diff --git a/research/t37-log-coverage-seed86/test_cli.py b/research/t37-log-coverage-seed86/test_cli.py new file mode 100644 index 0000000000..0d605f94bd --- /dev/null +++ b/research/t37-log-coverage-seed86/test_cli.py @@ -0,0 +1,86 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exercise output safety and source/path admission through the public CLIs. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tarfile +import tempfile + +if not __debug__: + raise RuntimeError('Run CLI tests with assertions enabled') + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +REL = PACKAGE.relative_to(ROOT) + + +def run(script, *args, optimized=False): + command = [sys.executable, '-I', '-B'] + (['-O'] if optimized else []) + return subprocess.run(command + [str(script), *map(str, args)], capture_output=True, text=True) + + +with tempfile.TemporaryDirectory(prefix='t37-cli-validation-') as temporary: + root = Path(temporary).resolve() + reports = [] + for optimized in (False, True): + output = root / (str(optimized) + '.json') + p = run(PACKAGE / 'verify.py', '--out', output, optimized=optimized) + assert p.returncode == 0, p.stderr + reports.append(output.read_bytes()) + assert reports[0] == reports[1] + + relocated = root / 'relocated with spaces' + inputs = json.loads((PACKAGE / 'SOURCES.json').read_bytes())['consumed_sha256'] + for name in list(inputs) + [str(REL / n) for n in ('audit.py', 'verify.py', 'SOURCES.json', 'CERTIFICATE.json')]: + target = relocated / name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, target) + p = run(relocated / REL / 'verify.py', '--out', root / 'relocated.json') + assert p.returncode == 0, p.stderr + assert (root / 'relocated.json').read_bytes() == reports[0] + + source = relocated / 'research/complex-t37-owners/verify.py' + source.write_bytes(source.read_bytes() + b'\n# source corruption control\n') + output = root / 'must-not-exist.json' + p = run(relocated / REL / 'verify.py', '--out', output) + assert p.returncode != 0 and 'Source pin differs' in p.stderr and not output.exists() + sentinel = root / 'preserved.json' + sentinel.write_bytes(b'preserve existing output\n') + p = run(relocated / REL / 'verify.py', '--out', sentinel) + assert p.returncode != 0 and 'Source pin differs' in p.stderr + assert sentinel.read_bytes() == b'preserve existing output\n' + p = run(PACKAGE / 'verify.py', '--out', sentinel) + assert p.returncode != 0 and 'FileExistsError' in p.stderr + assert sentinel.read_bytes() == b'preserve existing output\n' + + evidence = root / 'evidence' + evidence.mkdir() + with tarfile.open(ROOT / 'research/community-frontier942-audit/t37-replay.tar.gz') as bundle: + for member in bundle.getmembers(): + if member.name in ('STAGES.json', 'native/STEPS.json', 'discovery/STAGES.json', 'strict/STAGES.json') or member.name.endswith('.log'): + target = evidence / member.name + assert member.isfile() and target.resolve().is_relative_to(evidence) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(bundle.extractfile(member).read()) + p = run(PACKAGE / 'audit.py', '--work', evidence, '--out', root / 'audit.json') + assert p.returncode == 0, p.stderr + missing = evidence / 'native/phases.log' + original = missing.read_bytes() + missing.unlink() + p = run(PACKAGE / 'audit.py', '--work', evidence, '--out', output) + assert p.returncode != 0 and 'Missing or escaping file: native/phases.log' in p.stderr + assert not output.exists() + outside = root / 'outside.log' + outside.write_bytes(original) + missing.symlink_to(outside) + p = run(PACKAGE / 'audit.py', '--work', evidence) + assert p.returncode != 0 and 'Missing or escaping file: native/phases.log' in p.stderr + +print('PASS_T37_LOG_CLI_CONTROLS: optimized equivalence, relocation, source pin, ' + 'output preservation, missing log, escaping symlink; receipt ' + hashlib.sha256(reports[0]).hexdigest()) diff --git a/research/t37-log-coverage-seed86/verify.py b/research/t37-log-coverage-seed86/verify.py new file mode 100644 index 0000000000..0e8fe22a01 --- /dev/null +++ b/research/t37-log-coverage-seed86/verify.py @@ -0,0 +1,192 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Replay the pinned T37 log inventory and exhaust its single-log omissions. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +This executes the frozen native-stage predicates, not the full final binder. +""" +import argparse +import ast +from copy import deepcopy +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import tarfile +import tempfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +spec = importlib.util.spec_from_file_location('t37_log_audit', PACKAGE / 'audit.py') +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) +require = audit.require + + +def check_producer_orders(): + def declarations(relative): + tree = ast.parse((ROOT / relative).read_bytes()) + calls = sorted((n for n in ast.walk(tree) if isinstance(n, ast.Call) + and isinstance(n.func, ast.Name) and n.func.id == 'run' + and isinstance(n.args[0], ast.Constant)), key=lambda n: n.lineno) + return tree, tuple(n.args[0].value for n in calls) + _, top = declarations('research/complex-t37-owners/verify.py') + _, native = declarations('research/complex-t21-owners/vendor/pr870/construction/barch/reproduce_barch.py') + tree, discovery = declarations('research/complex-t37-owners/replay.py') + loops = [n for n in ast.walk(tree) if isinstance(n, ast.For) + and isinstance(n.target, ast.Tuple) + and [t.id for t in n.target.elts] == ['name', 'script', 'out']] + require(len(loops) == 1, 'Strict control declarations changed') + strict = discovery[:-1] + tuple(x[0] for x in ast.literal_eval(loops[0].iter)) + require(top == ('baseline799-cold',) + audit.TOP and native == audit.NATIVE + and discovery == audit.INDEXES['discovery/STAGES.json'][1] + and strict == audit.INDEXES['strict/STAGES.json'][1], 'Producer stage orders differ') + + +def native_predicates(source): + """Compile exactly the frozen native index read and its next two assertions.""" + tree = ast.parse(source.read_bytes()) + function = next(n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'check') + offsets = [i for i, n in enumerate(function.body) if isinstance(n, ast.Assign) + and len(n.targets) == 1 and isinstance(n.targets[0], ast.Name) + and n.targets[0].id == 'steps'] + require(len(offsets) == 1, 'Native-stage source slice changed') + body = function.body[offsets[0]:offsets[0] + 3] + require(len(body) == 3 and all(isinstance(n, ast.Assert) for n in body[1:]), + 'Native-stage assertions changed') + # Explicit optimization level retains the original predicates under python -O. + code = compile(ast.Module(body=body, type_ignores=[]), str(source), 'exec', optimize=0) + + def check(work): + exec(code, {'work': work, 'read': lambda p: json.loads(p.read_bytes())}) + return check, [body[0].lineno, body[-1].end_lineno] + + +def verify(): + sources = json.loads((PACKAGE / 'SOURCES.json').read_bytes()) + for name, digest in sources['consumed_sha256'].items(): + require(sha256((ROOT / name).read_bytes()).hexdigest() == digest, 'Source pin differs: ' + name) + check_producer_orders() + archive = ROOT / 'research/community-frontier942-audit/t37-replay.tar.gz' + frozen, lines = native_predicates(ROOT / 'research/complex-t37-owners/final_binding.py') + rejected = [] + native_omissions_accepted = [] + native_changes_observed = [] + with tempfile.TemporaryDirectory(prefix='t37-log-coverage-') as temporary: + work = Path(temporary).resolve() + with tarfile.open(archive) as bundle: + members = bundle.getmembers() + names = [m.name for m in members] + require(len(names) == len(set(names)), 'Duplicate archive member') + wanted = set(audit.INDEXES) | {n for n in names if n.endswith('.log')} + for name in sorted(wanted): + member = bundle.getmember(name) + target = work / name + require(member.isfile() and target.resolve().is_relative_to(work), + 'Invalid archived evidence: ' + name) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(bundle.extractfile(member).read()) + baseline = audit.check(work) + require(set(baseline['logs']) == wanted - set(audit.INDEXES), 'Unaccounted archived log') + require(len(baseline['logs']) == 34 and baseline['producer_digest_checks'] == 26 + and baseline['presence_only_logs'] == 8, 'Archived coverage changed') + frozen(work) + + def reject(name, operation): + try: + operation() + except ValueError: + rejected.append(name) + else: + raise RuntimeError('Accepted negative control: ' + name) + + for name, entry in baseline['logs'].items(): + path = work / name + original = path.read_bytes() + try: + path.unlink() + if not entry['producer_digest_checked']: + frozen(work) + native_omissions_accepted.append(name) + reject('omit:' + name, lambda: audit.check(work)) + path.write_bytes(original + b'\nchanged log control\n') + if entry['producer_digest_checked']: + reject('alter:' + name, lambda: audit.check(work)) + else: + changed = audit.check(work) + require(changed['logs'][name]['sha256'] != entry['sha256'], + 'Native content change was not observed') + native_changes_observed.append(name) + finally: + path.write_bytes(original) + + for name in audit.INDEXES: + path = work / name + original = path.read_bytes() + pristine = json.loads(original) + variants = [('omitted-stage', pristine[:-1]), ('reordered', list(reversed(pristine)))] + for value in (1, False, 0.0): + changed = deepcopy(pristine) + changed[0]['exit_code'] = value + variants.append(('exit-' + repr(value), changed)) + try: + for kind, value in variants: + path.write_text(json.dumps(value), encoding='utf-8') + reject(kind + ':' + name, lambda: audit.check(work)) + finally: + path.write_bytes(original) + # The current producer also has a cold-baseline branch. This is a + # synthetic coverage-positive control, not a cold supplier execution. + path = work / 'STAGES.json' + original = path.read_bytes() + cold = work / 'baseline799-cold.log' + try: + cold.write_bytes(b'synthetic coverage control\n') + stage = dict(name='baseline799-cold', exit_code=0, + log_sha256=sha256(cold.read_bytes()).hexdigest()) + path.write_text(json.dumps([stage] + json.loads(original)), encoding='utf-8') + require(len(audit.check(work)['logs']) == 35, 'Cold stage coverage differs') + finally: + path.write_bytes(original) + cold.unlink() + require(audit.check(work) == baseline, 'Pristine evidence was not restored') + identity = lambda value: sha256(json.dumps(value, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + certificate = { + 'coverage_sha256': identity(baseline), + 'rejected_control_names_sha256': identity(rejected), + 'frozen_native_predicate_lines': lines, + 'native_omissions_accepted_by_frozen_component': native_omissions_accepted, + 'native_content_changes_observed_without_rejection': len(native_changes_observed), + 'synthetic_cold_log_count': 35, + } + require(certificate == json.loads((PACKAGE / 'CERTIFICATE.json').read_bytes()), + 'Exact coverage/control certificate differs') + return { + 'status': 'PASS_T37_LOG_COVERAGE_CONTROLS', + 'coverage': baseline, + 'consumed_sha256': sources['consumed_sha256'], + 'frozen_native_predicate_lines': lines, + 'frozen_native_predicates_accept_omissions': native_omissions_accepted, + 'native_content_changes_observed_without_rejection': native_changes_observed, + 'rejected_controls': rejected, + 'synthetic_cold_log_count': 35, + 'scope': 'Archived log evidence and component-level native predicates only. ' + 'The complete original binder, native supplier, invoices and theorem ' + 'were not replayed. No counterexample to the mathematics is claimed.', + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = verify() + if args.out: + with args.out.open('x', encoding='utf-8') as stream: + stream.write(json.dumps(result, sort_keys=True, indent=2) + '\n') + print(result['status'], len(result['coverage']['logs']), 'logs;', + len(result['rejected_controls']), 'rejections;', + len(result['frozen_native_predicates_accept_omissions']), 'native omissions admitted by frozen slice') + + +if __name__ == '__main__': + main()