P19.d DiffT Before 5211acfe95a0c6d82a60e2524b5e46b47fe67a3e After bb35b941115a0a9f818e8512eebe67c29ee68355 Threshold: ZERO semantic mismatches to declared oracle; ZERO reducer mismatches; all mandatory head assertions PASS. Compare each stream and service/upstream channel independently; ignore only cross-channel arrival interleaving. --- P19.d 5211acfe95a0c6d82a60e2524b5e46b47fe67a3e +++ P19.d bb35b941115a0a9f818e8512eebe67c29ee68355 @@ -15,12 +15,25 @@ }, { "actual": { - "reads": 0, - "value": null + "reads": 1, + "value": { + "aheadCount": 0, + "aheadOfDefaultCount": 1, + "behindCount": 0, + "hasUpstream": true, + "pr": { + "baseRef": "main", + "headRef": "A", + "number": 613, + "state": "open", + "title": "Fixture A", + "url": "https://github.com/proof-audit/status-fixture/pull/613" + } + } }, "expectedPredicate": true, - "observedPredicate": false, - "outcome": "FAIL", + "observedPredicate": true, + "outcome": "PASS", "test": "local plus absent remote is eligible", "virtualTimeMs": 0 }, @@ -84,46 +97,20 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], "insertions": 0 } }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } - }, - "value": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } + "remote": null + }, + "value": null }, "expectedPredicate": true, - "observedPredicate": false, - "outcome": "FAIL", + "observedPredicate": true, + "outcome": "PASS", "test": "incompatible missing-PR response discarded", "virtualTimeMs": 0 }, @@ -149,7 +136,7 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], @@ -187,13 +174,78 @@ } }, "expectedPredicate": true, - "observedPredicate": false, - "outcome": "FAIL", + "observedPredicate": true, + "outcome": "PASS", "test": "allowed next missing-PR lookup recovers B PR", "virtualTimeMs": 0 } ], - "branchProbeChannel": [], + "branchProbeChannel": [ + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "A", + "virtualTimeMs": 0 + }, + { + "branch": "B", + "virtualTimeMs": 0 + }, + { + "branch": "B", + "virtualTimeMs": 0 + }, + { + "branch": "B", + "virtualTimeMs": 0 + } + ], "checkpoints": [ { "name": "missing-PR-held", @@ -223,6 +275,15 @@ "virtualTimeMs": 0 }, { + "allowed": true, + "input": { + "cwd": "/proof/repo", + "type": "vcs-status" + }, + "kind": "background-policy", + "virtualTimeMs": 0 + }, + { "allowed": false, "input": { "cwd": "/proof/repo", @@ -261,13 +322,49 @@ ], "invalidationChannel": [ { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-local" + }, + { "kind": "invalidate-all" }, { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-local" + }, + { "kind": "invalidate-all" }, { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-local" + }, + { "kind": "invalidate-all" + }, + { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-remote" + }, + { + "kind": "invalidate-local" + }, + { + "kind": "invalidate-remote" } ], "localReadChannel": [ @@ -353,6 +450,90 @@ } }, "n": 4, + "virtualTimeMs": 0 + }, + { + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "n": 5, + "virtualTimeMs": 0 + }, + { + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "n": 6, + "virtualTimeMs": 0 + }, + { + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "n": 7, + "virtualTimeMs": 0 + }, + { + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "n": 8, "virtualTimeMs": 0 } ], @@ -377,31 +558,18 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], "insertions": 0 } }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - } - } + "remote": null }, "merged": { "aheadCount": 0, - "aheadOfDefaultCount": 1, + "aheadOfDefaultCount": 0, "behindCount": 0, "branchChanges": { "baseRef": "origin/main", @@ -409,19 +577,12 @@ "insertions": 1 }, "hasPrimaryRemote": true, - "hasUpstream": true, + "hasUpstream": false, "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "pr": { - "baseRef": "main", - "headRef": "A", - "number": 613, - "state": "open", - "title": "Fixture A", - "url": "https://github.com/proof-audit/status-fixture/pull/613" - }, - "refName": "A", + "pr": null, + "refName": "B", "workingTree": { "deletions": 0, "files": [], @@ -444,7 +605,7 @@ "hasWorkingTreeChanges": false, "isDefaultRef": false, "isRepo": true, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], @@ -488,7 +649,7 @@ "title": "Fixture B", "url": "https://github.com/proof-audit/status-fixture/pull/614" }, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [], @@ -506,7 +667,8 @@ "kind": "remote-read-start", "n": 1, "options": { - "refreshUpstream": true + "refreshMissingPullRequest": true, + "refreshUpstream": false }, "value": { "aheadCount": 0, @@ -864,122 +1026,7 @@ }, { "event": { - "_tag": "snapshot", - "local": { - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "refName": "A", - "workingTree": { - "deletions": 0, - "files": [], - "insertions": 0 - } - }, - "remote": null - }, - "merged": { - "aheadCount": 0, - "aheadOfDefaultCount": 0, - "behindCount": 0, - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasUpstream": false, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "pr": null, - "refName": "A", - "workingTree": { - "deletions": 0, - "files": [], - "insertions": 0 - } - }, - "virtualTimeMs": 0 - }, - { - "event": { - "_tag": "snapshot", - "local": { - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "refName": "A", - "workingTree": { - "deletions": 0, - "files": [], - "insertions": 0 - } - }, - "remote": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "hasUpstream": true, - "pr": null - } - }, - "merged": { - "aheadCount": 0, - "aheadOfDefaultCount": 1, - "behindCount": 0, - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasUpstream": true, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "pr": null, - "refName": "A", - "workingTree": { - "deletions": 0, - "files": [], - "insertions": 0 - } - }, - "virtualTimeMs": 0 - }, - { - "event": { - "_tag": "snapshot", - "local": { - "branchChanges": { - "baseRef": "origin/main", - "deletions": 0, - "insertions": 1 - }, - "hasPrimaryRemote": true, - "hasWorkingTreeChanges": false, - "isDefaultRef": false, - "isRepo": true, - "refName": "A", - "workingTree": { - "deletions": 0, - "files": [], - "insertions": 0 - } - }, + "_tag": "remoteUpdated", "remote": { "aheadCount": 0, "aheadOfDefaultCount": 1, @@ -1029,6 +1076,193 @@ { "event": { "_tag": "remoteUpdated", + "remote": null + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", + "remote": { + "aheadCount": 0, + "aheadOfDefaultCount": 1, + "behindCount": 0, + "hasUpstream": true, + "pr": null + } + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 1, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", + "remote": { + "aheadCount": 0, + "aheadOfDefaultCount": 1, + "behindCount": 0, + "hasUpstream": true, + "pr": { + "baseRef": "main", + "headRef": "A", + "number": 613, + "state": "open", + "title": "Fixture A", + "url": "https://github.com/proof-audit/status-fixture/pull/613" + } + } + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 1, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": { + "baseRef": "main", + "headRef": "A", + "number": 613, + "state": "open", + "title": "Fixture A", + "url": "https://github.com/proof-audit/status-fixture/pull/613" + }, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", + "remote": null + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "A", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "localUpdated", + "local": { + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + } + }, + "merged": { + "aheadCount": 0, + "aheadOfDefaultCount": 0, + "behindCount": 0, + "branchChanges": { + "baseRef": "origin/main", + "deletions": 0, + "insertions": 1 + }, + "hasPrimaryRemote": true, + "hasUpstream": false, + "hasWorkingTreeChanges": false, + "isDefaultRef": false, + "isRepo": true, + "pr": null, + "refName": "B", + "workingTree": { + "deletions": 0, + "files": [], + "insertions": 0 + } + }, + "virtualTimeMs": 0 + }, + { + "event": { + "_tag": "remoteUpdated", "remote": { "aheadCount": 0, "aheadOfDefaultCount": 2, @@ -1066,7 +1300,7 @@ "title": "Fixture B", "url": "https://github.com/proof-audit/status-fixture/pull/614" }, - "refName": "A", + "refName": "B", "workingTree": { "deletions": 0, "files": [],