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
11 changes: 11 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -1,10 +1,21 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# build.yml — SonarQube analysis on pushes to main and on PRs.
# The top-level permissions block is required by the estate workflow
# security linter (standards governance-reusable: SPDX headers + permissions).
name: Build

on:
push:
branches:
- main
pull_request:
types: [opened, synchronize, reopened]

permissions:
contents: read

jobs:
sonarqube:
name: SonarQube
Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/dogfood-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ jobs:
else
echo "## DEED Manifest Validation" >> "$GITHUB_STEP_SUMMARY"
echo "" >> "$GITHUB_STEP_SUMMARY"
echo "Scanned **${A2ML_COUNT}** manifest file(s) (.deed, or legacy .a2ml). See step output for details." >> "$GITHUB_STEP_SUMMARY"
echo "Scanned **${MANIFEST_COUNT}** manifest file(s) (.deed, or legacy .a2ml). See step output for details." >> "$GITHUB_STEP_SUMMARY"
fi

# ---------------------------------------------------------------------------
Expand Down Expand Up @@ -100,7 +100,7 @@ jobs:
cat <<'EOF' >> "$GITHUB_STEP_SUMMARY"
## K9 Contract Validation

:warning: **No .a2ml/.deed manifest files found.** Every RSR-compliant repo should have a repo deed (`<reponame>_chora.deed`) at its root.
:warning: **No K9 contract files found.** Every RSR repo with config files should carry K9 contracts.

Generate contracts with: `k9iser generate .`
EOF
Expand Down Expand Up @@ -396,7 +396,7 @@ jobs:

| Tool/Format | Status | Notes |
|-------------|--------|-------|
| DEED repo deed (`<reponame>_chora.deed`) | ${A2ML_STATUS} | Required for all RSR repos |
| DEED repo deed (`<reponame>_chora.deed`) | ${DEED_STATUS} | Required for all RSR repos |
| K9 contracts | ${K9_STATUS} | Required for repos with config files |
| .editorconfig | ${EC_STATUS} | Required for all repos |
| Groove endpoint | ${GROOVE_STATUS} | Required for service repos |
Expand Down
3 changes: 3 additions & 0 deletions tests/idris2/depends.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@
# yields exit 2 (VOID), and VOID propagates: a battery must reclassify any
# green downstream of this unit's VOID as VOID.

name = "aerie-idris2-depends"
version = "1.0.0"

[upstream_units]
value = "none — self-contained model suite; mirrors src/api/zig/{proof,policy}.zig invariants"

Expand Down
3 changes: 3 additions & 0 deletions tests/idris2/diagnosticity.a2ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
# SPDX-License-Identifier: MPL-2.0
# Diagnosticity contract for the aerie model suite (tests/idris2).

name = "aerie-idris2-diagnosticity"
version = "1.0.0"

[detects]
condition = "divergence between the aerie specification models (proof envelope well-formedness, policy-gate monotonicity, longest-prefix route matching) and their stated invariants"
defect_class = "spec-model-drift"
Expand Down