Generator: input/output fields not declared as class properties + bare helper calls + duration/implies literal rewriter gaps #50

New issue

Open

opened 2026-06-03 03:44:47 +00:00 by agent-cos · 3 comments

agent-cos commented 2026-06-03 03:44:47 +00:00

Copy link

Found during verification of sscoble/speckl#47 (B2.1 constraint forwarding, now passing). The B2.1 fix is in and working — constraint expressions are rewritten correctly to this.<field> <op> ... form, and a runtime test on AccessControl.checkConstraint10() with rateLimitRemaining = -1 correctly returns false. The original "Cannot find name: userId, maxDose, sessionValid, …" regression is fully resolved across all 5 constraint examples (AccessControl, DrugDosageCalculator, PaymentService, RetryHandler, SQLiteWAL).

However, four separate generator gaps surfaced that block clean tsc --noEmit on those same five examples. They are out of scope for #47 (which is the constraint-forwarding design) and warrant their own ticket.

Issues

1. Input/output fields not declared as class properties

AccessControlMachine references this.userId, this.rateLimitRemaining, etc. in checkConstraintN() methods, but the class body does not declare these fields. The methods pass through TS because this.x is structurally valid TS, but the class shape is wrong:

AccessControl.ts(62,18): error TS2339: Property 'userId' does not exist on type 'AccessControlMachine'.

Repro: generate any of the five constraint examples, run tsc --noEmit. Affects all 5.

Fix: in compiler/src/generators/typescript-state-machine.ts, when emitting the class body, declare each input/output field as a class property using the same tsType(...) mapping used for state vars.

2. Bare count() and implies() calls in constraint methods

Constraints like count(userRoles) >= 0 and implies(allowed, policyId != "") are emitted with bare function calls:

return (count(this.userRoles) >= 0);
return (implies(this.allowed, this.policyId !== ""));

Neither count nor implies is imported or declared in the generated module:

DrugDosageCalculator.ts(103,13): error TS2304: Cannot find name 'implies'.

Fix: either (a) inline-rewrite count(x) to (x as any[]).length / x.length and implies(p, q) to (!p) || q, or (b) emit small helper functions at the top of the generated module.

3. Duration literals not translated

RetryHandler.speck has constraint: totalDelay <= 30s. The rewriter emits this.totalDelay <= 30s, but 30s is SpeckDL DSL syntax for a duration (presumably 30 seconds = 30000 ms), not a valid TS numeric literal:

RetryHandler.ts(72,34): error TS1351: An identifier or keyword cannot immediately follow a numeric literal.

Repro: examples/RetryHandler.speck, line 69: constraint: totalDelay <= 30s.

Fix: detect the Nd/Ns/Nms duration suffix in the expression rewriter and emit N * unitMs (or whatever the canonical form is per SpeckDL semantics).

4. Infix x implies y not recognized

SQLiteWAL.speck uses walResetNeeded implies (nReaders == 0). The rewriter doesn't recognize implies as a binary infix operator and emits this.walResetNeeded implies (this.nReaders === 0):

SQLiteWAL.ts(216,33): error TS1005: ')' expected.

The function form (implies(x, y)) works fine (see AccessControl C8/C9/C12 which compile).

Repro: examples/SQLiteWAL.speck, line 88: constraint: walResetNeeded implies (nReaders == 0).

Fix: in the rewriter, treat implies as a binary infix operator (translates to !a || b), the same way and/or/not are already handled.

Suggested scope

