Prove MicroInterp DFA coupling and re-gate abandoned CI smokes by fraware · Pull Request #215 · SentinelOps-CI/provability-fabric

fraware · 2026-07-18T04:59:09Z

Summary

F33 / P4: implement compileClauses + semanticsFromClauses, prove dfa_semantics_match (sorry 2→0), add lake build Runtime
Re-gate 8 leftovers with honest CI smokes (local mock / dry-run / secret-skip) instead of leaving them dispatch-only
Update lean-sorry burn-down + remediation tracker; do not claim 67/67

Workflows

Workflow	Re-gate mode
art-benchmark	deterministic Python smoke
lean-offline	Runtime build + scoped sorry scan (full mathlib offline stays dispatch)
dr-cross	push/schedule; skip when AWS secrets absent
edge-load / loadtest / perf-proofmeter	local mock + tiny k6/bench
publish-updates / revocation-sync	dry-run validation (no external registry/PR)

Test plan

lake build Runtime (local)
python scripts/art_runner.py --smoke
go build proofmeter_bench
PR CI green on new smoke workflows
Inventory after merge (expect higher gated count; exit 0 once tip runs succeed)

Close F33 P4 by landing compileClauses/semanticsFromClauses with a proved dfa_semantics_match (0 sorry) and a Runtime lake target. Revive the eight previously dispatch-only workflows with CI-sized smokes or secret-skip paths instead of further ungating; keep full SaaS/AWS modes dispatch-only.

cursor · 2026-07-18T04:59:13Z

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

github-actions · 2026-07-18T04:59:33Z

Thanks for the PR! CI will run CERT validation and replay checks. Results will appear in workflow badges and artifacts.

… smoke Lake requires vendor/mathlib which is absent on fresh runners; MicroInterp has no imports so lean can typecheck it directly when the vendor tree is missing.

github-actions · 2026-07-18T05:01:55Z

SBOM Security Report

Total Packages: 4528

Language Distribution:

go: 359
javascript: 3277
rust: 592
python: 1

License Distribution:

MIT: 1270
Apache-2.0: 45
CC0-1.0: 43
BSD-3-Clause: 34
ISC: 87
BSD-2-Clause: 41
Python-2.0: 2
MPL-2.0: 1
Unlicense: 5
CC-BY-4.0: 1
(Apache-2.0 OR MPL-1.1): 1
BlueOak-1.0.0: 3
(AFL-2.1 OR BSD-3-Clause): 2
(BSD-3-Clause OR GPL-2.0): 1
0BSD: 3
(MIT OR CC0-1.0): 4
MIT AND ISC: 1

✅ SBOM generated successfully
✅ No GPL licenses detected
✅ No high/critical vulnerabilities found

github-actions · 2026-07-18T05:05:22Z

Sample Replay

low_view %: N/A
status: unknown
Counterexample Explorer: https://console.localhost/replay/last

github-actions · 2026-07-18T05:05:39Z

Sample Replay

low_view %: N/A
status: unknown
Counterexample Explorer: https://console.localhost/replay/last

github-actions · 2026-07-18T05:06:46Z

Thanks for the PR! CI will run CERT validation and replay checks. Results will appear in workflow badges and artifacts.

github-actions · 2026-07-18T05:07:01Z

SBOM Security Report

Total Packages: 4528

Language Distribution:

go: 359
javascript: 3277
rust: 592
python: 1

License Distribution:

MIT: 1270
Apache-2.0: 45
CC0-1.0: 43
BSD-3-Clause: 34
ISC: 87
BSD-2-Clause: 41
Python-2.0: 2
MPL-2.0: 1
Unlicense: 5
CC-BY-4.0: 1
(Apache-2.0 OR MPL-1.1): 1
BlueOak-1.0.0: 3
(AFL-2.1 OR BSD-3-Clause): 2
(BSD-3-Clause OR GPL-2.0): 1
0BSD: 3
(MIT OR CC0-1.0): 4
MIT AND ISC: 1

✅ SBOM generated successfully
✅ No GPL licenses detected
✅ No high/critical vulnerabilities found

github-actions · 2026-07-18T05:08:48Z

Policy Coverage Report

Tools Coverage: 100%
Events Coverage: 100%
Egress Labeled: 100%
Replay Determinism: 100%

All policy gates passed successfully!

github-actions · 2026-07-18T05:09:15Z

Policy Coverage Report

Tools Coverage: 100%
Events Coverage: 100%
Egress Labeled: 100%
Replay Determinism: 100%

All policy gates passed successfully!

Clear unjustified soft-fail patterns in lean-offline sorry scan and loadtest full-mode teardown so CI required checks can pass.

github-actions · 2026-07-18T05:14:16Z

