Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 76 additions & 0 deletions .github/workflows/complete-record-source.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
name: complete-record-source

on:
pull_request:
paths:
- .github/workflows/complete-record-source.yml
- tests/Broker.NativeProof/RuntimeEvidence/**
workflow_dispatch:

permissions:
contents: read

concurrency:
group: complete-record-source-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true

jobs:
complete-record-source:
name: complete-record-source
runs-on: ubuntu-24.04
timeout-minutes: 10
steps:
- name: Check out the exact candidate
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
with:
ref: ${{ github.event.pull_request.head.sha || github.sha }}
fetch-depth: 2
persist-credentials: false

- name: Bind the checked-out candidate
shell: bash
env:
EXPECTED_SHA: ${{ github.event.pull_request.head.sha || github.sha }}
run: |
set -euo pipefail
test "$(git rev-parse HEAD)" = "$EXPECTED_SHA"
test -z "$(git status --porcelain --untracked-files=all)"

- name: Set up the exact .NET SDK
uses: actions/setup-dotnet@a98b56852c35b8e3190ac28c8c2271da59106c68 # v6
with:
dotnet-version: 10.0.401

- name: Set up the exact Node.js runtime
uses: actions/setup-node@249970729cb0ef3589644e2896645e5dc5ba9c38 # v6
with:
node-version: 24.8.0
cache: npm
cache-dependency-path: tests/Broker.NativeProof/RuntimeEvidence/tools/quint/package-lock.json

- name: Install the integrity-locked Quint CLI
shell: bash
run: npm ci --ignore-scripts --prefix tests/Broker.NativeProof/RuntimeEvidence/tools/quint

- name: Restore and build the typed evidence project
shell: bash
env:
CI: 'true'
DOTNET_PROCESSOR_COUNT: '1'
run: |
set -euo pipefail
project=tests/Broker.NativeProof/RuntimeEvidence/RuntimeEvidence.Tests.fsproj
dotnet restore "$project" --locked-mode
dotnet build "$project" --configuration Release --no-restore --maxcpucount:1

- name: Run the complete-record source gate
shell: bash
env:
CI: 'true'
DOTNET_PROCESSOR_COUNT: '1'
run: |
set -euo pipefail
export PATH="$PWD/tests/Broker.NativeProof/RuntimeEvidence/tools/quint/node_modules/.bin:$PATH"
dotnet test tests/Broker.NativeProof/RuntimeEvidence/RuntimeEvidence.Tests.fsproj \
--configuration Release --no-restore --no-build \
--logger 'console;verbosity=normal'
6 changes: 6 additions & 0 deletions docs/roadmaps/barc-01-useful-play.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,12 @@ The existing `.5b/.5f` source window has two independent corrections: HighBar mu

Count1 correlation/final-read proof remains distinct from actual quantity and later game completion. The subsequent `.5f` six-journey boundary retains construction/economy/combat/reclaim, guard/repair, factory/rally/queue, selected modes, local/generated pointer and keyboard, and independent imported tactical policies. Unknown outcomes stay unknown; optional atomic replacement and `.7` publication remain separate.

The complete-record runtime-evidence source is ready for protected delivery when its hosted
source gate passes. That gate uses a sanitized mechanical growing-log fixture, the typed F#
reducer, 27 canonical Quint scenarios, 14 ITFs, full concrete-state/effect correspondence,
and duplicate/order/prior-state refusal controls. This is source-delivery readiness only;
the stock product identity is unchanged and native useful-play acceptance remains **0/6**.

## Historical source checkpoint

BARC-01.5a is implemented locally from FSBar `f1a18c52246b88e958344cb3bcc87f3c2035a62e` and HighBar `680b62480bfb60a19b3591b7250e03787e1f93d1`. The checkpoint advances only the additive live sibling and browser tactical schema; the frozen five-file HighBar bundle remains byte-identical. It defines `LIVE_CONTROL_PROTOCOL_TACTICAL_V1` / `barc-live-tactical-v1` revision 1, while V1 peers retain the `.4` subset and must refuse tactical bodies before arm. Producer and consumer commit/readback references remain pending until the parent joins the tested local commits. `.5b–f` and the overall `.5` outcome remain open.
Expand Down
6 changes: 6 additions & 0 deletions tests/Broker.NativeProof/RuntimeEvidence/CodecTests.fs
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,12 @@ module CodecTests =
let finalDiagnostic=diagnostic.Replace(observation,finalObservation).Replace(observationHash,sha(bytes(finalObservation+"\n"))).Replace(operationBase64,Convert.ToBase64String(bytes refusedOperation)).Replace(operationHash,sha(bytes refusedOperation))
let projected=evaluate finalDiagnostic|>Codec.complete
if not(projected.Contains("\"status\":\"observed-failure\"") && projected.Contains($"\"check\":\"{check}\"") && projected.Contains("\"nativeAcceptance\":false")) then failwithf "final custody check refused: %s" check
for check,outcome,category in [ "infolog-record-settlement-exhausted","refused","refused"; "infolog-record-settlement-deadline","deadline","operation-unknown" ] do
let settlementObservation=observation.Replace("\"check\":\"policy-result-join\"",$"\"check\":\"{check}\"").Replace("\"outcome\":\"policy-nonaccepted\"",$"\"outcome\":\"{outcome}\"").Replace("\"policyObservation\":"+policyObservation,"\"policyObservation\":null")
let settlementOperation=$"{{\"schema\":\"fsbar.barc-stock-operation-result/v1\",\"status\":\"failed\",\"category\":\"{category}\"}}\n"
let settlementDiagnostic=diagnostic.Replace(observation,settlementObservation).Replace(observationHash,sha(bytes(settlementObservation+"\n"))).Replace(operationBase64,Convert.ToBase64String(bytes settlementOperation)).Replace(operationHash,sha(bytes settlementOperation))
let projected=evaluate settlementDiagnostic|>Codec.complete
if not(projected.Contains("\"status\":\"observed-failure\"") && projected.Contains($"\"check\":\"{check}\"") && projected.Contains("\"policyObservation\":null") && projected.Contains("\"nativeAcceptance\":false")) then failwithf "settlement diagnostic refused: %s" check
let rawLeak=mechanicalDiagnostic.Replace("\"check\":\"infolog-final-refresh\"","\"check\":\"PRIVATE_SENTINEL\"")
if (evaluate rawLeak|>Codec.complete).Contains("PRIVATE_SENTINEL") then failwith "unrecognized diagnostic detail escaped"
let oversized=diagnostic+String(' ',8193)
Expand Down
Loading