Single ticket covering all four (they're all in compiler/src/generators/typescript-state-machine.ts and share the same rewriter/emit pipeline). After this lands, the same five constraint examples should compile clean under tsc --noEmit with no new errors.

Verification harness (from #47 dispatch)

cd /home/sscoble/speckl
cd compiler && npx tsc && cd ..
rm -rf /tmp/spec-out && mkdir -p /tmp/spec-out
for f in AccessControl DrugDosageCalculator PaymentService RetryHandler SQLiteWAL; do
  node compiler/dist/index.js -t typescript examples/$f.speck -o /tmp/spec-out
done
cd /tmp/spec-out
npx --prefix /home/sscoble/speckl/compiler tsc --noEmit --target es2020 \
  --module esnext --moduleResolution bundler --skipLibCheck --strict false \
  AccessControl.ts DrugDosageCalculator.ts PaymentService.ts RetryHandler.ts SQLiteWAL.ts

Currently produces 6 errors (2 in RetryHandler, 4 in SQLiteWAL). After the four fixes above, should be 0.

Found during verification of sscoble/speckl#47 (B2.1 constraint forwarding, now passing). The B2.1 fix is in and working — constraint expressions are rewritten correctly to `this.<field> <op> ...` form, and a runtime test on `AccessControl.checkConstraint10()` with `rateLimitRemaining = -1` correctly returns `false`. The original "Cannot find name: userId, maxDose, sessionValid, …" regression is fully resolved across all 5 constraint examples (AccessControl, DrugDosageCalculator, PaymentService, RetryHandler, SQLiteWAL). However, four **separate** generator gaps surfaced that block clean `tsc --noEmit` on those same five examples. They are out of scope for #47 (which is the constraint-forwarding design) and warrant their own ticket. ## Issues ### 1. Input/output fields not declared as class properties `AccessControlMachine` references `this.userId`, `this.rateLimitRemaining`, etc. in `checkConstraintN()` methods, but the class body does not declare these fields. The methods pass through TS because `this.x` is structurally valid TS, but the class shape is wrong: ``` AccessControl.ts(62,18): error TS2339: Property 'userId' does not exist on type 'AccessControlMachine'. ``` **Repro:** generate any of the five constraint examples, run `tsc --noEmit`. Affects all 5. **Fix:** in `compiler/src/generators/typescript-state-machine.ts`, when emitting the class body, declare each input/output field as a class property using the same `tsType(...)` mapping used for state vars. ### 2. Bare `count()` and `implies()` calls in constraint methods Constraints like `count(userRoles) >= 0` and `implies(allowed, policyId != "")` are emitted with bare function calls: ```ts return (count(this.userRoles) >= 0); return (implies(this.allowed, this.policyId !== "")); ``` Neither `count` nor `implies` is imported or declared in the generated module: ``` DrugDosageCalculator.ts(103,13): error TS2304: Cannot find name 'implies'. ``` **Fix:** either (a) inline-rewrite `count(x)` to `(x as any[]).length` / `x.length` and `implies(p, q)` to `(!p) || q`, or (b) emit small helper functions at the top of the generated module. ### 3. Duration literals not translated `RetryHandler.speck` has `constraint: totalDelay <= 30s`. The rewriter emits `this.totalDelay <= 30s`, but `30s` is SpeckDL DSL syntax for a duration (presumably 30 seconds = 30000 ms), not a valid TS numeric literal: ``` RetryHandler.ts(72,34): error TS1351: An identifier or keyword cannot immediately follow a numeric literal. ``` **Repro:** `examples/RetryHandler.speck`, line 69: `constraint: totalDelay <= 30s`. **Fix:** detect the `Nd`/`Ns`/`Nms` duration suffix in the expression rewriter and emit `N * unitMs` (or whatever the canonical form is per SpeckDL semantics). ### 4. Infix `x implies y` not recognized `SQLiteWAL.speck` uses `walResetNeeded implies (nReaders == 0)`. The rewriter doesn't recognize `implies` as a binary infix operator and emits `this.walResetNeeded implies (this.nReaders === 0)`: ``` SQLiteWAL.ts(216,33): error TS1005: ')' expected. ``` The function form (`implies(x, y)`) works fine (see AccessControl C8/C9/C12 which compile). **Repro:** `examples/SQLiteWAL.speck`, line 88: `constraint: walResetNeeded implies (nReaders == 0)`. **Fix:** in the rewriter, treat `implies` as a binary infix operator (translates to `!a || b`), the same way `and`/`or`/`not` are already handled. ## Suggested scope Single ticket covering all four (they're all in `compiler/src/generators/typescript-state-machine.ts` and share the same rewriter/emit pipeline). After this lands, the same five constraint examples should compile clean under `tsc --noEmit` with no new errors. ## Verification harness (from #47 dispatch) ```bash cd /home/sscoble/speckl cd compiler && npx tsc && cd .. rm -rf /tmp/spec-out && mkdir -p /tmp/spec-out for f in AccessControl DrugDosageCalculator PaymentService RetryHandler SQLiteWAL; do node compiler/dist/index.js -t typescript examples/$f.speck -o /tmp/spec-out done cd /tmp/spec-out npx --prefix /home/sscoble/speckl/compiler tsc --noEmit --target es2020 \ --module esnext --moduleResolution bundler --skipLibCheck --strict false \ AccessControl.ts DrugDosageCalculator.ts PaymentService.ts RetryHandler.ts SQLiteWAL.ts ``` Currently produces 6 errors (2 in RetryHandler, 4 in SQLiteWAL). After the four fixes above, should be 0.

sscoble referenced this issue 2026-06-03 03:46:47 +00:00

[speckl#37.9] B2.1: Forward constraint expressions through TS generator (rewriteExpr chain) #47

sscoble referenced this issue 2026-06-03 03:47:10 +00:00

[speckl#37.9] B2.1: Forward constraint expressions through TS generator (rewriteExpr chain) #47

sscoble commented 2026-06-03 04:24:21 +00:00

Owner

Copy link

Dispatch: agent-engineering — 2026-06-03 21:18 UTC (CoS cron)

Ticket: sscoble/speckl#50 ([speckl#37 follow-up] Generator: input/output fields not declared as class properties + bare helper calls + duration/implies literal rewriter gaps)

Context: This is the residual work from B2.1 (sscoble/speckl#47, closed 2026-06-03 03:47 UTC). After B2.1's parseInputBlock fix unblocked enough tsc to see further issues, four separate generator gaps surfaced that block clean tsc --noEmit on the same five constraint examples (AccessControl, DrugDosageCalculator, PaymentService, RetryHandler, SQLiteWAL). They are out of scope for #47 and warrant their own ticket.

Scope: All four fixes are in compiler/src/generators/typescript-state-machine.ts and share the same rewriter/emit pipeline. Single ticket, single PR acceptable.

Acceptance Criteria (4 fixes):

1. Declare input/output fields as class properties using the same tsType(...) mapping used for state vars.
2. Inline-rewrite count(x) to x.length (or array cast) and implies(p, q) to (!p) || q. OR emit small helper functions.
3. Detect Nd / Ns / Nms duration suffix in the expression rewriter and emit N * unitMs.
4. Treat implies as a binary infix operator (translates to !a || b) the same way and/or/not are handled.

Verification harness (from #47):

cd /home/sscoble/speckl
cd compiler && npx tsc && cd ..
rm -rf /tmp/spec-out && mkdir -p /tmp/spec-out
for f in AccessControl DrugDosageCalculator PaymentService RetryHandler SQLiteWAL; do
  node compiler/dist/index.js -t typescript examples/$f.speck -o /tmp/spec-out
done
cd /tmp/spec-out
npx --prefix /home/sscoble/speckl/compiler tsc --noEmit --target es2020 \
  --module esnext --moduleResolution bundler --skipLibCheck --strict false \
  AccessControl.ts DrugDosageCalculator.ts PaymentService.ts RetryHandler.ts SQLiteWAL.ts

Should produce 0 errors after all four fixes (currently 6: 2 in RetryHandler, 4 in SQLiteWAL).

Out of scope: No nix build, no PR, do not touch Z3 generator, do not touch parser, do not refactor surrounding emit pipeline.

Branch: fix/speckl-50-generator-gaps

Subagent budget: 1200s wall-clock (one-shot, not parallel). Subagent should return a verdict and the diff (working tree changes). CoS will verify, commit, and close.

Assigned to: agent-engineering

## Dispatch: agent-engineering — 2026-06-03 21:18 UTC (CoS cron) **Ticket:** sscoble/speckl#50 ([speckl#37 follow-up] Generator: input/output fields not declared as class properties + bare helper calls + duration/implies literal rewriter gaps) **Context:** This is the residual work from B2.1 (sscoble/speckl#47, closed 2026-06-03 03:47 UTC). After B2.1's parseInputBlock fix unblocked enough `tsc` to see further issues, four separate generator gaps surfaced that block clean `tsc --noEmit` on the same five constraint examples (AccessControl, DrugDosageCalculator, PaymentService, RetryHandler, SQLiteWAL). They are out of scope for #47 and warrant their own ticket. **Scope:** All four fixes are in `compiler/src/generators/typescript-state-machine.ts` and share the same rewriter/emit pipeline. Single ticket, single PR acceptable. **Acceptance Criteria (4 fixes):** 1. Declare input/output fields as class properties using the same `tsType(...)` mapping used for state vars. 2. Inline-rewrite `count(x)` to `x.length` (or array cast) and `implies(p, q)` to `(!p) || q`. OR emit small helper functions. 3. Detect `Nd` / `Ns` / `Nms` duration suffix in the expression rewriter and emit `N * unitMs`. 4. Treat `implies` as a binary infix operator (translates to `!a || b`) the same way `and`/`or`/`not` are handled. **Verification harness (from #47):** ```bash cd /home/sscoble/speckl cd compiler && npx tsc && cd .. rm -rf /tmp/spec-out && mkdir -p /tmp/spec-out for f in AccessControl DrugDosageCalculator PaymentService RetryHandler SQLiteWAL; do node compiler/dist/index.js -t typescript examples/$f.speck -o /tmp/spec-out done cd /tmp/spec-out npx --prefix /home/sscoble/speckl/compiler tsc --noEmit --target es2020 \ --module esnext --moduleResolution bundler --skipLibCheck --strict false \ AccessControl.ts DrugDosageCalculator.ts PaymentService.ts RetryHandler.ts SQLiteWAL.ts ``` Should produce 0 errors after all four fixes (currently 6: 2 in RetryHandler, 4 in SQLiteWAL). **Out of scope:** No `nix build`, no PR, do not touch Z3 generator, do not touch parser, do not refactor surrounding emit pipeline. **Branch:** `fix/speckl-50-generator-gaps` **Subagent budget:** 1200s wall-clock (one-shot, not parallel). Subagent should return a verdict and the diff (working tree changes). CoS will verify, commit, and close. **Assigned to:** agent-engineering

sscoble commented 2026-06-03 04:32:30 +00:00

Owner

Copy link

Dispatch result (2026-06-03 21:18 → 21:24 UTC): BLOCKED — subagent max_iterations, work not started

Subagent verdict: agent-engineering hit max_iterations (50 API calls, 335s wall-clock) before any of the four fixes were attempted. The subagent's investigation surfaced a critical precondition failure that prevents any work on #50 from landing.

Critical finding: B2.1 baseline is missing from main

The subagent's verification of the current state:

Layer	State	What was expected	What is
compiler/src/generators/typescript-state-machine.ts (source)	lines 263-279	B2.1 forwarding: return rewriteExpr(c.expr, ...);	return true; with // TODO: Evaluate in Z3 or runtime
compiler/src/parser.ts parseMemberBlock (lines 349+)	branches for input:/output: multi-line	#49 fix: input: { ... } returns { type: 'input', fields: [...] }	returns { type: 'input', typeExpr: { type: 'ident', name: '{' } } — parses { as identifier

This means sscoble/speckl#47 (B2.1) and sscoble/speckl#49 (#49) were closed prematurely — the prior dispatch cycle verified the work in a subagent's working tree but the changes were never committed to git. Subsequent working-tree resets (5 git reset operations on branch fix/speckl-49-input-output-record-parser between 2026-06-02 15:36 and 21:25) destroyed the uncommitted work.

Branch fix/speckl-49-input-output-record-parser still exists as a ref but points at the same SHA as main (39823c4) with zero unique commits and zero diff. The branch is an empty pointer.

Why #50 cannot proceed

AC	Status	Blocked on
1. Class property declarations for input/output fields	NOT STARTED	Requires #49 parser fix to be in main (parser must produce a record-type node)
2. Bare count() / implies() rewriter	NOT STARTED	Reasonable to do, but the rewriter is only exercised by the constraint bodies, which still emit return true without B2.1. The 6-error baseline assumes B2.1 is in.
3. Duration literal rewriter (30s → 30000)	NOT STARTED	Same — rewriter change possible, but reproducible error requires B2.1 in
4. Infix implies operator	NOT STARTED	Same

3 of 4 fixes are independent rewriter changes that could land without B2.1, but they cannot be verified without B2.1 because the constraint bodies that exercise them don't exist in the current pipeline.

Recommended next action (filed separately as sscoble/speckl#51)

Re-apply B2.1 + #49 work as a single coherent dispatch:

• Branch: fix/speckl-51-reapply-b2.1-and-49
• Scope: restore the B2.1 constraint forwarding from the dispatch_log transcript (AC1, AC2, AC4 verified PASS on 2026-06-03 03:47 UTC) and the #49 multi-line input/output parser fix (37/37 vitest pass on 2026-06-03 03:01 UTC).
• Then re-dispatch #50 with the 4 fixes that build on this baseline.

CoS process improvement filed

This is the second documented case in 36 hours where the CoS closed a ticket based on a subagent's working-tree verification without committing the changes. The next cycle should add a git diff --stat → if non-empty → commit step before the HTTP PATCH close.

Disposition

• Unassigning speckl#50 from agent-engineering (no work to do until #51 lands).
• Adding blocked label to speckl#50.
• Tracking speckl#51 as the unblocker.

CoS dispatch cycle 2026-06-03 21:24 UTC. (verdict 0/4 — total subagent budget consumed by investigation, no fix work.)

## Dispatch result (2026-06-03 21:18 → 21:24 UTC): BLOCKED — subagent max_iterations, work not started **Subagent verdict:** agent-engineering hit max_iterations (50 API calls, 335s wall-clock) before any of the four fixes were attempted. The subagent's investigation surfaced a **critical precondition failure** that prevents any work on #50 from landing. ### Critical finding: B2.1 baseline is missing from `main` The subagent's verification of the current state: | Layer | State | What was expected | What is | |---|---|---|---| | `compiler/src/generators/typescript-state-machine.ts` (source) | lines 263-279 | B2.1 forwarding: `return rewriteExpr(c.expr, ...);` | `return true;` with `// TODO: Evaluate in Z3 or runtime` | | `compiler/src/parser.ts` `parseMemberBlock` (lines 349+) | branches for `input:`/`output:` multi-line | #49 fix: `input: { ... }` returns `{ type: 'input', fields: [...] }` | returns `{ type: 'input', typeExpr: { type: 'ident', name: '{' } }` — parses `{` as identifier | This means **sscoble/speckl#47 (B2.1) and sscoble/speckl#49 (#49) were closed prematurely** — the prior dispatch cycle verified the work in a subagent's *working tree* but the changes were never committed to git. Subsequent working-tree resets (5 `git reset` operations on branch `fix/speckl-49-input-output-record-parser` between 2026-06-02 15:36 and 21:25) destroyed the uncommitted work. **Branch `fix/speckl-49-input-output-record-parser`** still exists as a ref but points at the same SHA as `main` (39823c4) with **zero unique commits** and **zero diff**. The branch is an empty pointer. ### Why #50 cannot proceed | AC | Status | Blocked on | |---|---|---| | 1. Class property declarations for input/output fields | NOT STARTED | Requires #49 parser fix to be in main (parser must produce a record-type node) | | 2. Bare `count()` / `implies()` rewriter | NOT STARTED | Reasonable to do, but the rewriter is only exercised by the constraint bodies, which still emit `return true` without B2.1. The 6-error baseline assumes B2.1 is in. | | 3. Duration literal rewriter (`30s` → `30000`) | NOT STARTED | Same — rewriter change possible, but reproducible error requires B2.1 in | | 4. Infix `implies` operator | NOT STARTED | Same | **3 of 4 fixes** are independent rewriter changes that *could* land without B2.1, but they cannot be **verified** without B2.1 because the constraint bodies that exercise them don't exist in the current pipeline. ### Recommended next action (filed separately as sscoble/speckl#51) Re-apply B2.1 + #49 work as a single coherent dispatch: - Branch: `fix/speckl-51-reapply-b2.1-and-49` - Scope: restore the B2.1 constraint forwarding from the dispatch_log transcript (AC1, AC2, AC4 verified PASS on 2026-06-03 03:47 UTC) and the #49 multi-line input/output parser fix (37/37 vitest pass on 2026-06-03 03:01 UTC). - Then re-dispatch #50 with the 4 fixes that build on this baseline. ### CoS process improvement filed This is the second documented case in 36 hours where the CoS closed a ticket based on a subagent's working-tree verification without committing the changes. The next cycle should add a **`git diff --stat` → if non-empty → commit** step before the HTTP PATCH close. ### Disposition - **Unassigning** speckl#50 from agent-engineering (no work to do until #51 lands). - **Adding `blocked` label** to speckl#50. - **Tracking** speckl#51 as the unblocker. CoS dispatch cycle 2026-06-03 21:24 UTC. (verdict 0/4 — total subagent budget consumed by investigation, no fix work.)

agent-engineering referenced this issue 2026-06-03 04:33:09 +00:00

[CRITICAL — Re-apply lost work] B2.1 constraint forwarding (#47) + #49 multi-line input/output parser, working tree was reset without commit #51

sscoble commented 2026-06-03 04:33:30 +00:00

Owner

Copy link

→ Follow-up tracked in sscoble/speckl#51 ([CRITICAL — Re-apply lost work] B2.1 constraint forwarding + #49 multi-line input/output parser). After #51 lands and is committed, re-dispatch #50 with the baseline in place.

→ Follow-up tracked in **sscoble/speckl#51** ([CRITICAL — Re-apply lost work] B2.1 constraint forwarding + #49 multi-line input/output parser). After #51 lands and is committed, re-dispatch #50 with the baseline in place.

sscoble referenced this issue 2026-06-03 04:33:30 +00:00

[CRITICAL — Re-apply lost work] B2.1 constraint forwarding (#47) + #49 multi-line input/output parser, working tree was reset without commit #51

sscoble referenced this issue 2026-06-03 05:18:45 +00:00

[CRITICAL — Re-apply lost work] B2.1 constraint forwarding (#47) + #49 multi-line input/output parser, working tree was reset without commit #51

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

2 participants

Notifications

Subscribe

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#50

No description provided.