sscoble/speckl
1
0
Fork 0
Code Issues 2 Pull requests Projects Releases Packages Wiki Activity Actions

[speckl#37.7] B2: Forward constraint/verify expressions through TS generator (or evaluate at runtime) #45

New issue
Closed
opened 2026-06-02 21:55:51 +00:00 by sscoble · 2 comments
sscoble commented 2026-06-02 21:55:51 +00:00
Owner
Copy link

Problem

The TypeScript generator's checkConstraintN() and verifyN() stub emitters (around typescript-state-machine.ts:263-279) always return true with a // TODO: Evaluate in Z3 or runtime comment. No actual evaluation of the constraint expression or LTL-style verify formula ever happens at runtime. The generated code looks type-safe but is semantically a no-op for every spec with a constraint or verify block.

Affected examples

All 16 that have constraint or verify blocks: AccessControl, DrugDosageCalculator, KafkaProducer, OAuth2, PaymentService, Raft, RetryHandler, SQLitePager, SQLiteWAL, TemperatureMonitor, TigerBeetleLedger, TwoPhaseCommit, etc.

Scope

Forward the constraint expression through the existing rewriteExpr(...) chain and emit a real boolean expression. For verifyN, two acceptable resolutions (pick one):

  1. Runtime evaluation: Emit a real boolean expression that evaluates the LTL formula inline (e.g., via a small interpreter or a call into @speckdl/runtime if it exists).
  2. Z3 call-out: If the Z3 generator already handles LTL, call into it and short-circuit on false. Adds a Z3 runtime dependency to the TS output.

If neither resolution fits the 1200s subagent window, document the chosen approach in a comment and stub a follow-up ticket.

Out of scope

  • Do NOT implement a full LTL interpreter from scratch.
  • Do NOT touch the Z3 generator.
  • Do NOT run nix build or open a PR. Build only the compiler.

Acceptance Criteria

  • Pick resolution 1 (runtime) or resolution 2 (Z3 call-out) and document the choice in a comment
  • checkConstraintN() and verifyN() in the TS output return a real boolean (not always true) when the constraint/formula is violated
  • At least one example (recommend AccessControl.speck — simplest) is end-to-end verified: the emitted TS, when run, reports a constraint violation when the spec's constraint block is violated
  • All 16 examples still compile via tsc --noEmit --target es2020
  • Post the diff as a comment with a sample of the emitted constraint code and the runtime verification result

Why this exists

Triage on #39 found 6 bugs. B2 is the largest scope — Z3 integration or runtime evaluator work — and may need a second round of decomposition. Flagged as the 'do last' ticket.

Depends on

None (but B1's parser fix may unblock the AST shape; the generator can still be implemented independently if B1 lands in parallel)

Blocks

None

## Problem The TypeScript generator's `checkConstraintN()` and `verifyN()` stub emitters (around `typescript-state-machine.ts:263-279`) always return `true` with a `// TODO: Evaluate in Z3 or runtime` comment. No actual evaluation of the constraint expression or LTL-style `verify` formula ever happens at runtime. The generated code looks type-safe but is semantically a no-op for every spec with a `constraint` or `verify` block. ## Affected examples All 16 that have `constraint` or `verify` blocks: AccessControl, DrugDosageCalculator, KafkaProducer, OAuth2, PaymentService, Raft, RetryHandler, SQLitePager, SQLiteWAL, TemperatureMonitor, TigerBeetleLedger, TwoPhaseCommit, etc. ## Scope Forward the constraint expression through the existing `rewriteExpr(...)` chain and emit a real boolean expression. For `verifyN`, two acceptable resolutions (pick one): 1. **Runtime evaluation:** Emit a real boolean expression that evaluates the LTL formula inline (e.g., via a small interpreter or a call into `@speckdl/runtime` if it exists). 2. **Z3 call-out:** If the Z3 generator already handles LTL, call into it and short-circuit on `false`. Adds a Z3 runtime dependency to the TS output. If neither resolution fits the 1200s subagent window, document the chosen approach in a comment and stub a follow-up ticket. ## Out of scope - Do NOT implement a full LTL interpreter from scratch. - Do NOT touch the Z3 generator. - Do NOT run `nix build` or open a PR. Build only the compiler. ## Acceptance Criteria - [ ] Pick resolution 1 (runtime) or resolution 2 (Z3 call-out) and document the choice in a comment - [ ] `checkConstraintN()` and `verifyN()` in the TS output return a real boolean (not always `true`) when the constraint/formula is violated - [ ] At least one example (recommend `AccessControl.speck` — simplest) is end-to-end verified: the emitted TS, when run, reports a constraint violation when the spec's `constraint` block is violated - [ ] All 16 examples still compile via `tsc --noEmit --target es2020` - [ ] Post the diff as a comment with a sample of the emitted constraint code and the runtime verification result ## Why this exists Triage on #39 found 6 bugs. B2 is the largest scope — Z3 integration or runtime evaluator work — and may need a second round of decomposition. Flagged as the 'do last' ticket. ## Depends on None (but B1's parser fix may unblock the AST shape; the generator can still be implemented independently if B1 lands in parallel) ## Blocks None
sscoble commented 2026-06-03 01:41:36 +00:00
Author
Owner
Copy link

Decomposition — 2-child stack ready for PR-sequenced merge

Per Scott directive (2026-06-02 18:39 PT): decompose and stack PRs if necessary. This ticket is being split into two stackable children.

Child Scope ACs PR stack order Why split
#47 B2.1 — forward constraint expressions through rewriteExpr (synchronous, in-process) 4 PR 1 of 2 Pure boolean expressions, no LTL, no Z3 call-out. Fits 1200s.
#48 B2.2 — implement verifyN() with runtime LTL evaluator or Z3 call-out 5 PR 2 of 2 LTL subset (always/eventually/until/imply). Larger scope. Depends on #47.

Why split (not just dispatch as-is at 7 ACs):

  • 7+ ACs is the documented threshold for likely 1200s timeout (per the decompose-and-dispatch skill)
  • Constraints and verify are semantically different — constraints are stateless expressions, verify is LTL over a trace
  • Each child is independently releasable
  • The stack order matters: B2.1 (constraints) lands first, B2.2 (LTL) on top, so review of LTL is layered on top of a clean constraint baseline

PR stack patterns (Scott's choice):

  • Sequential merges: Open B2.1, merge, then open B2.2 against main. Clean main history, two PRs to review.
  • True stack: Open B2.1, then open B2.2 with base=b2.1-constraints. Review B2.2's diff on top of B2.1's branch. Merge B2.1 first, then B2.2 rebase-merge.

Dispatch plan (post-decomposition):

  • #47 (B2.1) → 4 ACs, dispatch sequentially (NOT parallel batch) per Scott's 18:39 PT directive on parallel-batch wall-clock
  • #48 (B2.2) → 5 ACs, dispatch sequentially after #47 ships
  • Both use the 1200s child_timeout_seconds budget; sequential dispatch avoids the parent wall-clock cap

Closing this ticket: Marking #45 as the B2 decomposition parent. Will be closed when both #47 and #48 ship.

## Decomposition — 2-child stack ready for PR-sequenced merge Per Scott directive (2026-06-02 18:39 PT): **decompose and stack PRs if necessary.** This ticket is being split into two stackable children. | Child | Scope | ACs | PR stack order | Why split | |---|---|---|---|---| | **#47** | B2.1 — forward constraint expressions through `rewriteExpr` (synchronous, in-process) | 4 | PR 1 of 2 | Pure boolean expressions, no LTL, no Z3 call-out. Fits 1200s. | | **#48** | B2.2 — implement `verifyN()` with runtime LTL evaluator or Z3 call-out | 5 | PR 2 of 2 | LTL subset (always/eventually/until/imply). Larger scope. Depends on #47. | **Why split (not just dispatch as-is at 7 ACs):** - 7+ ACs is the documented threshold for likely 1200s timeout (per the decompose-and-dispatch skill) - Constraints and verify are *semantically different* — constraints are stateless expressions, verify is LTL over a trace - Each child is independently releasable - The stack order matters: B2.1 (constraints) lands first, B2.2 (LTL) on top, so review of LTL is layered on top of a clean constraint baseline **PR stack patterns (Scott's choice):** - **Sequential merges:** Open B2.1, merge, then open B2.2 against main. Clean main history, two PRs to review. - **True stack:** Open B2.1, then open B2.2 with base=b2.1-constraints. Review B2.2's diff on top of B2.1's branch. Merge B2.1 first, then B2.2 rebase-merge. **Dispatch plan (post-decomposition):** - #47 (B2.1) → 4 ACs, dispatch sequentially (NOT parallel batch) per Scott's 18:39 PT directive on parallel-batch wall-clock - #48 (B2.2) → 5 ACs, dispatch sequentially after #47 ships - Both use the 1200s `child_timeout_seconds` budget; sequential dispatch avoids the parent wall-clock cap **Closing this ticket:** Marking #45 as the B2 decomposition parent. Will be closed when both #47 and #48 ship.
sscoble commented 2026-06-03 03:38:01 +00:00
Author
Owner
Copy link

CoS housekeeping closure (2026-06-02 cron cycle 21:50 UTC)

This ticket's scope has been carried by decomposition children. Closing the parent.

Decomposition (2026-06-02 18:39 PT, Scott directive)

Child Title State
sscoble/speckl#47 B2.1: Forward constraint expressions through TS generator (rewriteExpr chain) in flight (parser fix from #49 just landed, ready to re-dispatch)
sscoble/speckl#48 B2.2: Implement verifyN() with runtime LTL evaluator (or Z3 call-out) open, depends on #47 (PR stack 2 of 2)

Why close the parent

The B2 work is now bounded to two atomic-releasable children with explicit PR-stack ordering. The original 7 ACs of this ticket are split:

  • AC1, AC2 (constraint handling) → #47
  • AC3, AC4 (LTL verify, runtime vs Z3) → #48
  • AC5 (post the diff) → per child

The "choose runtime vs Z3" decision in AC1 here is also pushed to #48 (per the CoS verification, this is a Scott-level architecture call that the agent should not make unilaterally).

Cross-references

Closing this parent. Reopen if Scott wants the runtime-vs-Z3 decision in the original parent thread.

## CoS housekeeping closure (2026-06-02 cron cycle 21:50 UTC) This ticket's scope has been carried by decomposition children. Closing the parent. ### Decomposition (2026-06-02 18:39 PT, Scott directive) | Child | Title | State | |---|---|---| | **sscoble/speckl#47** | B2.1: Forward constraint expressions through TS generator (rewriteExpr chain) | in flight (parser fix from #49 just landed, ready to re-dispatch) | | **sscoble/speckl#48** | B2.2: Implement verifyN() with runtime LTL evaluator (or Z3 call-out) | open, depends on #47 (PR stack 2 of 2) | ### Why close the parent The B2 work is now bounded to two atomic-releasable children with explicit PR-stack ordering. The original 7 ACs of this ticket are split: - AC1, AC2 (constraint handling) → #47 - AC3, AC4 (LTL verify, runtime vs Z3) → #48 - AC5 (post the diff) → per child The "choose runtime vs Z3" decision in AC1 here is also pushed to #48 (per the CoS verification, this is a Scott-level architecture call that the agent should not make unilaterally). ### Cross-references - Parent triage: sscoble/speckl#39 (closed) - Sibling B5 (init block parser): sscoble/speckl#44 (closed, dispatch verified by CoS 2026-06-02 23:14 UTC) - Parser fix that unblocks B2.1: sscoble/speckl#49 (closed, dispatch verified 2026-06-03 03:01 UTC) Closing this parent. Reopen if Scott wants the runtime-vs-Z3 decision in the original parent thread.
Sign in to join this conversation.
No Branch/Tag specified
Branches Tags
main
lagrangia-v1.1
ifblock-fix
now-fix
lagrangia-score
fix/speckl-55-ltl-inner-identifier-scope
fix/parser-precondition-postcondition
fix/compiler-enum-rewrite-parser-quotes
No results found.
Labels
Clear labels   
blocked

   
bug

   
design

   
docs

   
engineering

   
feature

   
infra

   
priority:high

   
priority:low

   
priority:medium

   
question
No labels
blocked
bug
design
docs
engineering
feature
infra
priority:high
priority:low
priority:medium
question
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: sscoble/speckl#45
No description provided.
Delete branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?