# SPDX-License-Identifier: PMPL-1.0-or-later
# Mustfile — Physical state contract for anvomidaviser
# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

@abstract:
What MUST be true about this repository's files and configuration.
These are hard requirements — CI fails if any check fails.
@end

## File Presence

### license-present
- description: LICENSE file must exist
- run: test -f LICENSE
- severity: critical

### readme-present
- description: README.adoc or README.md must exist
- run: test -f README.adoc || test -f README.md
- severity: critical

### security-policy
- description: SECURITY.md must exist
- run: test -f SECURITY.md
- severity: critical

### ai-manifest
- description: 0-AI-MANIFEST.a2ml must exist
- run: test -f 0-AI-MANIFEST.a2ml
- severity: critical

### contributing
- description: CONTRIBUTING.adoc must exist
- run: test -f CONTRIBUTING.adoc || test -f CONTRIBUTING.md
- severity: warning

### editorconfig
- description: .editorconfig must exist
- run: test -f .editorconfig
- severity: warning

### cargo-builds
- description: Project must compile
- run: cargo check 2>&1 | tail -1
- severity: critical

### tests-pass
- description: All tests must pass
- run: cargo test
- severity: critical

## SPDX Compliance

### spdx-headers
- description: All source files must have SPDX-License-Identifier
- run: "! find src/ -name '*.rs' 2>/dev/null | head -20 | xargs grep -L 'SPDX-License-Identifier' 2>/dev/null | head -1 | grep -q ."
- severity: warning

### no-agpl
- description: No AGPL-3.0 references (superseded by PMPL)
- run: "! grep -r 'AGPL-3.0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q ."
- severity: critical

## Dangerous Patterns

### no-believe-me
- description: No believe_me in Idris2 code
- run: "! grep -r 'believe_me' --include='*.idr' . 2>/dev/null | grep -v node_modules | head -1 | grep -q ."
- severity: critical

### no-unsafe-coerce
- description: No unsafeCoerce in source
- run: "! grep -r 'unsafeCoerce\|unsafe_coerce' --include='*.rs' --include='*.idr' . 2>/dev/null | head -1 | grep -q ."
- severity: critical

### no-sorry
- description: No sorry/Admitted escape hatches
- run: "! grep -r 'sorry\|Admitted\|assert_total' --include='*.idr' --include='*.lean' --include='*.v' . 2>/dev/null | grep -v node_modules | head -1 | grep -q ."
- severity: critical

## Project-Specific Constraints (anvomidaviser)

### isu-scoring-types
- description: ISU scoring ABI types defined
- run: grep -q 'BaseValue\|GOE\|PCS\|TES' src/abi/ -r
- severity: critical

### element-code-parser
- description: Element code parsing module exists
- run: test -d src/core/ && grep -rq 'element\|jump\|spin' src/core/ src/codegen/
- severity: warning
