chore(licence): normalise to MPL-2.0 + CC-BY-SA-4.0 (canonical pair) #41
Workflow file for this run
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
| # SPDX-License-Identifier: MPL-2.0 | |
| # Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | |
| # | |
| # Coq Build Oracle — compiles formal/ and asserts no axiom slippage. | |
| # | |
| # Uses Ubuntu + apt-installed Coq rather than the coqorg/coq container | |
| # image. Rationale: coqorg/coq runs as user `coq` with opam-loaded PATH; | |
| # running it as root (the standard EACCES workaround for actions/checkout) | |
| # breaks coqc lookup because root has no opam env. Apt-installed Coq is | |
| # simpler and the proofs here don't require a specific 8.x patch level. | |
| name: Coq Build Oracle | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'formal/**' | |
| - '.github/workflows/coq-build.yml' | |
| pull_request: | |
| paths: | |
| - 'formal/**' | |
| - '.github/workflows/coq-build.yml' | |
| permissions: | |
| contents: read | |
| jobs: | |
| build: | |
| name: Compile Coq proofs + assumptions guard | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 60 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| - name: Install Coq | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update | |
| sudo apt-get install -y --no-install-recommends coq | |
| - name: Coq toolchain provenance | |
| run: coqc --version | |
| - name: Compile Provenance.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Provenance.v | tee Provenance.out | |
| - name: Compile Drift.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Drift.v | tee Drift.out | |
| - name: Compile Transaction.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Transaction.v | tee Transaction.out | |
| - name: Compile Planner.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Planner.v | tee Planner.out | |
| - name: Compile WAL.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q WAL.v | tee WAL.out | |
| - name: Compile Normalizer.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Normalizer.v | tee Normalizer.out | |
| - name: Compile VCL.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q VCL.v | tee VCL.out | |
| - name: Compile PlannerSemantic.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q PlannerSemantic.v | tee PlannerSemantic.out | |
| - name: Compile Octad.v | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| coqc -q Octad.v | tee Octad.out | |
| - name: Verify Provenance assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # Whitelist: 4 Parameters + 1 declared Axiom | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \ | |
| | sort -u \ | |
| | grep -vE '^(content|hash|sha256|genesis_hash|sha256_collision_resistant)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Provenance): unexpected axiom(s) in Print Assumptions:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat Provenance.out | |
| exit 1 | |
| fi | |
| echo "OK(Provenance): 3 theorems x 4 Parameters whitelisted" | |
| - name: Verify Drift assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # D1 whitelist: 5 ordering Parameters + 3 ordering axioms + 9 f_*_drift | |
| # D2 whitelist additions: f_detect_drift, strictly_greater, le_or_gt, | |
| # le_gt_exclusive, detector_iff_threshold | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Drift.out \ | |
| | sort -u \ | |
| | grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad|f_detect_drift|strictly_greater|le_or_gt|le_gt_exclusive|detector_iff_threshold)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Drift): unexpected axiom(s) in Print Assumptions:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat Drift.out | |
| exit 1 | |
| fi | |
| echo "OK(Drift): D1 (9 fns) + D2 (detector iff threshold) whitelisted" | |
| - name: Verify Transaction assumptions (must be empty) | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # Transaction.v has zero Parameters/Axioms — every theorem must | |
| # close under the global context. | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Transaction.out \ | |
| | sort -u || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Transaction): expected 0 axioms, found:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat Transaction.out | |
| exit 1 | |
| fi | |
| echo "OK(Transaction): 3 theorems closed under global context (0 axioms)" | |
| - name: Verify Planner assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # Whitelist: modality, condition, optimize, optimize_is_permutation | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Planner.out \ | |
| | sort -u \ | |
| | grep -vE '^(modality|condition|optimize|optimize_is_permutation)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Planner): unexpected axiom(s) in Print Assumptions:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat Planner.out | |
| exit 1 | |
| fi | |
| echo "OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted" | |
| - name: Verify WAL assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # Whitelist: entity_id, data, eq_entity_dec, functional_extensionality_dep | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' WAL.out \ | |
| | sort -u \ | |
| | grep -vE '^(entity_id|data|eq_entity_dec|functional_extensionality_dep)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(WAL): unexpected axiom(s) in Print Assumptions:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat WAL.out | |
| exit 1 | |
| fi | |
| echo "OK(WAL): C7 replay-idempotent + deterministic-off-touched" | |
| - name: Verify Normalizer assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Normalizer.out \ | |
| | sort -u \ | |
| | grep -vE '^(modality|modality_data|drifted|winner|winner_excludes_drifted|winner_stable_off_drifted|functional_extensionality_dep)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Normalizer): unexpected axiom(s):" | |
| echo "$UNEXPECTED" | |
| cat Normalizer.out | |
| exit 1 | |
| fi | |
| echo "OK(Normalizer): N2 idempotent + fills-drifted-when-winner" | |
| - name: Verify VCL assumptions (must be empty) | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' VCL.out \ | |
| | sort -u || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(VCL): expected 0 axioms, found:" | |
| echo "$UNEXPECTED" | |
| cat VCL.out | |
| exit 1 | |
| fi | |
| echo "OK(VCL): V2 preservation + progress (0 axioms)" | |
| - name: Verify PlannerSemantic assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' PlannerSemantic.out \ | |
| | sort -u \ | |
| | grep -vE '^(modality|condition|octad|exec_node|exec_node_comm|optimize|optimize_is_permutation)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(PlannerSemantic): unexpected axiom(s):" | |
| echo "$UNEXPECTED" | |
| cat PlannerSemantic.out | |
| exit 1 | |
| fi | |
| echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership" | |
| - name: Verify Octad assumptions whitelist | |
| working-directory: formal | |
| run: | | |
| set -euo pipefail | |
| # Whitelist: 2 Parameters (mval, ident) + functional_extensionality_dep | |
| # (Coq stdlib). modality is inductive; resolve is an operation | |
| # argument — neither is an axiom. | |
| UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \ | |
| | sort -u \ | |
| | grep -vE '^(mval|ident|functional_extensionality_dep)$' || true) | |
| if [ -n "$UNEXPECTED" ]; then | |
| echo "ERROR(Octad): unexpected axiom(s) in Print Assumptions:" | |
| echo "$UNEXPECTED" | |
| echo "---" | |
| cat Octad.out | |
| exit 1 | |
| fi | |
| echo "OK(Octad): O-series + R1-R3 modality algebra whitelisted" |