Skip to content

Conversation

@ootakazuhiko
Copy link
Collaborator

Summary

  • remove workflow_dispatch from ci-fast.yml and ci-extended.yml
  • keep these workflows reusable only, entry remains in ci.yml

Testing

  • not run (workflow change)

Related

Copilot AI review requested due to automatic review settings January 28, 2026 15:12
@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@ootakazuhiko
Copy link
Collaborator Author

Auto Update Branch

PR #1812 was behind base; triggered branch update.
If conflicts remain, manual resolution is required.

@github-actions
Copy link
Contributor

Quality Summary

  • Adapters:

  • Formal: n/a

  • Replay: n/a

  • Trace IDs:

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
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/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/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/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/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/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/b48b8552a3ef0378dad3d763488a14d8b3a0ebb2/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-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)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
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/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/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/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/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/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/6857b9c276a51cfd2fc4c22cdb1e2d83e9035aa7/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-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)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

Copy link

@chatgpt-codex-connector chatgpt-codex-connector bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b48b8552a3

ℹ️ About Codex in GitHub

Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".

Copy link
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR removes workflow_dispatch triggers from ci-fast.yml and ci-extended.yml as part of the CI consolidation effort described in issue #1006. The goal is to make these workflows reusable only (via workflow_call), with ci.yml serving as the single entry point for triggering CI workflows.

Changes:

  • Removed workflow_dispatch: trigger from ci-fast.yml
  • Removed workflow_dispatch: trigger from ci-extended.yml

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.

File Description
.github/workflows/ci-fast.yml Removed workflow_dispatch trigger to limit to workflow_call only
.github/workflows/ci-extended.yml Removed workflow_dispatch trigger to limit to workflow_call only

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@github-actions
Copy link
Contributor

❓ Code Generation Drift Detection

Status:
Regeneration needed: No


Automated by AE-Framework Codegen

@github-actions
Copy link
Contributor

🔍 Verification Summary

  • Traceability: 6 scenarios
    • Tests: 3 (50%)
    • Impl: 3 (50%)
    • Formal: 3 (50%)
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/A
Linked examples (up to 3) - Successful reservation (id: successful-reservation) test: [traceability/inventory.trace.test.ts](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/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/77888218ccc22d476c2fbbc3ae3bf2871e956625/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/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/77888218ccc22d476c2fbbc3ae3bf2871e956625/tests/traceability/inventory.trace.test.ts) impl: [domain/inventory.ts](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/src/domain/inventory.ts) formal: [tla+/Inventory.tla](https://github.com/itdojp/ae-framework/blob/77888218ccc22d476c2fbbc3ae3bf2871e956625/specs/formal/tla+/Inventory.tla)
Hit basis (tests/formal) - Test hits: title=3 id=0 tag=0 - Formal hits: title=0 id=3 tag=0
- Model Check (TLC): 2/8 (25%) modules ok
Non-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)
- Alloy: detected 2 specs (execution skipped) - Contracts: schemas=true conditions=true machine=true - Contracts exec: parseIn=false pre=false post=false parseOut=false

@github-actions
Copy link
Contributor

CodeX Artifacts Summary

  • • Contract/E2E templates: 1 files (dir: tests/api/generated)
  • • Tests: PBT files=122, BDD features=0
  • • Formal specs: TLA=1, Alloy=1

@ootakazuhiko ootakazuhiko merged commit 36b7cf0 into main Jan 28, 2026
43 of 45 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant