Experiment formal verification receipt provider results 01 - kmosoti/FabricO11y GitHub Wiki

Native receipt verification: finite measurements

Alpha acceptance was paused for this engineering work. Synthetic receipts below are explicitly marked: their commands were not executed. They test the verifier, not product acceptance. The receipt protocol, representation contract, hash ablation and provider discrimination preceded runs.

At clean source a5c834728d8c667f7422e94a2bf63fd91a4f0589, both default RustCrypto and optional OpenSSL variants completed their differential/benchmark drivers with actual exit 0 and confirmed whole-tree stops. Each matched the unchanged Python reference on 21 common decisions and deliberately rejected four representation aliases that Python accepted. Positive reports matched after normalizing environment observations. Earlier lint/resolution failures and slower scalar/assembly measurements remain retained; these measurements do not retroactively qualify them.

Measured provider comparison

The CPU was an i7-10750H with AVX2 and no SHA instruction flag. Each corpus had ten logs of the listed size, one warmup per implementation and seven alternating Python/native pairs. Timing includes process startup, Git/registry checks and complete log hashing; fixtures and compilation are outside timing. OpenSSL and default batches ran in that fixed order, rather than interleaved with each other. All files were on the mounted DATA volume under the required resource launcher.

Bytes per log Default native median OpenSSL native median Python median in OpenSSL batch
64 B 15.462 ms 15.914 ms 59.052 ms
64 KiB 18.298 ms 17.112 ms 60.408 ms
4 MiB 171.136 ms 94.132 ms 134.623 ms

The ten-large-log native ratio of medians fell 45.0%; OpenSSL's median paired reduction relative to Python was 30.2%. The tiny native case regressed 2.9%, or 0.453 ms. Native maximum RSS medians were about 6.6 MiB, Python about 21.2 MiB. GNU time CPU observations have 0.01-second precision and are not wall times. These are warm finite local measurements, not a universal engine ranking.

Python and the candidate resolved the same local libcrypto 3.5.9 file. Agreement between them alone is therefore not an independent crypto oracle. Known vectors and RustCrypto cross-checks across ten sizes and ten chunk boundaries separately checked the adapter; all three digest tests exited 0. The feature's full 56-test suite exited 0 before a test-only typed-array adjustment; afterward the three digest tests, all-target/all-feature Clippy, formatting and release build exited 0. Default crypto remains portable and unchanged unless the explicit feature is enabled. The earlier optional assembly backend improved the large native case only about 9.2% and remained slower than Python; it was not adopted.

Evidence and remaining work

DATA-relative provider report: results/verification-provider-ablation-01/actual-comparison-01.json, SHA-256 fcccc4f879ffd1cf1e72fcb6d0baa4bc8207a0c4df3a4c68ac0757d428a7191a. It pins both driver reports, wrapper exits/stops and archived ELF identities. OpenSSL differential completed at 2026-10-18T02:58:59.933206Z; default completed at 03:00:10.239411Z. Full-input digest verification has an Omega(B) byte-reading bound; changing the provider reduces constant cost, not the work required for integrity.

The subsequently executed isolated hash-comparison mutant established the named defect observation below. Production dispatcher integration, complete required checks, architecture/docs validation and explicit workflow adoption remain necessary. No acceptance, security certification, general optimality or release completion follows from these experiments.

Executed hash-comparison defect control

The isolated source fb9244da384ae942d0fd8150f007b5ab387661f3 changed only ArtifactStore's final digest decision to permit a non-JSON input with a mismatched pin: expected.is_none_or(|pin| actual == pin) || !keep_json. Full reading, path/metadata checks, budgets and JSON checks remained in place. This is a deliberately defective experiment artifact, never a production candidate.

The feature build exited 0 and stopped at 2026-10-18T03:07:31.472388Z. Both executables were then copied to owned DATA artifacts with mode 0500. The existing differential driver ran against that pinned mutant and exited 1, with the outer launcher also recording 1 and confirmed whole-tree stop at 2026-10-18T03:08:38.894341Z. Its report remains overall_status=failed.

The positive fixture exited 0 for both Python and the mutant. Exactly one unexpected mismatch occurred: modified-log exited 1 in the unchanged Python reference and 0 in the defective native checker. The other 24 cases retained their expected outcomes, including all four declared strict representation differences. There were no driver/setup errors; benchmarks were deferred and no timing corpus ran. Source, reference and ELF identities remained unchanged. Thus the actual 1 records detection of this concrete checker defect; an arbitrary nonzero exit would not satisfy the control.

  • Raw report: results/rust-tooling-migration/receipt-mutant-01/candidate-report.json, SHA-256 684630520e0b5b26c0ef30a5152c445bb55185906785abcb7d8f4d32ad52c5d8.
  • Reviewed execution: results/verification-receipt-mutant-01/actual-result-01.json.
  • Mutant ELF SHA-256: c0da06842ee973953e64c08045d5772003ea1cc0e45620450d7b5064cf5329c1.
  • Driver ELF SHA-256: 3cd0180265d2f7c7da57162d70bb4a32ca0c7682d64e3cc97c87211bf4a7968f.
  • Outer stop receipt SHA-256: a955343f434361792de275c145b8b62216f93a9fbe192829280a4f65c51b6b07.

The actual command through the original resource launcher was:

/run/media/kmosoti/data/FabricO11y/results/verification-receipt-mutant-01/artifacts/receipt_differential --candidate /run/media/kmosoti/data/FabricO11y/results/verification-receipt-mutant-01/artifacts/xtask /run/media/kmosoti/data/FabricO11y/results/rust-tooling-migration/receipt-mutant-01

The complete literal environment/launcher argv and executable hashes are preserved in results/verification-receipt-mutant-01/experiment-plan-01.json and its actual mutant-differential-01.json wrapper. All runs used the original 16/20 GiB limits, no swap and 1800-second deadline, a fresh whole-DATA 95 GB census and 2 GiB reservation. The failure directory was retained; no failed result was rewritten as a normal success.