chore(ci): fold manual model checking into formal verify #1778
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
❓ Code Generation Drift DetectionStatus: Automated by AE-Framework Codegen |
Collaborator
Author
Auto Update BranchPR #1778 was behind base; triggered branch update. |
Contributor
❓ Code Generation Drift DetectionStatus: Automated by AE-Framework Codegen |
Contributor
Quality Summary
|
Contributor
🔍 Verification Summary
Unlinked (top 5)- Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/ALinked examples (up to 3)- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/2a7181509909a60d20d28faae18567b51ca3eeb3/specs/formal/tla+/Inventory.tla)Hit basis (tests/formal)- Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0Non-OK modules (top 5)- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) |
Contributor
CodeX Artifacts Summary
|
27 tasks
Contributor
There was a problem hiding this comment.
Pull request overview
This PR consolidates the manual model-checking workflow into the existing formal-verify GitHub Actions workflow, reducing workflow count and updating the Issue #1006 workflow inventory/docs accordingly.
Changes:
- Fold
model-checking-manualfunctionality intoformal-verify.yml’sworkflow_dispatch(incl. selectable TLA file usage). - Adjust
workflow_dispatchconcurrency grouping to account for additional inputs. - Remove
model-checking-manual.ymland update Issue #1006 workflow trigger/inventory documentation.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
.github/workflows/formal-verify.yml |
Adds dispatch-time TLA file selection and updates concurrency grouping to support the consolidation. |
.github/workflows/model-checking-manual.yml |
Deletes the standalone manual model-checking workflow after consolidation. |
docs/notes/issue-1006-workflow-triggers.md |
Updates trigger counts and removes references to the deleted workflow. |
docs/notes/issue-1006-workflow-trigger-profiles.md |
Updates trigger profiles/counts to reflect the removed workflow. |
docs/notes/issue-1006-workflow-overlap-candidates.md |
Updates formal verification trigger mapping and removes the deleted workflow from overlap candidates. |
docs/notes/issue-1006-workflow-inventory.md |
Updates workflow inventory counts and removes the deleted workflow from the list/prefix counts. |
docs/notes/issue-1006-ci-consolidation-draft.md |
Records the consolidation as a low-risk move in the CI consolidation draft. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Contributor
CI Status Snapshot (2026-01-25T14:02:01.510Z)
|
…ojp/ae-framework into chore/ci-formal-manual-merge
Contributor
❓ Code Generation Drift DetectionStatus: Automated by AE-Framework Codegen |
Contributor
🔍 Verification Summary
Unlinked (top 5)- Device registration publishes enough pre-keys and emits audit log (id: device-registration-publishes-enough-pre-keys-and-emits-audit-log) test:N/A impl:N/A formal:N/A - Invalid auth tag triggers audit violation for AES-GCM envelopes (id: invalid-auth-tag-triggers-audit-violation-for-aes-gcm-envelopes) test:N/A impl:N/A formal:N/A - Session rotation stays within forward secrecy thresholds (id: session-rotation-stays-within-forward-secrecy-thresholds) test:N/A impl:N/A formal:N/ALinked examples (up to 3)- Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/specs/formal/tla+/Inventory.tla) - Prevent negative stock (id: prevent-negative-stock) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/specs/formal/tla+/Inventory.tla) - Idempotent by order id (id: idempotent-by-order-id) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/00881c191a52413005a955453e7549a8585e16d0/specs/formal/tla+/Inventory.tla)Hit basis (tests/formal)- Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0Non-OK modules (top 5)- KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) - KvOnceImpl (log: artifacts/codex/KvOnceImpl.tlc.log.txt) - KvOnce (log: artifacts/codex/KvOnce.tlc.log.txt) - KvOnceRefinement (log: artifacts/codex/KvOnceRefinement.tlc.log.txt) |
Contributor
CodeX Artifacts Summary
|
Collaborator
Author
|
Copilotレビュー対応を反映しました。
main 取り込み済みでコンフリクトは解消しています。 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
概要
変更点
tlaFileを反映tlaFileを加味確認
Refs #1006 #1160