Skip to content
Closed
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
34 changes: 15 additions & 19 deletions .github/workflows/coq-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -94,18 +94,13 @@ jobs:
echo "⚠️ INV-1 proof file missing — warn only (non-critical path)"
fi

- name: Validate assertions/igla_assertions.json
- name: Run trios-phd tests (audit + cite)
run: |
python3 -c "
import json, sys
with open('assertions/igla_assertions.json') as f:
data = json.load(f)
assert len(data['invariants']) == 5, 'Expected 5 invariants'
for inv in data['invariants']:
assert 'id' in inv and 'status' in inv
assert inv['status'] in ('Proven', 'Admitted'), f'Invalid status: {inv[\"status\"]}'
print('✅ igla_assertions.json valid:', len(data[\"invariants\"]), 'invariants')
"
cargo test -p trios-phd --no-fail-fast

- name: Run trios-phd audit (validates assertions/igla_assertions.json + PhD bridge)
run: |
cargo run -p trios-phd -- --repo . audit

- name: Run Rust invariant tests
run: |
Expand All @@ -115,12 +110,13 @@ print('✅ igla_assertions.json valid:', len(data[\"invariants\"]), 'invariants'
if: always()
run: |
echo "## 🧮 Coq Invariant Gate — L-R14" >> $GITHUB_STEP_SUMMARY
echo "| Invariant | Theorem | Status |" >> $GITHUB_STEP_SUMMARY
echo "|-----------|---------|--------|" >> $GITHUB_STEP_SUMMARY
echo "| INV-1 | bpb_decreases_with_real_gradient | Admitted |" >> $GITHUB_STEP_SUMMARY
echo "| INV-2 | asha_champion_survives | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-3 | gf16_safe_domain | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-4 | nca_entropy_stability | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-5 | lucas_closure_gf16 | Proven (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| Invariant | Coq file | Status |" >> $GITHUB_STEP_SUMMARY
echo "|-----------|----------|--------|" >> $GITHUB_STEP_SUMMARY
echo "| INV-1 | lr_phi_optimality.v | Admitted |" >> $GITHUB_STEP_SUMMARY
echo "| INV-2 | igla_asha_bound.v | Proven (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-3 | gf16_precision.v | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-4 | nca_entropy_band.v | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-5 | lucas_closure_gf16.v | Admitted (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "| INV-12 | igla_asha_bound.v | Proven (BLOCKING) |" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo "φ² + φ⁻² = 3 | TRINITY | IGLA RACE v2" >> $GITHUB_STEP_SUMMARY
echo "φ² + φ⁻² = 3 | TRINITY | IGLA RACE v2 | trios-phd audit" >> $GITHUB_STEP_SUMMARY
20 changes: 10 additions & 10 deletions .github/workflows/laws-guard.yml
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ jobs:

- name: Check schema version
run: |
if ! grep -q "LAWS_SCHEMA_VERSION: 2.0" LAWS.md; then
if ! grep -qE "LAWS_SCHEMA_VERSION:?\*?\*? 2\.0" LAWS.md; then
echo "❌ BREACH: LAWS_SCHEMA_VERSION missing or not 2.0"
exit 1
fi
Expand All @@ -50,7 +50,7 @@ jobs:
fi
echo "✅ All 13 sections present"

- name: L1: No .sh files
- name: "L1: No .sh files"
run: |
COUNT=$(find . -name "*.sh" ! -path "*/node_modules/*" ! -path "*/.git/*" ! -path "*/target/*" | wc -l)
if [ "$COUNT" -gt 0 ]; then
Expand All @@ -60,7 +60,7 @@ jobs:
fi
echo "✅ L1: No .sh files"

- name: L2: PR closes issue (PR only)
- name: "L2: PR closes issue (PR only)"
if: github.event_name == 'pull_request'
run: |
if ! echo "${{ github.event.pull_request.body }}" | grep -iE "(Closes|Fixes|Resolves) #[0-9]+"; then
Expand All @@ -70,7 +70,7 @@ jobs:
fi
echo "✅ L2: PR closes an issue"

- name: I5: No /extension root directory
- name: "I5: No /extension root directory"
run: |
if [ -d "./extension" ]; then
echo "❌ I5 VIOLATION: /extension root directory exists"
Expand Down Expand Up @@ -107,30 +107,30 @@ jobs:
- name: Cache cargo
uses: Swatinem/rust-cache@v2

- name: I1: cargo build
- name: "I1: cargo build"
run: |
cargo build --all --workspace
echo "✅ I1: Build passes"

- name: I2: cargo test
- name: "I2: cargo test"
run: |
cargo test --all --workspace
echo "✅ I2: Tests pass"

- name: I3: clippy
- name: "I3: clippy"
run: |
cargo clippy --all-targets --all-features -- -D warnings
echo "✅ I3: Clippy clean"

- name: I4: Docs exist
- name: "I4: Docs exist"
run: |
if [ ! -f README.md ]; then
echo "❌ I4 VIOLATION: README.md missing"
exit 1
fi
echo "✅ I4: README.md exists"

- name: I7: No wasm-unsafe-eval in manifest
- name: "I7: No wasm-unsafe-eval in manifest"
run: |
MANIFEST_FILE="crates/trios-ext/extension/manifest.json"
if [ -f "$MANIFEST_FILE" ]; then
Expand All @@ -141,7 +141,7 @@ jobs:
fi
echo "✅ I7: wasm-unsafe-eval check passed"

- name: I9: Experience current
- name: "I9: Experience current"
run: |
TODAY=$(date +%Y%m%d)
EXPERIENCE_FILE=".trinity/experience/trios_${TODAY}.trinity"
Expand Down
2 changes: 1 addition & 1 deletion .trinity/state/LAWS_HASH
Original file line number Diff line number Diff line change
@@ -1 +1 @@
cba380ba9796774b9ab9934f3f4071fe8cf6f0c3c2ea81ab548c210efac80ade /Users/playra/trios/LAWS.md
cba380ba9796774b9ab9934f3f4071fe8cf6f0c3c2ea81ab548c210efac80ade LAWS.md
Loading
Loading