Repository navigation
Merge cycle/129: coh runs an arbitrary FLAT CM expressed in JSON #38
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: coh-min | |
| # The coh-min slice's CI gate. Builds the stdlib-only runtime under the | |
| # canonical `dune`, then runs every acceptance oracle #129 declares. Each gate | |
| # stage is its OWN step as well as a `make gate` prerequisite, so a failure is | |
| # visible in the job summary without reading the gate log. | |
| # | |
| # Triggers on the cycle branch so β sees it green before merge. | |
| on: | |
| push: | |
| branches: [ main, master, 'cycle/**' ] | |
| pull_request: | |
| defaults: | |
| run: | |
| working-directory: research/cm-language/runtime/coh-min | |
| jobs: | |
| coh-min: | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Set up OCaml | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: "5.2" | |
| - name: Install dune | |
| # coh-min is stdlib-only and carries no .opam file, so there are no | |
| # deps to resolve — only the build tool itself. | |
| run: opam install dune -y | |
| - name: Fetch cue | |
| # Fetched as a pinned release binary (the same pattern the linkcheck | |
| # job uses for lychee), so the vetting gates are deterministic and need | |
| # no opam/go toolchain. | |
| run: | | |
| set -euo pipefail | |
| ver=v0.9.2 | |
| curl -fsSL "https://github.com/cue-lang/cue/releases/download/${ver}/cue_${ver}_linux_amd64.tar.gz" \ | |
| | tar xz cue | |
| sudo mv cue /usr/local/bin/cue | |
| cue version | |
| - name: Build | |
| run: opam exec -- dune build | |
| # AC12 / #127: the vendored JSON and SHA-256 must stay BYTE-IDENTICAL to | |
| # ascent-0's. Checked in CI rather than trusted, because a drift here | |
| # would silently change every digest the receipts bind. | |
| - name: "Vendored files byte-identical to ascent-0" | |
| run: | | |
| set -euo pipefail | |
| cmp lib/json.ml ../ascent-0/lib/json.ml | |
| cmp lib/sha256.ml ../ascent-0/lib/sha256.ml | |
| echo "lib/json.ml and lib/sha256.ml are byte-identical to ../ascent-0/lib/" | |
| # AC1: the headline. No CM identity and no CM-specific classifier may | |
| # appear in the acceptance path; both are DISCOVERED from the shipped IRs. | |
| # Quoted: an unquoted `#` starts a YAML comment and would truncate a name. | |
| - name: "AC1 genericity (no cm_id branch, no classifier)" | |
| run: opam exec -- make genericity | |
| # AC7/AC12: every shipped IR is a canonical #NormalizedCMIR, and every | |
| # refusal fixture matches the cue verdict recorded for it. | |
| - name: "AC7 vet IRs against #NormalizedCMIR" | |
| run: opam exec -- make vet-ir | |
| - name: Test (unit + end-to-end) | |
| run: opam exec -- dune runtest | |
| # AC1/AC3/AC4/AC12: both methodologies over every discovered case, plus | |
| # the input-sensitivity check (no two receipts byte-identical). | |
| - name: "AC1/AC3/AC4 measurement cases (both methodologies)" | |
| run: opam exec -- make cases | |
| # AC3/AC5/AC6/AC11: every discovered fail-closed case, with zero receipt | |
| # bytes measured rather than assumed. | |
| - name: "AC5/AC6/AC11 fail-closed refusals" | |
| run: opam exec -- make refusals | |
| - name: "AC7 emitted artifacts vet against their 0.2 contracts" | |
| run: opam exec -- make vet | |
| - name: "AC7 schemas are non-vacuous" | |
| run: opam exec -- make vet-non-vacuity | |
| # AC8 / design gate 9: one missing-block case per canonical block for all | |
| # four artifact families, refused by BOTH cue and the runtime. | |
| - name: "AC8 gate-9 matrix (all four artifact families)" | |
| run: opam exec -- make vet-negative | |
| - name: "AC12 path confinement (fail-closed, zero receipt bytes)" | |
| run: opam exec -- make confine | |
| - name: "AC13 gate (AC1-12)" | |
| run: opam exec -- make gate |