|
1 | 1 | # SPDX-License-Identifier: PMPL-1.0-or-later |
2 | | -# Mustfile - declarative state contract (template) |
| 2 | +# Mustfile - declarative state contract for BoJ Server |
3 | 3 | # See: https://github.com/hyperpolymath/mustfile |
4 | 4 |
|
5 | 5 | version: 1 |
6 | 6 |
|
7 | 7 | metadata: |
8 | | - name: project-state-contract |
9 | | - spec: v0.0.1 |
10 | | - description: "Invariant checks for config, policy, gateway, logs, and schema." |
| 8 | + name: boj-server-state-contract |
| 9 | + spec: v0.1.0 |
| 10 | + description: "Invariant checks for BoJ capability catalogue, cartridges, and formal proofs." |
11 | 11 |
|
12 | 12 | parameters: |
13 | | - gateway_port: "8080" |
14 | | - schema_version: "v0.0.1" |
| 13 | + gateway_port: "9000" |
| 14 | + abi_dir: "src/abi" |
| 15 | + ffi_dir: "ffi/zig" |
15 | 16 |
|
16 | 17 | checks: |
17 | | - - name: config-valid |
18 | | - description: "config/service.yaml must be valid." |
19 | | - run: "yq -e '.' config/service.yaml >/dev/null" |
| 18 | + - name: zero-believe-me |
| 19 | + description: "No believe_me, assert_total, or assert_smaller in any Idris2 source." |
| 20 | + run: "bash -uc '! grep -rn \"believe_me\\|assert_total\\|assert_smaller\" --include=\"*.idr\" src/ cartridges/ | grep -v -- \"--.*believe_me\" | grep -v \"|||.*believe_me\"'" |
20 | 21 |
|
21 | | - - name: policy-compiles |
22 | | - description: "policy/policy.ncl must compile." |
23 | | - run: "nickel check policy/policy.ncl" |
| 22 | + - name: abi-typechecks |
| 23 | + description: "Core ABI Idris2 files must type-check with %default total." |
| 24 | + run: "cd src/abi && idris2 --check --package boj boj.ipkg" |
24 | 25 |
|
25 | | - - name: gateway-exposes-port |
26 | | - description: "Service must expose the configured port." |
27 | | - run: "bash -uc 'ss -lnt | rg \":${GATEWAY_PORT:-8080}\"'" |
| 26 | + - name: ffi-builds |
| 27 | + description: "Core FFI Zig layer must compile clean." |
| 28 | + run: "cd ffi/zig && zig build" |
28 | 29 |
|
29 | | - - name: logs-are-json |
30 | | - description: "Logs must be JSON." |
31 | | - run: "bash -uc 'rg --files -g \"*.json\" logs | xargs -r jq -e .'" |
| 30 | + - name: ffi-tests-pass |
| 31 | + description: "Core FFI tests must pass." |
| 32 | + run: "cd ffi/zig && zig build test" |
32 | 33 |
|
33 | | - - name: schema-version-matches |
34 | | - description: "Schema must match version spec." |
35 | | - run: "bash -uc 'rg -n \"${SCHEMA_VERSION:-v0.0.1}\" schema'" |
| 34 | + - name: cartridge-fleet-abi |
| 35 | + description: "Fleet-MCP ABI must type-check." |
| 36 | + run: "cd cartridges/fleet-mcp/abi && idris2 --check fleet-mcp.ipkg" |
| 37 | + |
| 38 | + - name: cartridge-nesy-abi |
| 39 | + description: "NeSy-MCP ABI must type-check." |
| 40 | + run: "cd cartridges/nesy-mcp/abi && idris2 --check nesy-mcp.ipkg" |
| 41 | + |
| 42 | + - name: cartridge-database-abi |
| 43 | + description: "Database-MCP ABI must type-check." |
| 44 | + run: "cd cartridges/database-mcp/abi && idris2 --check database-mcp.ipkg" |
| 45 | + |
| 46 | + - name: cartridge-agent-abi |
| 47 | + description: "Agent-MCP ABI must type-check." |
| 48 | + run: "cd cartridges/agent-mcp/abi && idris2 --check agent-mcp.ipkg" |
| 49 | + |
| 50 | + - name: cartridge-ffi-tests |
| 51 | + description: "All cartridge FFI tests must pass." |
| 52 | + run: | |
| 53 | + cd cartridges/fleet-mcp/ffi && zig build test && |
| 54 | + cd ../../nesy-mcp/ffi && zig build test && |
| 55 | + cd ../../database-mcp/ffi && zig build test && |
| 56 | + cd ../../agent-mcp/ffi && zig build test |
| 57 | + |
| 58 | + - name: spdx-headers |
| 59 | + description: "All source files must have PMPL-1.0-or-later SPDX headers." |
| 60 | + run: "bash -uc 'find src/ ffi/ cartridges/ -name \"*.idr\" -o -name \"*.zig\" | xargs grep -L \"PMPL-1.0-or-later\" | head -5 | { read line && echo \"Missing SPDX: $line\" && exit 1 || true; }'" |
| 61 | + |
| 62 | + - name: menu-exists |
| 63 | + description: "A2ML menu must exist." |
| 64 | + run: "test -f .machine_readable/servers/menu.a2ml" |
| 65 | + |
| 66 | + - name: order-ticket-exists |
| 67 | + description: "Order-ticket protocol spec must exist." |
| 68 | + run: "test -f .machine_readable/servers/order-ticket.scm" |
0 commit comments