diff --git a/research/deferred-signed/README.md b/research/deferred-signed/README.md index 5879168905..121e3ba636 100644 --- a/research/deferred-signed/README.md +++ b/research/deferred-signed/README.md @@ -38,9 +38,12 @@ checks. Replay uses temporary directories and leaves frozen evidence intact. The rational tensor control requires SymPy; the other new drivers use the standard library. CI installs the pinned dependency for replay. -`validation-prior/` preserves the original executed audit sources and measured -native receipts. The portability checker permits only two documented path -substitutions; it does not silently treat different mathematical code as an +The validation-prior directory preserves the original executed audit sources +and structured native receipts. Four historical replay log files are excluded +by the root .gitignore rule for log files; their SHA-256 values remain recorded in +SOURCE.json under ignored_log_sha256, but the raw log contents are not shipped +or required by the replay. The portability checker permits only two documented +path substitutions; it does not silently treat different mathematical code as already-passed check. Machine elapsed times are excluded from regenerated mathematical-output comparisons. The `new_multiplication_bound: false` fields in these historical receipts accurately record their scope when run; the diff --git a/research/deferred-signed/SOURCE.json b/research/deferred-signed/SOURCE.json index 3521d3c5cd..fe6d0bc5ef 100644 --- a/research/deferred-signed/SOURCE.json +++ b/research/deferred-signed/SOURCE.json @@ -6,7 +6,7 @@ "Makefile": "d3da97587cfa850d826bbb450f13121ff46e4e87bc91681e669279557562494a", "README.md": "5fe2101e1bd639a1739e4986c807f3a659b463a8a5873126e11727e8e63298a1", "research/deferred-signed/PROOF.md": "cf5cced8cecace5f4308647523bc86a0869daeb1aa49c382bec03411674a1741", - "research/deferred-signed/README.md": "b1d761d02a5bb3413f705c9fac321a96e9b42f4bfd949c175131af97316b7463", + "research/deferred-signed/README.md": "3d8ca54fb959c62835ce0612bbb764eb7bfde593adbfcd39f35e866d09ee741b", "research/deferred-signed/check_complex_identity.py": "8a31abe1d46ab3aa76b954cb87004e28d4974cce5eea2dea17d6283992902e7d", "research/deferred-signed/round6-complex-interface-controls.json": "7f4375ff2baefd6455d5353968d4c1a38666cda7f417ebd21286f09e16131d22", "research/deferred-signed/round6-complex-literal-ledger/result.json": "db1d41515236c2710b4caeb22d91eea63cf1deeb0d659346d0661da71ed07baa", @@ -122,23 +122,25 @@ "research/deferred-signed/swapnil-round7/tests/test_round7.py": "c0e988d363f9d989275693b340e97b59dc16e4d8835e1e9ea3d4c589da277a0f", "research/deferred-signed/swapnil-round7/tests/test_witness.py": "8cc1b358bd92a31d454c7dc9a2739d1d9cb53f19e3f88035aa4cd6babf11cb77", "research/deferred-signed/validation-prior/complex-prior-replay.json": "04201d7df9fe95f10859d482a2386b65fdcba5f8d7347e7837866de88ff75de4", - "research/deferred-signed/validation-prior/frames-replay.log": "3895170eb8078f6d7c9f0d814f54cc24b01309abcbe183a361d101e634a99998", - "research/deferred-signed/validation-prior/lifted-replay.log": "e24e6b3e793f49808dc14c36799a11140938d6fb53ba7bdce92a99f89b277671", "research/deferred-signed/validation-prior/round6_complex_interface_controls.py": "7ca3e245c7bdd814d6315f2b32ef5e0d4610834dd9e3190cc551a182c87bf5ed", "research/deferred-signed/validation-prior/round6_complex_literal_ledger.py": "b973d467d949912edc1cf65ee22703f9692431de72e3d87d82f442a6f7a61a1c", "research/deferred-signed/validation-prior/round7_balanced_assembly_candidate.py": "e10abe35cc8b536d78eda3e234ef48a6a7e49019893ec3d920779f2ac66443fd", "research/deferred-signed/validation-prior/round7_literal_frame_ledger.py": "02617ba608f971e3bdd2b45d4cbfc3d0d629873a0b9f7c22b12f347d099fdb59", "research/deferred-signed/validation-prior/round7_tensor_endpoint_controls.py": "f1487b01167ef37cd180a0d969c815bcf26e627f3c264b89ccd974b63478ae91", - "research/deferred-signed/validation-prior/stair-replay.log": "8a7cad5cb0ff905203c46da45642224d178cfd8c9d7d97a1502f1195705f0231", - "research/deferred-signed/validation-prior/stair_control-replay.log": "82bf3dda4e3f5ec4e3ca796a5544364e2864a28a877642773132e902da4755d6", "research/deferred-signed/validation-prior/swapnil-round7-full-basis.json": "1bcd74316f11ebc2c36f0c9b5638f314a3982c97e96c572816602087169f0e42", "research/deferred-signed/validation-prior/swapnil-round7-moment-audit.json": "92567c2050caeaf987358acee5dde5d8610e0f12bff6385899e3c043d6cefb89", "research/deferred-signed/validation-prior/swapnil-round7-validation-job.json": "bb9488bd2c19423e4ccff4cd8e5052f0848a5b107a133a31179c020d26a7465e", - "research/deferred-signed/verify.py": "cebcddbdfc553c37da7ab6b66b7e94c1dcd0610b82e79453ed937831c400c418", + "research/deferred-signed/verify.py": "87db1a2df0e7b79248266f4a307d0d2d22c1b9fbd8205039486a283295def475", "scripts/structured_bulk_assembly.py": "e99467e14211fba699878ed036e1e2362eb8e395dc22f9ecdcecc7fbf2cc736d", "research/deferred-signed/VALIDATION.json": "c267be2b45769619b1fcb078b5aaa40f24ce1f0345161d180f138d297cd19264", "research/joint-dual/SOURCE.json": "0f2bc2e6d72534ab3884d050abdc328b112cbc4296e6cc04516f65ab87ee96b2", "certificates/joint-dual-kappa.json": "6dff7f3bd3bf149714e9f161892c944d8788d0894ff0c4056610a3283368253e", "certificates/joint-dual-validation.json": "9af3bb95c2dacb7ffb410936f284ca5b0c288fc8ce492a97b349161dfc978113" + }, + "ignored_log_sha256": { + "research/deferred-signed/validation-prior/frames-replay.log": "3895170eb8078f6d7c9f0d814f54cc24b01309abcbe183a361d101e634a99998", + "research/deferred-signed/validation-prior/lifted-replay.log": "e24e6b3e793f49808dc14c36799a11140938d6fb53ba7bdce92a99f89b277671", + "research/deferred-signed/validation-prior/stair-replay.log": "8a7cad5cb0ff905203c46da45642224d178cfd8c9d7d97a1502f1195705f0231", + "research/deferred-signed/validation-prior/stair_control-replay.log": "82bf3dda4e3f5ec4e3ca796a5544364e2864a28a877642773132e902da4755d6" } } diff --git a/research/deferred-signed/verify.py b/research/deferred-signed/verify.py index b3536e65e5..9b36b211c0 100644 --- a/research/deferred-signed/verify.py +++ b/research/deferred-signed/verify.py @@ -34,6 +34,14 @@ def verify_pins(): pins=read(HERE/'SOURCE.json') for rel,sha in pins['files'].items(): assert hashlib.sha256((ROOT/rel).read_bytes()).hexdigest()==sha,('source drift',rel) + ignored_logs=pins.get('ignored_log_sha256',{}) + assert set(ignored_logs)=={ + 'research/deferred-signed/validation-prior/frames-replay.log', + 'research/deferred-signed/validation-prior/lifted-replay.log', + 'research/deferred-signed/validation-prior/stair-replay.log', + 'research/deferred-signed/validation-prior/stair_control-replay.log', + } + assert all(rel.endswith('.log') and len(sha)==64 and all(c in '0123456789abcdef' for c in sha) for rel,sha in ignored_logs.items()) foreign=read(HERE/'swapnil-round7/IMPORT.json') for rel,sha in foreign['files'].items(): assert hashlib.sha256((HERE/'swapnil-round7'/rel).read_bytes()).hexdigest()==sha,('foreign drift',rel) @@ -46,12 +54,12 @@ def verify_pins(): if name=='round7_balanced_assembly_candidate.py': old=old.replace("HERE/'integration/scripts'", "HERE.parents[1]/'scripts'").replace("HERE/'integration/scripts/structured_bulk_assembly.py'", "HERE.parents[1]/'scripts/structured_bulk_assembly.py'") assert old==(HERE/name).read_text(),('unreviewed port edit',name) - return len(pins['files']) + return len(pins['files']),len(ignored_logs) def main(): assert __debug__,'verification requires assertions' ap=argparse.ArgumentParser();ap.add_argument('--replay',action='store_true');ap.add_argument('--replay-own',action='store_true');args=ap.parse_args() - count=verify_pins();bit=read(HERE/'round7-literal-ledger/result.json');cx=read(HERE/'round6-complex-literal-ledger/result.json') + count,ignored_logs=verify_pins();bit=read(HERE/'round7-literal-ledger/result.json');cx=read(HERE/'round6-complex-literal-ledger/result.json') assert all(bit[k] for k in ('complete_forward_F2','complete_reflected_F2','reflected_frame_continuity','histogram_matches_external')) assert all(cx[k] for k in ('actual_forward_equal_frames','reflected_continuity','actual_geometry_passed','histogram_matches_pinned')) H={int(t):n for t,n in bit['histogram'].items()};C={int(t):n for t,n in cx['full_histogram'].items()} @@ -94,6 +102,6 @@ def main(): assert r.returncode==0,(argv,r.stdout[-4000:]) if '--control' in argv:assert 'certified=False' in r.stdout print('PASS native',argv,flush=True) - print('PASS',count,'pins; both independent moments; 47 constraints; 7 margins; kappa=63965813/10^12 > 2^-14') + print('PASS',count,'tracked pins;',ignored_logs,'ignored legacy-log hashes recorded; both independent moments; 47 constraints; 7 margins; kappa=63965813/10^12 > 2^-14') print('Conditional on retained analytic/fixed-tape interfaces; not formal verification of the full theorem.') if __name__=='__main__':main()