Thanks for the PR! CI will run CERT validation and replay checks. Results will appear in workflow badges and artifacts.

Skip elan install when the pinned toolchain is already present from cache.

github-actions · 2026-07-18T05:17:20Z

Sample Replay

low_view %: N/A
status: unknown
Counterexample Explorer: https://console.localhost/replay/last

github-actions · 2026-07-18T05:17:26Z

Thanks for the PR! CI will run CERT validation and replay checks. Results will appear in workflow badges and artifacts.

github-actions · 2026-07-18T05:19:00Z

Sample Replay

low_view %: N/A
status: unknown
Counterexample Explorer: https://console.localhost/replay/last

github-actions · 2026-07-18T05:21:10Z

SBOM Security Report

Total Packages: 4528

Language Distribution:

go: 359
javascript: 3277
rust: 592
python: 1

License Distribution:

MIT: 1270
Apache-2.0: 45
CC0-1.0: 43
BSD-3-Clause: 34
ISC: 87
BSD-2-Clause: 41
Python-2.0: 2
MPL-2.0: 1
Unlicense: 5
CC-BY-4.0: 1
(Apache-2.0 OR MPL-1.1): 1
BlueOak-1.0.0: 3
(AFL-2.1 OR BSD-3-Clause): 2
(BSD-3-Clause OR GPL-2.0): 1
0BSD: 3
(MIT OR CC0-1.0): 4
MIT AND ISC: 1

✅ SBOM generated successfully
✅ No GPL licenses detected
✅ No high/critical vulnerabilities found

github-actions · 2026-07-18T05:23:46Z

SBOM Security Report

Total Packages: 4528

Language Distribution:

go: 359
javascript: 3277
rust: 592
python: 1

License Distribution:

MIT: 1270
Apache-2.0: 45
CC0-1.0: 43
BSD-3-Clause: 34
ISC: 87
BSD-2-Clause: 41
Python-2.0: 2
MPL-2.0: 1
Unlicense: 5
CC-BY-4.0: 1
(Apache-2.0 OR MPL-1.1): 1
BlueOak-1.0.0: 3
(AFL-2.1 OR BSD-3-Clause): 2
(BSD-3-Clause OR GPL-2.0): 1
0BSD: 3
(MIT OR CC0-1.0): 4
MIT AND ISC: 1

✅ SBOM generated successfully
✅ No GPL licenses detected
✅ No high/critical vulnerabilities found

github-actions · 2026-07-18T05:23:53Z

Policy Coverage Report

Tools Coverage: 100%
Events Coverage: 100%
Egress Labeled: 100%
Replay Determinism: 100%

All policy gates passed successfully!

github-actions · 2026-07-18T05:24:53Z

Policy Coverage Report

Tools Coverage: 100%
Events Coverage: 100%
Egress Labeled: 100%
Replay Determinism: 100%

All policy gates passed successfully!

fix(ci): compile MicroInterp without vendored mathlib in lean-offline…

75e0ea5

… smoke Lake requires vendor/mathlib which is absent on fresh runners; MicroInterp has no imports so lean can typecheck it directly when the vendor tree is missing.

fix(ci): justify remaining || true for ci-honesty on wave8 smokes

4f3bd4d

Clear unjustified soft-fail patterns in lean-offline sorry scan and loadtest full-mode teardown so CI required checks can pass.

fix(ci): tolerate cached elan toolchain in lean-offline smoke

3ad096f

Skip elan install when the pinned toolchain is already present from cache.

fraware merged commit ad4fafd into main Jul 18, 2026
93 of 94 checks passed

fraware deleted the wave8/f33-and-ci-revive branch July 18, 2026 05:27

fraware mentioned this pull request Jul 18, 2026

fix(ci): pin k6 to clear platform-perf-smoke tip red #216

Merged

3 tasks

Uh oh!

Conversation

fraware commented Jul 18, 2026

Summary

Workflows

Test plan

Uh oh!

cursor Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

SBOM Security Report

Language Distribution:

License Distribution:

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

SBOM Security Report

Language Distribution:

License Distribution:

Uh oh!

github-actions Bot commented Jul 18, 2026

Policy Coverage Report

Uh oh!

github-actions Bot commented Jul 18, 2026

Policy Coverage Report

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

Uh oh!

github-actions Bot commented Jul 18, 2026

SBOM Security Report

Language Distribution:

License Distribution:

Uh oh!

github-actions Bot commented Jul 18, 2026

SBOM Security Report

Language Distribution:

License Distribution:

Uh oh!

github-actions Bot commented Jul 18, 2026

Policy Coverage Report

Uh oh!

github-actions Bot commented Jul 18, 2026

Policy Coverage Report

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant