From e684417e1d79cd73e5fec572a8fb38ac3ad62209 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:48:32 +0000 Subject: [PATCH 1/7] ci: assert Idris 2 0.8.0 in CI/required, the version the digest-pinned image ships What was wrong: .github/workflows/ci.yml asserted `idris2 --version` matches 0.7.0 while its container image (pinned by digest, the same digest trope-check.yml uses and documents as 0.8.0) ships 0.8.0, so "CI / required" was red on main from 2026-10-21 (run 39622697863) for a reason unrelated to any change. Issue #83. What changed: the case label and the error message say 0.8.0. The digest is unchanged; the version note now agrees with it, as the comment above the image asks. What I ran: actionlint -shellcheck= -pyflakes= .github/workflows/ci.yml -> clean. What I did not run: the job itself (no Idris 2 in this session); CI on this pull request is the check. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 06e6d7c..435726c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -77,8 +77,8 @@ jobs: ver="$(idris2 --version)" echo "idris2 --version -> ${ver}" case "$ver" in - *"0.7.0"*) ;; - *) echo "::error::expected Idris 2 0.7.0, got: ${ver}"; exit 1 ;; + *"0.8.0"*) ;; + *) echo "::error::expected Idris 2 0.8.0, got: ${ver}"; exit 1 ;; esac idris2 --typecheck abi.ipkg From c3601a68b1e73aa3049d534864a544a9f82c2692 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:48:32 +0000 Subject: [PATCH 2/7] test(check-examples): under TROPECHECK_REQUIRED=1 a missing canonical schema is a failure What was wrong: when ../trope-checker is absent the schema-drift guard printed a note and the script could still exit 0, so under TROPECHECK_REQUIRED=1 (CI) a guard that silently did not run looked green (review finding on #81). The header comment also said the script "lowers" the examples; it checks the checked-in examples/*.ir.json documents and lowers nothing (there is no compiler yet). What changed: with TROPECHECK_REQUIRED=1 and no canonical schema the script prints FAIL and exits 1, mirroring the existing missing-binary rule; without the variable it still skips with a note that names the switch. Header comment corrected. Output strings and exit codes on the happy path are unchanged. What I ran (all with the fast core built from trope-checker 4ecba4f): sibling present, REQUIRED=1 -> ok x7, exit 0 no sibling, REQUIRED=1 -> FAIL ... schema-drift guard did not run, exit 1 no sibling, unset -> note ... skipping schema-drift guard, exit 0 bash -n tests/check-examples.sh -> ok Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- tests/check-examples.sh | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/tests/check-examples.sh b/tests/check-examples.sh index d090700..b802ca3 100644 --- a/tests/check-examples.sh +++ b/tests/check-examples.sh @@ -2,9 +2,12 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# Every Haec example lowers to a well-formed Trope IR document. Pure bash + jq, -# no Python. Self-contained: structural checks against the vendored IR contract. -# The full round-trip (verdicts) runs when the sibling trope-checker is present. +# Every checked-in example IR (examples/*.ir.json — lowered by hand; there is no +# compiler yet) is a well-formed Trope IR document. This script checks those +# documents; it does not lower anything. Pure bash + jq, no Python. +# Self-contained: structural checks against the vendored IR contract. The +# schema-drift guard and the full round-trip (verdicts) run when the sibling +# trope-checker is present. set -uo pipefail ROOT="$(cd "$(dirname "$0")/.." && pwd)" @@ -36,8 +39,12 @@ if [ -f "$SIB/schemas/trope-ir.schema.json" ]; then else echo -e "${R}FAIL${O} vendored IR schema has drifted from trope-checker/schemas/trope-ir.schema.json"; fail=1 fi +elif [ "${TROPECHECK_REQUIRED:-0}" = "1" ]; then + # Under TROPECHECK_REQUIRED=1 (CI) a guard that silently does not run is a + # fake gate, exactly as for the checker binary below. + echo -e "${R}FAIL${O} TROPECHECK_REQUIRED=1 but no canonical schema at $SIB/schemas/trope-ir.schema.json — schema-drift guard did not run"; fail=1 else - echo -e "${Y}note${O} sibling trope-checker not checked out; skipping schema-drift guard" + echo -e "${Y}note${O} sibling trope-checker not checked out; skipping schema-drift guard (TROPECHECK_REQUIRED=1 makes this fatal)" fi # 4. full round-trip: verdicts via the reference checker. From 0c385f4fb54398eade871332e4f2dcc50e86028a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:48:32 +0000 Subject: [PATCH 3/7] ci(trope-check): pin the checker at trope-checker 4ecba4f and re-vendor the canonical IR schema What was wrong: trope-check.yml checked out trope-checker at 69221ad6 (main @ 2026-07-28), which predates the spec v0.2 consolidation that landed there on 2026-10-31 (#107) and the decoder fixes of #109; the vendored design/trope-ir.schema.json matched that old revision only, so against current trope-checker main the drift guard fails. What changed: the checkout ref is 4ecba4f1862aec144ec940b1d8a93ddabd1cb591 (trope-checker main, 2026-11-02) and design/trope-ir.schema.json is a verbatim copy of schemas/trope-ir.schema.json at that revision (explicit type annotations and a tau pass-through; the required fields are unchanged). What I ran: TROPECHECK_REQUIRED=1 TROPECHECK_BIN= bash tests/check-examples.sh -> before re-vendoring: FAIL drift guard, exit 1; after: ok x7 (three well-formed documents, schema match, three round-trips to the stated verdicts, witness e_collapse/fate.quality), exit 0. actionlint on trope-check.yml -> clean. What I did not run: the Idris2 reference-checker build the workflow performs (no Idris 2 here); the workflow run on this pull request is the attestation. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .github/workflows/trope-check.yml | 2 +- design/trope-ir.schema.json | 503 +++++++++++++++++++++++++----- 2 files changed, 423 insertions(+), 82 deletions(-) diff --git a/.github/workflows/trope-check.yml b/.github/workflows/trope-check.yml index 0343cd2..cd0cb1f 100644 --- a/.github/workflows/trope-check.yml +++ b/.github/workflows/trope-check.yml @@ -42,7 +42,7 @@ jobs: uses: actions/checkout@v7.0.1 with: repository: hyperpolymath/trope-checker - ref: 69221ad6bec0c9286cb5c917edfad281e7e0089e # main @ 2026-07-28 + ref: 4ecba4f1862aec144ec940b1d8a93ddabd1cb591 # main @ 2026-11-02 (after Phase 0 #107 and #109) path: trope-checker # The pinned idris2-pack image is minimal and ships no jq, which both the diff --git a/design/trope-ir.schema.json b/design/trope-ir.schema.json index 8c6ecb9..a589150 100644 --- a/design/trope-ir.schema.json +++ b/design/trope-ir.schema.json @@ -5,14 +5,27 @@ "$comment": "SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) . SPDX-License-Identifier: MPL-2.0 The language-neutral interchange of the trope-particularity calculus (spec/calculus.adoc). This is the canonical PREVENT profile (DEPLOY_VARIANT=prevent, R-2026-06-22): the three deceptive grade values (fate=Falsified, bond=Misbound, merge=Conflated) and the untagged merge are MALFORMED here and are rejected at validation with the offending coordinate named. The grade shape is the dependent record Sigma(fate). Bond(fate.bearer) x Merge; the if/then/else on bond makes bearer-incoherent grades unrepresentable (HC-4). The semantics (Idris2 src/) carries the COMPLETE lattices including the deceptive bottoms; the detect profile (calculus §6.1) permits them and defers the check to the verdict; it is documented in the calculus, not shipped as a separate schema here.", "description": "A labelled DAG: nodes are property-instances (field-presence + type tag), edges are effect applications carrying a loss-shape grade, and a use-model node carries the floor. The checker is a pure function from this document to a verdict.", "type": "object", - "required": ["version", "profile", "nodes", "edges", "use_model"], + "required": [ + "version", + "profile", + "nodes", + "edges", + "use_model" + ], "additionalProperties": false, "properties": { - "$schema": { "type": "string" }, - "$comment": { "type": "string" }, + "$schema": { + "type": "string" + }, + "$comment": { + "type": "string" + }, "version": { "type": "string", - "enum": ["0.1", "0.2"], + "enum": [ + "0.1", + "0.2" + ], "$comment": "0.2 is current (R-2026-07-07, ADR 0004: A1 two-sided deceptive zeros, A2 chain retention order, A3 Attenuated(0)->Present normalization at ingest — verdict semantics changed, wire format unchanged). 0.1 documents remain accepted and are normalized and graded identically under 0.2 semantics." }, "profile": { @@ -23,206 +36,534 @@ "nodes": { "type": "array", "minItems": 1, - "items": { "$ref": "#/$defs/node" } + "items": { + "$ref": "#/$defs/node" + } }, "edges": { "type": "array", - "items": { "$ref": "#/$defs/edge" } + "items": { + "$ref": "#/$defs/edge" + } }, - "use_model": { "$ref": "#/$defs/useModel" } + "use_model": { + "$ref": "#/$defs/useModel" + } }, "$defs": { - "fieldName": { "enum": ["quality", "bearer", "context", "record"] }, - + "fieldName": { + "enum": [ + "quality", + "bearer", + "context", + "record" + ] + }, "delta": { "$comment": "A fidelity element of N union {inf, top}. Finite delta is tropical (min-plus) quantified loss; inf is total quantified loss; top is loss of unknown amount. Attenuated(0) is wire-legal and is normalized to Present at IR ingest (R-2026-07-07-03, A3): validators rewrite it before grading.", "oneOf": [ - { "type": "integer", "minimum": 0 }, - { "type": "string", "enum": ["inf", "top"] } + { + "type": "integer", + "minimum": 0 + }, + { + "type": "string", + "enum": [ + "inf", + "top" + ] + } ] }, - - "fatePresent": { "type": "object", "required": ["k"], "additionalProperties": false, "properties": { "k": { "const": "Present" } } }, - "fateAttenuated": { "type": "object", "required": ["k", "delta"], "additionalProperties": false, "properties": { "k": { "const": "Attenuated" }, "delta": { "$ref": "#/$defs/delta" } } }, - "fatePredicated": { "type": "object", "required": ["k", "predicate"], "additionalProperties": false, "properties": { "k": { "const": "Predicated" }, "predicate": { "type": "string", "minLength": 1 } } }, - "fateDropped": { "type": "object", "required": ["k"], "additionalProperties": false, "properties": { "k": { "const": "Dropped" } } }, - + "fatePresent": { + "type": "object", + "required": [ + "k" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Present" + } + } + }, + "fateAttenuated": { + "type": "object", + "required": [ + "k", + "delta" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Attenuated" + }, + "delta": { + "$ref": "#/$defs/delta" + } + } + }, + "fatePredicated": { + "type": "object", + "required": [ + "k", + "predicate" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Predicated" + }, + "predicate": { + "type": "string", + "minLength": 1 + } + } + }, + "fateDropped": { + "type": "object", + "required": [ + "k" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Dropped" + } + } + }, "fateQuality": { "$comment": "Predicated is well-formed ONLY on the quality field (calculus 3.1). Falsified (deceptive) is excluded under the prevent profile.", "oneOf": [ - { "$ref": "#/$defs/fatePresent" }, - { "$ref": "#/$defs/fateAttenuated" }, - { "$ref": "#/$defs/fatePredicated" }, - { "$ref": "#/$defs/fateDropped" } + { + "$ref": "#/$defs/fatePresent" + }, + { + "$ref": "#/$defs/fateAttenuated" + }, + { + "$ref": "#/$defs/fatePredicated" + }, + { + "$ref": "#/$defs/fateDropped" + } ] }, "fateNonQuality": { "$comment": "No Predicated off the quality field; no Falsified under prevent.", "oneOf": [ - { "$ref": "#/$defs/fatePresent" }, - { "$ref": "#/$defs/fateAttenuated" }, - { "$ref": "#/$defs/fateDropped" } + { + "$ref": "#/$defs/fatePresent" + }, + { + "$ref": "#/$defs/fateAttenuated" + }, + { + "$ref": "#/$defs/fateDropped" + } ] }, - "fate": { "type": "object", - "required": ["quality", "bearer", "context", "record"], + "required": [ + "quality", + "bearer", + "context", + "record" + ], "additionalProperties": false, "properties": { - "quality": { "$ref": "#/$defs/fateQuality" }, - "bearer": { "$ref": "#/$defs/fateNonQuality" }, - "context": { "$ref": "#/$defs/fateNonQuality" }, - "record": { "$ref": "#/$defs/fateNonQuality" } + "quality": { + "$ref": "#/$defs/fateQuality" + }, + "bearer": { + "$ref": "#/$defs/fateNonQuality" + }, + "context": { + "$ref": "#/$defs/fateNonQuality" + }, + "record": { + "$ref": "#/$defs/fateNonQuality" + } } }, - "bond": { "$comment": "Intact where bearer present; Withheld/Severed where bearer absent. Misbound (deceptive, bearer present) is excluded under prevent. The Sigma-dependency is enforced by the grade-level if/then/else, not here.", "type": "object", - "required": ["k"], + "required": [ + "k" + ], "additionalProperties": false, - "properties": { "k": { "enum": ["Intact", "Withheld", "Severed"] } } + "properties": { + "k": { + "enum": [ + "Intact", + "Withheld", + "Severed" + ] + } + } }, - "merge": { "$comment": "Single, or Fused with a REQUIRED provenance tag tau (R-2026-06-22: an untagged merge does not elaborate). Conflated (deceptive) is excluded under prevent.", "oneOf": [ - { "type": "object", "required": ["k"], "additionalProperties": false, "properties": { "k": { "const": "Single" } } }, - { "type": "object", "required": ["k", "tau"], "additionalProperties": false, "properties": { "k": { "const": "Fused" }, "tau": { "type": "string", "minLength": 1 } } } + { + "type": "object", + "required": [ + "k" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Single" + } + } + }, + { + "type": "object", + "required": [ + "k", + "tau" + ], + "additionalProperties": false, + "properties": { + "k": { + "const": "Fused" + }, + "tau": { + "type": "string", + "minLength": 1 + } + } + } ] }, - "grade": { "$comment": "The dependent record Sigma(fate). Bond(fate.bearer) x Merge. HC-4: the if/then/else makes bearer-incoherent states unrepresentable.", "type": "object", - "required": ["fate", "bond", "merge"], + "required": [ + "fate", + "bond", + "merge" + ], "additionalProperties": false, "properties": { - "fate": { "$ref": "#/$defs/fate" }, - "bond": { "$ref": "#/$defs/bond" }, - "merge": { "$ref": "#/$defs/merge" } + "fate": { + "$ref": "#/$defs/fate" + }, + "bond": { + "$ref": "#/$defs/bond" + }, + "merge": { + "$ref": "#/$defs/merge" + } }, "if": { - "properties": { "fate": { "properties": { "bearer": { "properties": { "k": { "const": "Dropped" } }, "required": ["k"] } }, "required": ["bearer"] } }, - "required": ["fate"] + "type": "object", + "properties": { + "fate": { + "type": "object", + "properties": { + "bearer": { + "type": "object", + "properties": { + "k": { + "const": "Dropped" + } + }, + "required": [ + "k" + ] + } + }, + "required": [ + "bearer" + ] + } + }, + "required": [ + "fate" + ] }, "then": { + "type": "object", "$comment": "bearer absent -> bond is a clean named drop (Withheld) or a constitutive severance (Severed).", - "properties": { "bond": { "properties": { "k": { "enum": ["Withheld", "Severed"] } } } } + "properties": { + "bond": { + "type": "object", + "properties": { + "k": { + "enum": [ + "Withheld", + "Severed" + ] + } + } + } + } }, "else": { + "type": "object", "$comment": "bearer present -> the tie holds (Intact). Severed/Withheld here would be incoherent (HC-4); Misbound is the deceptive case, excluded under prevent.", - "properties": { "bond": { "properties": { "k": { "const": "Intact" } } } } + "properties": { + "bond": { + "type": "object", + "properties": { + "k": { + "const": "Intact" + } + } + } + } } }, - "node": { "type": "object", - "required": ["id", "type"], + "required": [ + "id", + "type" + ], "additionalProperties": false, "properties": { - "id": { "type": "string", "minLength": 1 }, + "id": { + "type": "string", + "minLength": 1 + }, "type": { "$comment": "Trope[S] (a property-instance over a field-presence subset), FloatingQuality (quality severed; no bearer field), or Codomain (a collapse target, e.g. Bool; a non-trope).", - "enum": ["Trope", "FloatingQuality", "Codomain"] + "enum": [ + "Trope", + "FloatingQuality", + "Codomain" + ] }, "present": { "type": "array", "uniqueItems": true, - "items": { "$ref": "#/$defs/fieldName" } + "items": { + "$ref": "#/$defs/fieldName" + } + }, + "codomain": { + "type": "string", + "minLength": 1 }, - "codomain": { "type": "string", "minLength": 1 }, - "label": { "type": "string" } + "label": { + "type": "string" + } }, "allOf": [ { - "if": { "properties": { "type": { "const": "FloatingQuality" } }, "required": ["type"] }, + "if": { + "type": "object", + "properties": { + "type": { + "const": "FloatingQuality" + } + }, + "required": [ + "type" + ] + }, "then": { + "type": "object", "$comment": "A FloatingQuality has no bearer field (the severance is structurally visible).", - "properties": { "present": { "not": { "contains": { "const": "bearer" } } } } + "properties": { + "present": { + "not": { + "type": "array", + "contains": { + "const": "bearer" + } + } + } + } } }, { - "if": { "properties": { "type": { "const": "Codomain" } }, "required": ["type"] }, - "then": { "required": ["codomain"] } + "if": { + "type": "object", + "properties": { + "type": { + "const": "Codomain" + } + }, + "required": [ + "type" + ] + }, + "then": { + "type": "object", + "required": [ + "codomain" + ], + "properties": { + "codomain": true + } + } } ] }, - "edge": { "type": "object", - "required": ["id", "effect", "inputs", "output", "grade"], + "required": [ + "id", + "effect", + "inputs", + "output", + "grade" + ], "additionalProperties": false, "properties": { - "id": { "type": "string", "minLength": 1 }, + "id": { + "type": "string", + "minLength": 1 + }, "effect": { "$comment": "The six writable effects. The deceptive trio (falsify, misbind, conflate) and any untagged merge are NOT writable (HC-3); they cannot appear as a well-formed effect here.", - "enum": ["preserve", "project", "collapse", "detach", "attenuate", "fuse"] + "enum": [ + "preserve", + "project", + "collapse", + "detach", + "attenuate", + "fuse" + ] }, "inputs": { "type": "array", - "items": { "type": "string", "minLength": 1 }, + "items": { + "type": "string", + "minLength": 1 + }, "minItems": 1, "maxItems": 2 }, - "output": { "type": "string", "minLength": 1 }, - "grade": { "$ref": "#/$defs/grade" }, - "note": { "type": "string" } + "output": { + "type": "string", + "minLength": 1 + }, + "grade": { + "$ref": "#/$defs/grade" + }, + "note": { + "type": "string" + } }, "allOf": [ { - "if": { "properties": { "effect": { "const": "fuse" } }, "required": ["effect"] }, + "if": { + "type": "object", + "properties": { + "effect": { + "const": "fuse" + } + }, + "required": [ + "effect" + ] + }, "then": { + "type": "object", "$comment": "fuse is the only two-instance writable effect; its grade must be a labelled (Fused) merge.", - "properties": { "inputs": { "minItems": 2, "maxItems": 2 }, "grade": { "properties": { "merge": { "required": ["tau"], "properties": { "k": { "const": "Fused" } } } } } } + "properties": { + "inputs": { + "type": "array", + "minItems": 2, + "maxItems": 2 + }, + "grade": { + "type": "object", + "properties": { + "merge": { + "type": "object", + "required": [ + "tau" + ], + "properties": { + "k": { + "const": "Fused" + }, + "tau": true + } + } + } + } + } }, "else": { + "type": "object", "$comment": "every other writable effect is single-instance.", - "properties": { "inputs": { "minItems": 1, "maxItems": 1 } } + "properties": { + "inputs": { + "type": "array", + "minItems": 1, + "maxItems": 1 + } + } } } ] }, - "floorFate": { "$comment": "A floor MAY be specified per field; absent fields impose no demand (calculus 5.2). A floor may not demand a deceptive value.", "type": "object", "additionalProperties": false, "minProperties": 1, "properties": { - "quality": { "$ref": "#/$defs/fateQuality" }, - "bearer": { "$ref": "#/$defs/fateNonQuality" }, - "context": { "$ref": "#/$defs/fateNonQuality" }, - "record": { "$ref": "#/$defs/fateNonQuality" } + "quality": { + "$ref": "#/$defs/fateQuality" + }, + "bearer": { + "$ref": "#/$defs/fateNonQuality" + }, + "context": { + "$ref": "#/$defs/fateNonQuality" + }, + "record": { + "$ref": "#/$defs/fateNonQuality" + } } }, - "floorGrade": { "$comment": "The minimum retained particularity the use requires. Every coordinate is OPTIONAL; an omitted coordinate imposes no demand on it.", "type": "object", "additionalProperties": false, "minProperties": 1, "properties": { - "fate": { "$ref": "#/$defs/floorFate" }, - "bond": { "$ref": "#/$defs/bond" }, - "merge": { "$ref": "#/$defs/merge" } + "fate": { + "$ref": "#/$defs/floorFate" + }, + "bond": { + "$ref": "#/$defs/bond" + }, + "merge": { + "$ref": "#/$defs/merge" + } } }, - "useModel": { "type": "object", - "required": ["output", "floor"], + "required": [ + "output", + "floor" + ], "additionalProperties": false, "properties": { - "id": { "type": "string" }, - "label": { "type": "string" }, + "id": { + "type": "string" + }, + "label": { + "type": "string" + }, "output": { "$comment": "The node whose accumulated grade is checked against the floor.", "type": "string", "minLength": 1 }, - "floor": { "$ref": "#/$defs/floorGrade" } + "floor": { + "$ref": "#/$defs/floorGrade" + } } } } From 34734ca06c73a348eaf03c19db3e1261ff470751 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:48:32 +0000 Subject: [PATCH 4/7] docs(affirmation): say what check-examples.sh checks; 2026-11-04 entry for the re-vendored schema and bumped pin What was wrong: the 2026-10-27 entry said the examples "lower to well-formed Trope IR" as if the script lowered them; it checks the hand-lowered examples/*.ir.json (review finding on #81). The snapshot also predates the checker pin bump and the schema re-vendoring in this change. What changed: the 2026-10-27 entry states what was checked and quotes the script's closing line as its wording; a 2026-11-04 entry records the run here with the fast core from trope-checker 4ecba4f (ok x7, exit 0; the drift guard failed before re-vendoring, exit 1), says the Idris2 path is NOT RUN here and that trope-check.yml is the attestation, and notes the CI/required assertion fix. :revdate: bumped. What I ran: the command recorded in the entry (see the previous commit). What I did not run: the Idris2 reference-checker path. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- AFFIRMATION.adoc | 45 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 36 insertions(+), 9 deletions(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 794cfc2..a31d922 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -2,7 +2,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-License-Identifier: CC-BY-SA-4.0 = AFFIRMATION — Haec -:revdate: 2026-10-27 +:revdate: 2026-11-04 A dated, ground-truthed honesty snapshot. This is the brief's "STATUS" for Haec: what exists, what is verified, what is deferred — stated plainly, no overclaim. @@ -34,16 +34,43 @@ and its examples lower to IR the checker accepts. == As of 2026-10-27 *Ground truth (run here, UTC 07:49, haec `e9bee39`):* -`TROPECHECK_REQUIRED=1 TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh` (the path is a placeholder for the built fast core) → the three examples -(`faithful-record`, `survey-collapse`, `station-average`) lower to well-formed Trope -IR; the vendored `design/trope-ir.schema.json` matches the canonical checker schema; -all three round-trip through the checker to the verdict each states — +`TROPECHECK_REQUIRED=1 TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh` (the path is a placeholder for the built fast core) → the three checked-in +example IR documents (`faithful-record`, `survey-collapse`, `station-average`; +lowered by hand — there is no compiler, and the script checks these documents, it +does not produce them) are well-formed Trope IR; the vendored +`design/trope-ir.schema.json` matched the canonical checker schema at that checker +revision; all three round-trip through the checker to the verdict each states — `faithful-record` `p-sufficient`, `survey-collapse` `p-insufficient` with witness -`e_collapse/fate.quality`, `station-average` `p-sufficient`. "examples: all lower to -valid Trope IR." The checker was the Rust fast core built from trope-checker -`44020f9` (`main` 216f23b plus the two Phase 0 spec/CI patches, which do not touch -`src/rust`). +`e_collapse/fate.quality`, `station-average` `p-sufficient`. The script's closing +line reads "examples: all lower to valid Trope IR" (its wording; see above). The +checker was the Rust fast core built from trope-checker `44020f9` (`main` 216f23b +plus the two Phase 0 spec/CI patches, which do not touch `src/rust`). *Still true, stated once:* no compiler, no LSP, no runtime; the O2 lowering obligations in `design/elaboration.adoc` are stated, not discharged; no proofs of our own. + +== As of 2026-11-04 + +*Ground truth (run here, haec `6b36491` plus the changes that land with this +entry):* the same command, with the fast core built from trope-checker `4ecba4f` +(`main` after Phase 0 landed there via #107, plus the decoder fixes of #109) and +`design/trope-ir.schema.json` re-vendored from that revision → ok ×7 (three +well-formed documents, schema match, three round-trips to the stated verdicts, +witness `e_collapse/fate.quality` unchanged), exit 0. Before the re-vendoring the +same run failed the drift guard ("vendored IR schema has drifted …", exit 1): the +canonical schema changed shape between `69221ad6` and `4ecba4f` (explicit `type` +annotations and a `tau` pass-through; the required fields are unchanged), which is +what the guard exists to catch. `tests/check-examples.sh` now also fails under +`TROPECHECK_REQUIRED=1` when the canonical schema is absent, so CI cannot pass +with the guard silently skipped. + +*NOT RUN here:* the Idris2 reference-checker path that +`.github/workflows/trope-check.yml` takes (no Idris 2 in this session). That +workflow, now pinned to trope-checker `4ecba4f`, is the attestation; its run on +this change is cited in the pull request. `CI / required` now asserts Idris 2 +0.8.0, the version the digest-pinned image ships (it asserted 0.7.0 and was red on +`main` from 2026-10-21; haec #83). + +*Still true, stated once:* no compiler, no LSP, no runtime; O2 obligations stated, +not discharged; no proofs of our own. From 7dec135f0489970221d3dca80fdc855f1ac057bc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:57:54 +0000 Subject: [PATCH 5/7] ci: point the standards reusable-workflow callers at metadatastician/standards@857ff09 (the repository was transferred) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: every workflow here that calls a hyperpolymath/standards reusable (.github/workflows/governance.yml .github/workflows/hypatia-scan.yml .github/workflows/mirror.yml .github/workflows/scorecard.yml .github/workflows/secret-scanner.yml ) has failed before any job was created since 2026-10-26: `hyperpolymath/standards` was transferred to `metadatastician/standards` and GitHub Actions does not follow repository redirects for `jobs..uses` (run annotation: "error parsing called workflow ... workflow was not found"). Because the ruleset's only required status check, `scan / gitleaks`, is a job of the called secret-scanner workflow, no pull request in this repository could satisfy it. The owner has already made the same move in trope-checker (#107, #110), where the scanner has been green on main since 2026-10-31, and in vocarium's own secret-scanner.yml (#48). What changed: only the `uses:` lines — each caller now names metadatastician/standards/.github/workflows/@857ff096af11451841fb10488fed1438523973a1, the commit trope-checker main uses. Every input and secret those reusables declare at that commit is optional, so the callers' with/secrets blocks are left as they were. Nothing else in the files changes. What this does NOT fix (owner-only, repository settings): the Actions policy "Allow select actions and reusable workflows" must also permit `metadatastician/standards/.github/workflows/*@*`; until it does, these runs end in a startup failure that names that policy (as vocarium's re-pointed scanner does today). The re-point is necessary either way. What I ran: actionlint -shellcheck= -pyflakes= over the changed files -> clean. What I did not run: the workflows themselves; the runs on this branch are the test, and the `scan / gitleaks` job appearing is the discriminating signal. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 2 +- .github/workflows/mirror.yml | 2 +- .github/workflows/scorecard.yml | 2 +- .github/workflows/secret-scanner.yml | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 00e89ce..61d7068 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -21,4 +21,4 @@ concurrency: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd + uses: metadatastician/standards/.github/workflows/governance-reusable.yml@857ff096af11451841fb10488fed1438523973a1 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 0b1aaa2..ba081a6 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -20,4 +20,4 @@ permissions: jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd + uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@857ff096af11451841fb10488fed1438523973a1 diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index 063ae7b..d0650d2 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -12,5 +12,5 @@ permissions: contents: read jobs: mirror: - uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd + uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@857ff096af11451841fb10488fed1438523973a1 secrets: inherit diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 581210f..89511df 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -27,4 +27,4 @@ jobs: contents: read security-events: write id-token: write - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd + uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@857ff096af11451841fb10488fed1438523973a1 diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 2efb57d..f8a6be4 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -15,5 +15,5 @@ permissions: contents: read jobs: scan: - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd + uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@857ff096af11451841fb10488fed1438523973a1 secrets: inherit From 3e6afc34bca38ac58e442b167685117d61f2e563 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 22:58:48 +0000 Subject: [PATCH 6/7] docs(affirmation): cite the CI runs for the Idris2 path and the CI/required assertion fix What changed: the 2026-11-04 entry names run 41928694567 (job examples-lower-to-valid-ir, success 2026-11-04T22:51:37Z, Idris2 reference checker built at trope-checker 4ecba4f) as the attestation for the path NOT RUN here, and records that in run 41928694928 CI/required now passes the Idris 2 0.8.0 assertion, the abi.ipkg typecheck and the Zig FFI tests and fails only in its final root-shape allowlist step (.machine_readable/ root-allow.txt, the owner-only half of #83). What I ran: nothing new locally (prose); the cited runs are CI's. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- AFFIRMATION.adoc | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index a31d922..3805619 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -65,12 +65,19 @@ what the guard exists to catch. `tests/check-examples.sh` now also fails under `TROPECHECK_REQUIRED=1` when the canonical schema is absent, so CI cannot pass with the guard silently skipped. -*NOT RUN here:* the Idris2 reference-checker path that +*NOT RUN here, attested by CI:* the Idris2 reference-checker path that `.github/workflows/trope-check.yml` takes (no Idris 2 in this session). That -workflow, now pinned to trope-checker `4ecba4f`, is the attestation; its run on -this change is cited in the pull request. `CI / required` now asserts Idris 2 -0.8.0, the version the digest-pinned image ships (it asserted 0.7.0 and was red on -`main` from 2026-10-21; haec #83). +workflow, now pinned to trope-checker `4ecba4f`, ran on this change: job +`examples-lower-to-valid-ir` of +https://github.com/hyperpolymath/haec/actions/runs/41928694567 — success, +2026-11-04T22:51:37Z (the Idris2 reference checker built at `4ecba4f` gives the +same three verdicts and witness). `CI / required` now asserts Idris 2 0.8.0, the +version the digest-pinned image ships (it asserted 0.7.0 and was red on `main` +from 2026-10-21; haec #83): in run 41928694928 the Idris step passes +(`idris2 --version -> Idris 2, version 0.8.0-6ca00e72e`, `abi.ipkg` typechecks, +the Zig FFI tests pass) and the job then fails in its last step on the +root-shape allowlist (`.machine_readable/root-allow.txt`, the owner-only half +of #83), so that check stays red for a reason this entry does not claim to fix. *Still true, stated once:* no compiler, no LSP, no runtime; O2 obligations stated, not discharged; no proofs of our own. From f7a99d0076e3fd3887e2e1e406dc6e4f02f746db Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 23:38:17 +0000 Subject: [PATCH 7/7] ci: pass the mirror secrets explicitly and drop the scanner's secret inheritance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The two callers re-pointed in 3e6afc3 still said `secrets: inherit`. The reusables they now call declare the opposite contract at 857ff09: mirror-reusable.yml declares ten named optional secrets (GITLAB_SSH_KEY … R2_AGE_RECIPIENT) and says in its header not to use inherit; secret-scanner-reusable.yml declares no workflow_call.secrets, references no secrets.* context, and says the caller passes no secrets line. The callers now match that contract, which is also the shape of trope-checker's callers on main, where the scanner has been green since 2026-10-31 at the same pin. Evidence: zizmor secrets-inherit on both lines (CodeRabbit on hermeneia #80 and workbench #78); SonarCloud's "C Security Rating on New Code" cleared on workbench #78 at fe3f743 after the identical change and is the failing condition here. actionlint -shellcheck= -pyflakes= on both files: clean. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- .github/workflows/mirror.yml | 12 +++++++++++- .github/workflows/secret-scanner.yml | 1 - 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index d0650d2..72d3508 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -13,4 +13,14 @@ permissions: jobs: mirror: uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@857ff096af11451841fb10488fed1438523973a1 - secrets: inherit + secrets: + GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }} + BITBUCKET_SSH_KEY: ${{ secrets.BITBUCKET_SSH_KEY }} + CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }} + SOURCEHUT_SSH_KEY: ${{ secrets.SOURCEHUT_SSH_KEY }} + DISROOT_SSH_KEY: ${{ secrets.DISROOT_SSH_KEY }} + GITEA_SSH_KEY: ${{ secrets.GITEA_SSH_KEY }} + RADICLE_KEY: ${{ secrets.RADICLE_KEY }} + R2_ACCESS_KEY_ID: ${{ secrets.R2_ACCESS_KEY_ID }} + R2_SECRET_ACCESS_KEY: ${{ secrets.R2_SECRET_ACCESS_KEY }} + R2_AGE_RECIPIENT: ${{ secrets.R2_AGE_RECIPIENT }} diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index f8a6be4..fece7d3 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -16,4 +16,3 @@ permissions: jobs: scan: uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@857ff096af11451841fb10488fed1438523973a1 - secrets: inherit