Skip to content

Experiment: compare cold probability identities on isolated runners - #1003

Closed
Nicola-Ceornea wants to merge 3 commits into
masterfrom
experiment/probability-cold-1002-20261020
Closed

Nicola-Ceornea wants to merge 3 commits into
masterfrom
experiment/probability-cold-1002-20261020

Conversation

@Nicola-Ceornea

Copy link
Copy Markdown
Member

Feasibility experiment for #1002: two independent hosted jobs fetch pinned dependencies without an Actions cache, freshly rebuild the existing proof project, and record all 15 current input/toolchain/policy identity fields for comparison.

This draft is not intended to merge. It does not enable reuse, modify the gate or claim a complete verification pass; semantic controls and canaries are outside this measurement. The experiment is restricted to this branch. Validation: actionlint passed.

@Nicola-Ceornea

Copy link
Copy Markdown
Member Author

The strengthened cache-free feasibility experiment passed on both independent hosted runners: all 14 preparation identity fields remain identical after fresh builds, and all 15 final identity fields match between runners. All 2,824 closures were audited. The missing direct Mathlib roots and ProofWidgets dependency bookkeeping target are now prepared explicitly; no identity fields were excluded.

Run: https://github.com/EthereumPhone/PQ1/actions/runs/39488413242

This experiment is not a complete semantic-control gate. Production implementation and full validation are in draft PR #1008 for #1002. Closing this disposable experiment without merging; its branch and retained evidence remain available.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant