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

Compare commits

base: sscoble:ifblock-fix
Branches Tags
sscoble:main
sscoble:lagrangia-v1.1
sscoble:ifblock-fix
sscoble:now-fix
sscoble:lagrangia-score
sscoble:fix/speckl-55-ltl-inner-identifier-scope
sscoble:fix/parser-precondition-postcondition
sscoble:fix/compiler-enum-rewrite-parser-quotes
..
compare: sscoble:main
Branches Tags
sscoble:lagrangia-v1.1
sscoble:ifblock-fix
sscoble:now-fix
sscoble:lagrangia-score
sscoble:fix/speckl-55-ltl-inner-identifier-scope
sscoble:main
sscoble:fix/parser-precondition-postcondition
sscoble:fix/compiler-enum-rewrite-parser-quotes

No commits in common. "ifblock-fix" and "main" have entirely different histories.
ifblock-fi ... main

39 changed files with 519 additions and 3351 deletions
Download patch file Download diff file Expand all files Collapse all files

399
compiler/__tests__/parser.test.ts
View file

@ -1,10 +1,6 @@
import { describe, it, expect } from 'vitest'; import { describe, it, expect } from 'vitest';
import path from 'path';
import { fileURLToPath } from 'url';
import { parseSpeckContent, parseSpeckFile } from '../src/parser.js'; import { parseSpeckContent, parseSpeckFile } from '../src/parser.js';
const __dirname = path.dirname(fileURLToPath(import.meta.url));
describe('SpeckDL Parser', () => { describe('SpeckDL Parser', () => {
describe('parseSpeckContent', () => { describe('parseSpeckContent', () => {
it('should parse a minimal speck definition with name', () => { it('should parse a minimal speck definition with name', () => {
@ -104,60 +100,6 @@ speck Second {
} }
}); });
it('should parse input with multi-line record type (speckl#57)', () => {
const content = `speck Test {
input: {
operation: Operation,
maxRetries: Nat,
initialDelay: Real,
maxDelay: Real
}
output: {
success: Bool,
finalResult: String,
attemptCount: Nat,
totalDelay: Real
}
}`;
const ast = parseSpeckContent(content);
const input = ast.specks[0].members[0];
const output = ast.specks[0].members[1];
expect(input.type).toBe('input');
expect(output.type).toBe('output');
if (input.type === 'input') {
expect(input.typeExpr.type).toBe('record');
expect(input.typeExpr.fields).toHaveLength(4);
expect(input.typeExpr.fields![0].name).toBe('operation');
expect(input.typeExpr.fields![3].name).toBe('maxDelay');
}
if (output.type === 'output') {
expect(output.typeExpr.type).toBe('record');
expect(output.typeExpr.fields).toHaveLength(4);
expect(output.typeExpr.fields![0].name).toBe('success');
expect(output.typeExpr.fields![3].name).toBe('totalDelay');
}
});
it('should parse input with multi-line record type, comments inside (speckl#57)', () => {
// Edge case: line comments inside the block
const content = `speck Test {
input: {
// the operation to retry
operation: Operation,
// max number of retry attempts
retries: Nat
}
}`;
const ast = parseSpeckContent(content);
const input = ast.specks[0].members[0];
if (input.type === 'input') {
expect(input.typeExpr.type).toBe('record');
expect(input.typeExpr.fields).toHaveLength(2);
expect(input.typeExpr.fields![0].name).toBe('operation');
expect(input.typeExpr.fields![1].name).toBe('retries');
}
});
it('should parse input with list type', () => { it('should parse input with list type', () => {
const content = `speck Test { const content = `speck Test {
input: [Nat] input: [Nat]
@ -537,7 +479,7 @@ speck Second {
}); });
it('should parse full TigerBeetle speck from file', () => { it('should parse full TigerBeetle speck from file', () => {
const ast = parseSpeckFile(path.join(__dirname, 'tigerbeetle.speck')); const ast = parseSpeckFile('./__tests__/tigerbeetle.speck');
expect(ast.specks).toHaveLength(1); expect(ast.specks).toHaveLength(1);
const speck = ast.specks[0]; const speck = ast.specks[0];
@ -582,343 +524,4 @@ speck Second {
} }
}); });
}); });
// Cycle 57: oneof syntax for proto wire-format discriminated unions.
describe('oneof blocks (cycle 57)', () => {
it('should parse a minimal oneof with two variants', () => {
const content = `speck One {
oneof Payload {
create_group: CreateGroup
add_steward: AddSteward
}
}`;
const ast = parseSpeckContent(content);
const oneof = ast.specks[0].members.find(m => m.type === 'oneof');
expect(oneof).toBeDefined();
if (oneof?.type === 'oneof') {
expect(oneof.name).toBe('Payload');
expect(oneof.variants).toEqual([
{ fieldName: 'create_group', typeName: 'CreateGroup' },
{ fieldName: 'add_steward', typeName: 'AddSteward' },
]);
}
});
it('should tolerate trailing commas / semicolons (proto-style)', () => {
const content = `speck One {
oneof Payload {
create_group: CreateGroup,
add_steward: AddSteward;
}
}`;
const ast = parseSpeckContent(content);
const oneof = ast.specks[0].members.find(m => m.type === 'oneof');
if (oneof?.type === 'oneof') {
expect(oneof.variants).toHaveLength(2);
}
});
it('should skip comments inside oneof blocks', () => {
const content = `speck One {
oneof Payload {
// bootstrap variant
create_group: CreateGroup
/* member action */
add_member: AddMember
}
}`;
const ast = parseSpeckContent(content);
const oneof = ast.specks[0].members.find(m => m.type === 'oneof');
if (oneof?.type === 'oneof') {
expect(oneof.variants.map(v => v.fieldName)).toEqual(['create_group', 'add_member']);
}
});
it('should coexist with interface and event blocks', () => {
const content = `speck Mix {
event CreateGroup { name: String }
interface AddSteward { new_steward: String }
oneof Payload {
create_group: CreateGroup
add_steward: AddSteward
}
}`;
const ast = parseSpeckContent(content);
const members = ast.specks[0].members;
expect(members.filter(m => m.type === 'event')).toHaveLength(1);
expect(members.filter(m => m.type === 'interface')).toHaveLength(1);
expect(members.filter(m => m.type === 'oneof')).toHaveLength(1);
});
});
// Cycle 58: transition envelope — a proto message wrapping a oneof payload
// plus metadata fields. Federated-meetup's `Transition` message is the
// canonical example: prior_state, payload (oneof), steward_signatures,
// hlc, branch_id, signed_at.
describe('transition blocks (cycle 58)', () => {
it('should parse a minimal transition with regular fields', () => {
const content = `speck One {
transition Transition {
hlc: Bytes
branch_id: Nat
}
}`;
const ast = parseSpeckContent(content);
const t = ast.specks[0].members.find(m => m.type === 'transition');
expect(t).toBeDefined();
if (t?.type === 'transition') {
expect(t.name).toBe('Transition');
expect(t.fields.map(f => f.name)).toEqual(['hlc', 'branch_id']);
expect(t.payloadOneof).toBeUndefined();
expect(t.typeDiscriminator).toBeUndefined();
}
});
it('should recognize payload: <OneofName> and record the reference', () => {
const content = `speck One {
oneof TransitionPayload {
create_group: CreateGroupPayload
}
transition Transition {
type: TransitionType
payload: TransitionPayload
hlc: Bytes
}
}`;
const ast = parseSpeckContent(content);
const t = ast.specks[0].members.find(m => m.type === 'transition');
if (t?.type === 'transition') {
expect(t.payloadOneof).toBe('TransitionPayload');
// payload must NOT appear in fields
expect(t.fields.map(f => f.name)).toEqual(['hlc']);
// type is a discriminator reference, not a regular field
expect(t.typeDiscriminator).toBe('TransitionType');
expect(t.fields.find(f => f.name === 'type')).toBeUndefined();
}
});
it('should tolerate trailing commas and comments', () => {
const content = `speck One {
transition Transition {
// timestamp from the signer
signed_at: Timestamp,
hlc: Bytes;
}
}`;
const ast = parseSpeckContent(content);
const t = ast.specks[0].members.find(m => m.type === 'transition');
if (t?.type === 'transition') {
expect(t.fields.map(f => f.name)).toEqual(['signed_at', 'hlc']);
}
});
});
// Cycle 59: `state as <MessageName> { ... }` to override the
// .proto generator's default `<SpeckName>State` message name.
// This unblocks federated-meetup's proto migration: the consumer
// Go code imports `pb.StateSnapshot`, not `pb.FederatedMeetupState`.
describe('state as <Name> (cycle 59)', () => {
it('should record messageName override on StateNode', () => {
const content = `speck FederatedMeetup {
state as StateSnapshot {
branch_id: Nat,
stewards: StringList
}
}`;
const ast = parseSpeckContent(content);
const state = ast.specks[0].members.find(m => m.type === 'state');
if (state?.type === 'state') {
expect(state.messageName).toBe('StateSnapshot');
expect(state.variables.map(v => v.name)).toEqual(['branch_id', 'stewards']);
}
});
it('should leave messageName undefined when no `as` clause is present', () => {
const content = `speck FederatedMeetup {
state: {
branch_id: Nat
}
}`;
const ast = parseSpeckContent(content);
const state = ast.specks[0].members.find(m => m.type === 'state');
if (state?.type === 'state') {
expect(state.messageName).toBeUndefined();
}
});
});
// Cycle 60: enum interfaces (e.g. CustodyTier) parse as `kind: 'enum'`
// and the .proto generator emits a real `enum X { ... }` block.
describe('enum interfaces (cycle 60)', () => {
it('should classify bare-identifier interfaces as enums', () => {
const content = `speck FederatedMeetup {
interface CustodyTier {
ColdHardware
HotSigning
ThresholdSplit
BackupOnly
Compromised
}
}`;
const ast = parseSpeckContent(content);
const tier = ast.specks[0].members.find(m => m.name === 'CustodyTier');
if (tier?.type === 'interface') {
expect(tier.kind).toBe('enum');
expect(tier.methods.map(m => m.name)).toEqual([
'ColdHardware', 'HotSigning', 'ThresholdSplit', 'BackupOnly', 'Compromised'
]);
}
});
});
// Cycle 61: top-of-file `event_suffix:` directive. When set, the .proto
// generator appends the suffix to every event message name.
describe('event_suffix directive (cycle 61)', () => {
it('should record eventSuffix on the SpeckNode', () => {
const content = `speck FederatedMeetup {
event_suffix: "Payload"
event CreateGroup { name: String }
}`;
const ast = parseSpeckContent(content);
expect(ast.specks[0].eventSuffix).toBe('Payload');
});
it('should leave eventSuffix undefined when not set', () => {
const content = `speck FederatedMeetup {
event CreateGroup { name: String }
}`;
const ast = parseSpeckContent(content);
expect(ast.specks[0].eventSuffix).toBeUndefined();
});
it('should tolerate quoted and bare values', () => {
const a = parseSpeckContent('speck A {\n event_suffix: "Payload"\n}');
const b = parseSpeckContent('speck B {\n event_suffix: Payload\n}');
expect(a.specks[0].eventSuffix).toBe('Payload');
expect(b.specks[0].eventSuffix).toBe('Payload');
});
});
// Cycle 62: inline `//` comments on field declarations were bleeding
// into the type expression. Real federated-meetup had:
// mesh_ip: Bytes // 4 bytes (IPv4 overlay)
// emitted as `Bytes // 4 bytes (IPv4 overlay) mesh_ip = 2;` —
// broken syntax. The fix strips the comment before parsing the type.
describe('inline comment stripping (cycle 62)', () => {
it('should strip inline // comments from event field types', () => {
const content = `speck One {
event InitialMeshPeer {
host_wg_key: Bytes, // 32 bytes
mesh_ip: Bytes // 4 bytes (IPv4 overlay)
}
}`;
const ast = parseSpeckContent(content);
const ev = ast.specks[0].members.find(m => m.name === 'InitialMeshPeer');
if (ev?.type === 'event') {
const meshIp = ev.fields.find(f => f.name === 'mesh_ip');
expect(meshIp?.type.name).toBe('Bytes');
expect(meshIp?.type.name).not.toContain('IPv4');
}
});
it('should strip inline // comments from interface field types', () => {
const content = `speck One {
interface InitialMeshPeer {
host_wg_key: Bytes, // X25519
mesh_ip: Bytes // 4 bytes (IPv4 overlay)
}
}`;
const ast = parseSpeckContent(content);
const iface = ast.specks[0].members.find(m => m.name === 'InitialMeshPeer');
if (iface?.type === 'interface') {
const meshIp = iface.fields.find(f => f.name === 'mesh_ip');
expect(meshIp?.type.name).toBe('Bytes');
expect(meshIp?.type.name).not.toContain('IPv4');
}
});
});
// Cycle 63: 'state as <Name> { ... }' must dispatch through the
// same parseStateBlockMultiline path as 'state: { ... }'. Cycle 59
// added the parser-side extraction of the `as` clause; this test
// confirms the block-dispatcher also routes the new header form.
describe('state as <Name> dispatch (cycle 63)', () => {
it('should dispatch state as StateSnapshot to parseStateBlockMultiline', () => {
const content = `speck FederatedMeetup {
state as StateSnapshot {
branch_id: Nat
}
}`;
const ast = parseSpeckContent(content);
const state = ast.specks[0].members.find(m => m.type === 'state');
if (state?.type === 'state') {
expect(state.messageName).toBe('StateSnapshot');
expect(state.variables.map(v => v.name)).toEqual(['branch_id']);
}
});
});
// Cycle 65: default-value syntax `= <expr>` on event fields was
// bleeding into the type expression. Real federated-meetup has
// initial_mesh_peers: List<InitialMeshPeer> = []
// emitted as `List<InitialMeshPeer> = [] initial_mesh_peers = 1;`
// which protoc rejects. The fix strips `= <expr>` from the type
// before parsing (the default is a Speckl semantic; the .proto wire
// format has no place for it).
describe('default value stripping (cycle 65)', () => {
it('should strip `= []` from event field type expressions', () => {
const content = `speck One {
event CreateGroup {
initial_mesh_peers: List<InitialMeshPeer> = []
}
}`;
const ast = parseSpeckContent(content);
const ev = ast.specks[0].members.find(m => m.name === 'CreateGroup');
if (ev?.type === 'event') {
const f = ev.fields[0];
expect(f.name).toBe('initial_mesh_peers');
expect(f.type.type).toBe('list');
expect(f.type.elementType?.name).toBe('InitialMeshPeer');
// The full type string should not contain '= []' anywhere — verify
// via the elementType name and the parent's name (both undefined
// for List, so we check the parser did not preserve the default
// in any visible field).
const asAny = f.type as any;
expect(JSON.stringify(asAny)).not.toContain('= []');
}
});
});
// Cycle 73: List<T> fields in interface records must be preserved in the AST.
// Previously the generator emitted empty type for these fields because
// it called speckTypeToProto(f.type.name) which returns '' when .name is
// undefined (List/Map/Set nodes use .elementType/.keyType/.valueType,
// not .name). The generator was fixed, but this test locks in the parser
// behavior so a regression is caught early.
describe('List<T> in interface record fields (cycle 73)', () => {
it('should parse List<T> fields in interface records', () => {
const content = `speck One {
interface Container {
items: List<Ticket>,
names: List<String>
}
interface Ticket {
id: String
}
}`;
const ast = parseSpeckContent(content);
const iface = ast.specks[0].members.find(m => m.name === 'Container');
expect(iface).toBeDefined();
if (iface?.type === 'interface') {
expect(iface.fields).toBeDefined();
expect(iface.fields.length).toBe(2);
expect(iface.fields[0].name).toBe('items');
expect(iface.fields[0].type.type).toBe('list');
expect(iface.fields[0].type.elementType?.name).toBe('Ticket');
expect(iface.fields[1].name).toBe('names');
expect(iface.fields[1].type.type).toBe('list');
expect(iface.fields[1].type.elementType?.name).toBe('String');
}
});
});
}); });

165
compiler/dist/__tests__/compiler.test.js vendored
View file

@ -1,13 +1,10 @@
import { describe, it, expect, beforeAll } from 'vitest'; import { describe, it, expect, beforeAll } from 'vitest';
import fs from 'fs'; import fs from 'fs';
import path from 'path'; import path from 'path';
import { fileURLToPath } from 'url';
import { execSync } from 'child_process';
import { parseSpeckFile } from '../parser.js'; import { parseSpeckFile } from '../parser.js';
import { generateProvenanceGraph } from '../generators/provenance.js'; import { generateProvenanceGraph } from '../generators/provenance.js';
import { generateCycloneDX } from '../generators/cyclonedx.js'; import { generateCycloneDX } from '../generators/cyclonedx.js';
import { generateSPDX } from '../generators/spdx.js'; import { generateSPDX } from '../generators/spdx.js';
const __dirname = path.dirname(fileURLToPath(import.meta.url));
describe('Compiler E2E', () => { describe('Compiler E2E', () => {
let ast; let ast;
const testOutputDir = './test-output'; const testOutputDir = './test-output';
@ -18,7 +15,7 @@ describe('Compiler E2E', () => {
} }
}); });
it('should parse RetryHandler.speck', () => { it('should parse RetryHandler.speck', () => {
const specPath = path.join(__dirname, '..', '..', '..', 'examples', 'RetryHandler.speck'); const specPath = path.join(process.cwd(), '..', 'examples', 'RetryHandler.speck');
ast = parseSpeckFile(specPath); ast = parseSpeckFile(specPath);
expect(ast).toBeDefined(); expect(ast).toBeDefined();
expect(ast.specks).toBeDefined(); expect(ast.specks).toBeDefined();
@ -57,164 +54,4 @@ describe('Compiler E2E', () => {
expect(spdx.spdx).toBeDefined(); expect(spdx.spdx).toBeDefined();
}); });
}); });
// ---------------------------------------------------------------------------
// Regression tests for Z3 / TypeScript / Rust expression translation fixes.
//
// These tests compile the FederatedMeetupProduct spec against each backend
// (z3, typescript, rust) and assert that the generated output contains the
// expected translated patterns. They guard against regressions in:
// - implies() argument preservation (Z3 + TS + Rust)
// - multi-level field access flattening (Z3)
// - len()/length() normalization (Z3)
// - nil → speckl_nil translation (Z3)
// - != → (distinct X Y) wrapping (Z3)
// - constraint checks emitting real every() / iter().all() (TS + Rust)
// - 'in' operator → .has() in verify expressions (TS)
// - multiple verify blocks all emitted (memberKey dedup fix) (TS + Rust)
// ---------------------------------------------------------------------------
const SPEC_PATH = '/home/sscoble/projects/federated-meetup/specs/FederatedMeetupProduct.speckdl';
const OUT_DIR = './out'; // CLI writes to ./out relative to compiler cwd
const COMPILER_DIR = '/home/sscoble/speckl/compiler';
describe('Z3 / TS / Rust expression translation regressions', () => {
let z3Output;
let tsOutput;
let rustOutput;
beforeAll(() => {
// Clean out directory to avoid stale output
execSync(`rm -rf ${OUT_DIR}`, { cwd: COMPILER_DIR });
execSync(`mkdir -p ${OUT_DIR}`, { cwd: COMPILER_DIR });
// Compile to all three targets
execSync(`npx tsx src/index.ts ${SPEC_PATH} --target z3 --output ${OUT_DIR}`, { cwd: COMPILER_DIR, stdio: 'pipe' });
z3Output = fs.readFileSync(path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct.smt2'), 'utf-8');
execSync(`npx tsx src/index.ts ${SPEC_PATH} --target typescript --output ${OUT_DIR}`, { cwd: COMPILER_DIR, stdio: 'pipe' });
tsOutput = fs.readFileSync(path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct.ts'), 'utf-8');
execSync(`npx tsx src/index.ts ${SPEC_PATH} --target rust --output ${OUT_DIR}`, { cwd: COMPILER_DIR, stdio: 'pipe' });
rustOutput = fs.readFileSync(path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct', 'src', 'lib.rs'), 'utf-8');
}, 120_000);
// 1. Z3: implies() preserves both arguments → (=> P Q) not (=> true true)
it('Z3: implies() emits (=> P Q) preserving both arguments', () => {
expect(z3Output).toContain('(=>');
expect(z3Output).toContain('(=> (= o_status Refunded) (distinct o_refunded_at speckl_nil))');
// Ensure we did NOT regress to (=> true true)
expect(z3Output).not.toContain('(=> true true)');
expect(z3Output).not.toContain('(=> true');
});
// 2. Z3: multi-level field access m.price.amount → m_price_amount
it('Z3: multi-level field access m.price.amount flattens to m_price_amount', () => {
expect(z3Output).toContain('m_price_amount');
// Ensure we did NOT regress to single-level m_price or bare m.price.amount
expect(z3Output).not.toContain('m.price.amount');
// The constraint m_price_amount >= 0 should be present
expect(z3Output).toContain('(>= m_price_amount 0)');
});
// 3. Z3: len() handled same as length() → speckl_len_Int
it('Z3: len() is translated to speckl_len_Int (same as length())', () => {
// The spec uses len(m.price.currency) — should become speckl_len_Int
expect(z3Output).toContain('(speckl_len_Int m_price_currency)');
// Ensure we did NOT regress to bare len() or length()
expect(z3Output).not.toMatch(/\blen\s*\(/);
expect(z3Output).not.toMatch(/\blength\s*\(/);
});
// 4. Z3: nil translated to speckl_nil
it('Z3: nil is translated to speckl_nil sentinel', () => {
expect(z3Output).toContain('(declare-const speckl_nil Int)');
expect(z3Output).toContain('speckl_nil');
// Ensure we did NOT regress to bare nil / null
expect(z3Output).not.toMatch(/\bnil\b/);
});
// 5. Z3: != produces (distinct X Y) not bare 'distinct'
it('Z3: != produces wrapped (distinct X Y) not bare distinct', () => {
// The constraint g.hosting_tier != Free should emit (distinct g_hosting_tier Free)
expect(z3Output).toContain('(distinct g_hosting_tier Free)');
// Ensure we did NOT regress to bare 'distinct g_hosting_tier Free' without parens
// (the fix wraps the operator in parens)
// A bare distinct would look like "g_hosting_tier distinct Free" without surrounding parens
expect(z3Output).not.toMatch(/[^(]\w+\s+distinct\s+\w+/);
});
// 6. TS: implies(p,q) → (!p || q) not (p || q)
it('TS: implies(p, q) translates to (!p || q), not (p || q)', () => {
// constraint 6: implies(o.status == Refunded, o.refunded_at != nil)
// Should become (!(o.status === ...) || (o.refunded_at !== ...))
expect(tsOutput).toContain('(!(');
expect(tsOutput).toContain('||');
// The specific pattern: (!(o.status === ... || (o.refunded_at !== nil))
expect(tsOutput).toMatch(/!\(o\.status === .* \|\| \(o\.refunded_at !== /);
// Ensure the CODE (not comments) has negation on p.
// A regression would have `return this.orders.every((o: any) => (o.status ===`
// (without the `!(` negation before `o.status`).
// Strip comments to avoid matching the original spec text in comments.
const tsNoComments = tsOutput.replace(/^\s*\/\/.*$/gm, '');
// Positive: the every() body starts with (!(o.status — the (! is the negation
expect(tsNoComments).toMatch(/every\(\(o:\s*any\)\s*=>\s*\(!\(o\.status/);
// Negative: a regression would have every((o: any) => (o.status without the ! negation
expect(tsNoComments).not.toMatch(/every\(\(o:\s*any\)\s*=>\s*\(o\.status/);
});
// 7. TS: constraint checks emit real every() not return true
it('TS: constraint checks emit real .every() calls, not return true', () => {
expect(tsOutput).toContain('.every(');
// Multiple constraints use every() — at least 8 constraints
const everyCount = (tsOutput.match(/\.every\(/g) || []).length;
expect(everyCount).toBeGreaterThanOrEqual(8);
// Ensure we did NOT regress to `return true` stubs
// A stub would have checkConstraintN() { return true; }
expect(tsOutput).not.toMatch(/checkConstraint\d+\(\):\s*boolean\s*\{\s*return\s*true\s*;\s*\}/);
});
// 8. TS: 'in' operator in verify expressions → .has() not raw 'in'
it('TS: "in" operator in verify expressions translates to .has(), not raw in', () => {
// V1: always(implies(event == PurchaseTicket, ticket_id in tickets))
// Should become tickets.has(ticket_id)
expect(tsOutput).toContain('.has(');
expect(tsOutput).toContain('tickets.has(ticket_id)');
// Ensure we did NOT regress to raw 'in' operator (JS `in` checks property keys, not membership).
// A regression would look like `ticket_id in tickets` in CODE (not comments).
// Strip comments to avoid matching the original spec text in comments.
const tsNoComments = tsOutput.replace(/^\s*\/\/.*$/gm, '');
expect(tsNoComments).not.toMatch(/\bticket_id\s+in\s+tickets\b/);
});
// 9. TS/Rust: multiple verify blocks all emitted (memberKey dedup fix)
it('TS: all 6 verify blocks are emitted (memberKey dedup fix)', () => {
// The spec has 6 verify blocks; previously dedup killed all but the first
expect(tsOutput).toContain('verify1');
expect(tsOutput).toContain('verify2');
expect(tsOutput).toContain('verify3');
expect(tsOutput).toContain('verify4');
expect(tsOutput).toContain('verify5');
expect(tsOutput).toContain('verify6');
expect(tsOutput).not.toContain('verify7'); // only 6 verify blocks in spec
});
it('Rust: all 6 verify blocks are emitted (memberKey dedup fix)', () => {
expect(rustOutput).toContain('verify_1');
expect(rustOutput).toContain('verify_2');
expect(rustOutput).toContain('verify_3');
expect(rustOutput).toContain('verify_4');
expect(rustOutput).toContain('verify_5');
expect(rustOutput).toContain('verify_6');
expect(rustOutput).not.toContain('verify_7');
});
// 10. Rust: constraint checks emit iter().all() not return true
it('Rust: constraint checks emit iter().all(), not return true stubs', () => {
expect(rustOutput).toContain('.iter().all(');
// Multiple constraints use iter().all() — at least 8 constraints
const iterAllCount = (rustOutput.match(/\.iter\(\)\.all\(/g) || []).length;
expect(iterAllCount).toBeGreaterThanOrEqual(8);
// Ensure we did NOT regress to `return true` stubs
expect(rustOutput).not.toMatch(/check_invariant_\d+\(&self\)\s*->\s*bool\s*\{\s*true\s*\}/);
});
// 11. Rust: implies() → (!p || q) in Rust
it('Rust: implies(p, q) translates to (!p || q) in Rust', () => {
// constraint 6: implies(o.status == Refunded, o.refunded_at != nil)
// Should become (!(o.status == ... || (o.refunded_at != ...))
expect(rustOutput).toContain('(!(');
expect(rustOutput).toMatch(/!\(o\.status == .* \|\| \(o\.refunded_at != /);
// Ensure the CODE (not comments) has negation on p.
// A regression would have `self.orders.iter().all(|o| (o.status ==`
// (without the `!(` negation before `o.status`).
// Strip comments to avoid matching the original spec text in comments.
const rustNoComments = rustOutput.replace(/^\s*\/\/.*$/gm, '');
// Positive: the iter().all() body starts with (!(o.status — the (! is the negation
expect(rustNoComments).toMatch(/iter\(\)\.all\(\|o\|\s*\(!\(o\.status/);
// Negative: a regression would have iter().all(|o| (o.status without the ! negation
expect(rustNoComments).not.toMatch(/iter\(\)\.all\(\|o\|\s*\(o\.status/);
});
});
//# sourceMappingURL=compiler.test.js.map //# sourceMappingURL=compiler.test.js.map

2
compiler/dist/__tests__/compiler.test.js.map vendored
View file

File diff suppressed because one or more lines are too long

11
compiler/dist/index.js vendored
View file

@ -6,7 +6,6 @@ import { generateProvenanceGraph } from './generators/provenance.js';
import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateCycloneDX } from './generators/cyclonedx.js';
import { generateSPDX } from './generators/spdx.js'; import { generateSPDX } from './generators/spdx.js';
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
import { generateProtobuf } from './generators/protobuf.js';
import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
import { generateRust } from './generators/rust.js'; import { generateRust } from './generators/rust.js';
import fs from 'fs'; import fs from 'fs';
@ -42,7 +41,7 @@ async function main() {
alias: 't', alias: 't',
describe: 'Compilation target', describe: 'Compilation target',
type: 'string', type: 'string',
choices: ['typescript', 'z3', 'rust', 'protobuf', 'all'], choices: ['typescript', 'z3', 'rust', 'all'],
default: 'typescript', default: 'typescript',
}) })
.option('verify-depth', { .option('verify-depth', {
@ -85,14 +84,6 @@ async function main() {
console.log('\nGenerating Rust state machine...'); console.log('\nGenerating Rust state machine...');
generateRust(ast, options.outputDir); generateRust(ast, options.outputDir);
} }
// Generate protobuf schema if target is protobuf or all
// This is the load-bearing backend for the "no glue code" claim:
// the emitted .proto is the canonical wire format. Run `buf generate`
// on the output to produce Go/TS/Rust/C/Python/Java bindings.
if (options.target === 'protobuf' || options.target === 'all') {
console.log('\nGenerating protobuf schema (.proto)...');
generateProtobuf(ast, options.outputDir);
}
// Always generate provenance (it's the core output) if not z3-only or rust-only // Always generate provenance (it's the core output) if not z3-only or rust-only
if (options.target !== 'z3' && options.target !== 'rust') { if (options.target !== 'z3' && options.target !== 'rust') {
console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');

2
compiler/dist/index.js.map vendored
View file

@ -1 +1 @@
{"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,gBAAgB,EAAE,MAAM,0BAA0B,CAAC;AAC5D,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,MAAM,EAAE,UAAU,EAAE,KAAK,CAAC;YACxD,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAA2D;QACxE,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,uDAAuD;IACvD,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QAC1D,OAAO,CAAC,GAAG,CAAC,oCAAoC,CAAC,CAAC;QAClD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IACvC,CAAC;IAED,wDAAwD;IACxD,iEAAiE;IACjE,sEAAsE;IACtE,8DAA8D;IAC9D,IAAI,OAAO,CAAC,MAAM,KAAK,UAAU,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QAC9D,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,gBAAgB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAC3C,CAAC;IAED,gFAAgF;IAChF,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,gEAAgE;IAChE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"} {"version":3,"file":"index.js","sourceRoot":"","sources":["../src/index.ts"],"names":[],"mappings":";AAEA,OAAO,KAAK,MAAM,OAAO,CAAC;AAC1B,OAAO,EAAE,OAAO,EAAE,MAAM,eAAe,CAAC;AACxC,OAAO,EAAE,cAAc,EAAE,MAAM,aAAa,CAAC;AAC7C,OAAO,EAAE,uBAAuB,EAAE,MAAM,4BAA4B,CAAC;AACrE,OAAO,EAAE,iBAAiB,EAAE,MAAM,2BAA2B,CAAC;AAC9D,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,8BAA8B,EAAE,MAAM,0CAA0C,CAAC;AAC1F,OAAO,EAAE,UAAU,EAAa,yBAAyB,EAAE,mBAAmB,EAAE,MAAM,oBAAoB,CAAC;AAC3G,OAAO,EAAE,YAAY,EAAE,MAAM,sBAAsB,CAAC;AACpD,OAAO,EAAE,MAAM,IAAI,CAAC;AACpB,OAAO,IAAI,MAAM,MAAM,CAAC;AASxB,KAAK,UAAU,IAAI;IACjB,uDAAuD;IACvD,MAAM,WAAW,GAAG,IAAI,CAAC,IAAI,CAAC,IAAI,CAAC,OAAO,CAAC,IAAI,GAAG,CAAC,MAAM,CAAC,IAAI,CAAC,GAAG,CAAC,CAAC,QAAQ,CAAC,EAAE,IAAI,EAAE,eAAe,CAAC,CAAC;IACtG,IAAI,EAAE,CAAC,UAAU,CAAC,WAAW,CAAC,EAAE,CAAC;QAC/B,IAAI,CAAC;YACH,MAAM,EAAE,QAAQ,EAAE,GAAG,MAAM,MAAM,CAAC,eAAe,CAAC,CAAC;YACnD,QAAQ,CAAC,SAAS,WAAW,GAAG,EAAE,EAAE,KAAK,EAAE,SAAS,EAAE,CAAC,CAAC;QAC1D,CAAC;QAAC,MAAM,CAAC;YACP,OAAO,CAAC,KAAK,CAAC,oDAAoD,CAAC,CAAC;YACpE,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;QAClB,CAAC;IACH,CAAC;IAED,MAAM,IAAI,GAAG,MAAM,KAAK,CAAC,OAAO,CAAC,OAAO,CAAC,IAAI,CAAC,CAAC;SAC5C,OAAO,CAAC,WAAW,EAAE,iCAAiC,EAAE,CAAC,QAAQ,EAAE,EAAE;QACpE,OAAO,QAAQ;aACZ,UAAU,CAAC,MAAM,EAAE;YAClB,QAAQ,EAAE,yBAAyB;YACnC,IAAI,EAAE,QAAQ;YACd,YAAY,EAAE,IAAI;SACnB,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,yCAAyC;YACnD,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,OAAO;SACjB,CAAC;aACD,MAAM,CAAC,QAAQ,EAAE;YAChB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,oBAAoB;YAC9B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,YAAY,EAAE,IAAI,EAAE,MAAM,EAAE,KAAK,CAAC;YAC5C,OAAO,EAAE,YAAqB;SAC/B,CAAC;aACD,MAAM,CAAC,cAAc,EAAE;YACtB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,kDAAkD;YAC5D,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,EAAE;SACZ,CAAC;aACD,MAAM,CAAC,YAAY,EAAE;YACpB,KAAK,EAAE,GAAG;YACV,QAAQ,EAAE,mBAAmB;YAC7B,IAAI,EAAE,QAAQ;YACd,OAAO,EAAE,CAAC,KAAK,EAAE,MAAM,EAAE,MAAM,CAAC;YAChC,OAAO,EAAE,MAAe;SACzB,CAAC,CAAC;IACP,CAAC,CAAC;SACD,IAAI,EAAE;SACN,IAAI,CAAC;IAER,MAAM,IAAI,GAAG,IAAI,CAAC,IAAc,CAAC;IACjC,MAAM,OAAO,GAAG;QACd,SAAS,EAAE,IAAI,CAAC,SAAmB;QACnC,SAAS,EAAE,IAAI,CAAC,SAAoC;QACpD,MAAM,EAAE,IAAI,CAAC,MAA8C;QAC3D,WAAW,EAAE,IAAI,CAAC,WAAqB;KACxC,CAAC;IAEF,OAAO,CAAC,GAAG,CAAC,aAAa,IAAI,KAAK,CAAC,CAAC;IAEpC,uBAAuB;IACvB,MAAM,GAAG,GAAG,cAAc,CAAC,IAAI,CAAC,CAAC;IAEjC,MAAM,UAAU,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC;IACrC,MAAM,WAAW,GAAG,GAAG,CAAC,MAAM,CAAC,MAAM,CAAC,CAAC,GAAG,EAAE,CAAC,EAAE,EAAE,CAAC,GAAG,GAAG,CAAC,CAAC,OAAO,CAAC,MAAM,EAAE,CAAC,CAAC,CAAC;IAC7E,OAAO,CAAC,GAAG,CAAC,4BAA4B,UAAU,cAAc,WAAW,YAAY,CAAC,CAAC;IAEzF,iCAAiC;IACjC,IAAI,CAAC,EAAE,CAAC,UAAU,CAAC,OAAO,CAAC,SAAS,CAAC,EAAE,CAAC;QACtC,EAAE,CAAC,SAAS,CAAC,OAAO,CAAC,SAAS,EAAE,EAAE,SAAS,EAAE,IAAI,EAAE,CAAC,CAAC;IACvD,CAAC;IAED,oFAAoF;IACpF,MAAM,SAAS,GAAG,EAAE,CAAC,YAAY,CAAC,IAAI,EAAE,OAAO,CAAC,CAAC;IAEjD,uDAAuD;IACvD,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QAC1D,OAAO,CAAC,GAAG,CAAC,oCAAoC,CAAC,CAAC;QAClD,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IACvC,CAAC;IAED,gFAAgF;IAChF,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,OAAO,CAAC,GAAG,CAAC,mDAAmD,CAAC,CAAC;QACjE,uBAAuB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;IAClD,CAAC;IAED,8CAA8C;IAC9C,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,KAAK,EAAE,CAAC;QACxD,OAAO,CAAC,GAAG,CAAC,6BAA6B,CAAC,CAAC;QAC3C,kDAAkD;QAClD,KAAK,MAAM,KAAK,IAAI,GAAG,CAAC,MAAM,EAAE,CAAC;YAC/B,MAAM,UAAU,GAAG,yBAAyB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YACpE,MAAM,QAAQ,GAAG,mBAAmB,CAAC,SAAS,EAAE,KAAK,CAAC,IAAI,CAAC,CAAC;YAC5D,kDAAkD;YACjD,KAAa,CAAC,WAAW,GAAG,UAAU,CAAC;YACvC,KAAa,CAAC,KAAK,GAAG,QAAQ,CAAC;QAClC,CAAC;QACD,MAAM,SAAS,GAAc,EAAE,WAAW,EAAE,OAAO,CAAC,WAAW,EAAE,CAAC;QAClE,UAAU,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,EAAE,SAAS,CAAC,CAAC;IAChD,CAAC;IAED,gEAAgE;IAChE,IAAI,OAAO,CAAC,MAAM,KAAK,IAAI,IAAI,OAAO,CAAC,MAAM,KAAK,MAAM,EAAE,CAAC;QACzD,OAAO,CAAC,GAAG,CAAC,0CAA0C,CAAC,CAAC;QACxD,8BAA8B,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAEvD,yCAAyC;QACzC,IAAI,OAAO,CAAC,SAAS,KAAK,KAAK,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YAChE,OAAO,CAAC,GAAG,CAAC,+BAA+B,CAAC,CAAC;YAC7C,iBAAiB,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QAC5C,CAAC;QAED,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,IAAI,OAAO,CAAC,SAAS,KAAK,MAAM,EAAE,CAAC;YACjE,OAAO,CAAC,GAAG,CAAC,0BAA0B,CAAC,CAAC;YACxC,YAAY,CAAC,GAAG,EAAE,OAAO,CAAC,SAAS,CAAC,CAAC;QACvC,CAAC;IACH,CAAC;IAED,OAAO,CAAC,GAAG,CAAC,mCAAmC,OAAO,CAAC,SAAS,GAAG,CAAC,CAAC;AACvE,CAAC;AAED,IAAI,EAAE,CAAC,KAAK,CAAC,CAAC,GAAG,EAAE,EAAE;IACnB,OAAO,CAAC,KAAK,CAAC,qBAAqB,EAAE,GAAG,CAAC,CAAC;IAC1C,OAAO,CAAC,IAAI,CAAC,CAAC,CAAC,CAAC;AAClB,CAAC,CAAC,CAAC"}

47
compiler/dist/parser.d.ts vendored
View file

@ -2,12 +2,6 @@ export interface SpeckNode {
type: 'speck'; type: 'speck';
name: string; name: string;
members: MemberNode[]; members: MemberNode[];
version?: string;
author?: string;
license?: string;
protoPackage?: string;
goPackage?: string;
eventSuffix?: string;
} }
export interface ImportNode { export interface ImportNode {
type: 'import'; type: 'import';
@ -35,28 +29,10 @@ export interface VerifyNode {
temporalExpr: string; temporalExpr: string;
depth?: number; depth?: number;
} }
export interface InterfaceField {
name: string;
type: TypeExpr;
}
export interface RpcMethod {
name: string;
requestType: string;
responseType: string;
clientStreaming?: boolean;
serverStreaming?: boolean;
}
export interface ServiceNode {
type: 'service';
name: string;
rpcs: RpcMethod[];
}
export interface InterfaceNode { export interface InterfaceNode {
type: 'interface'; type: 'interface';
name: string; name: string;
kind: 'enum' | 'record' | 'service' | 'mixed';
methods: MethodSignature[]; methods: MethodSignature[];
fields: InterfaceField[];
} }
export interface MethodSignature { export interface MethodSignature {
name: string; name: string;
@ -74,26 +50,6 @@ export interface EventNode {
type: TypeExpr; type: TypeExpr;
}[]; }[];
} }
export interface OneofNode {
type: 'oneof';
name: string;
variants: OneofVariant[];
}
export interface OneofVariant {
fieldName: string;
typeName: string;
}
export interface TransitionNode {
type: 'transition';
name: string;
fields: TransitionField[];
payloadOneof?: string;
typeDiscriminator?: string;
}
export interface TransitionField {
name: string;
type: TypeExpr;
}
export interface ProvenanceNode { export interface ProvenanceNode {
type: 'provenance'; type: 'provenance';
clauses: ProvenanceClause[]; clauses: ProvenanceClause[];
@ -147,7 +103,6 @@ export interface BOMNode {
export interface StateNode { export interface StateNode {
type: 'state'; type: 'state';
variables: StateVar[]; variables: StateVar[];
messageName?: string;
} }
export interface StateVar { export interface StateVar {
name: string; name: string;
@ -201,7 +156,7 @@ export type ActionStatement = {
type: 'ifblock'; type: 'ifblock';
raw: string; raw: string;
}; };
export type MemberNode = ImportNode | InputNode | OutputNode | ConstraintNode | VerifyNode | InterfaceNode | EventNode | OneofNode | TransitionNode | ProvenanceNode | ReviewNode | DerivesNode | SatisfiesNode | AuthorNode | SourceNode | BOMNode | StateNode | InitNode | ActionNode | ServiceNode; export type MemberNode = ImportNode | InputNode | OutputNode | ConstraintNode | VerifyNode | InterfaceNode | EventNode | ProvenanceNode | ReviewNode | DerivesNode | SatisfiesNode | AuthorNode | SourceNode | BOMNode | StateNode | InitNode | ActionNode;
export interface TypeExpr { export interface TypeExpr {
type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident'; type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident';
name?: string; name?: string;

2
compiler/dist/parser.d.ts.map vendored
View file

File diff suppressed because one or more lines are too long

444
compiler/dist/parser.js vendored
View file

@ -51,13 +51,6 @@ function parseSpeck(lines, startIndex) {
return null; return null;
const name = headerMatch[1]; const name = headerMatch[1];
const members = []; const members = [];
// Cycle 73: refactored from static-field hack to local-object pattern.
// Previously, proto_package / go_package / event_suffix were stored
// on (parseSpeck as any)._protoPackage etc — static function fields
// that leaked between parse calls. Now collected in a local metadata
// object and spread into the return value. No reset needed because
// the object is local to this invocation.
const metadata = {};
let i = startIndex + 1; let i = startIndex + 1;
let braceCount = 1; let braceCount = 1;
while (i < lines.length && braceCount > 0) { while (i < lines.length && braceCount > 0) {
@ -67,35 +60,12 @@ function parseSpeck(lines, startIndex) {
i++; i++;
continue; continue;
} }
// ── Top-of-file protobuf metadata directives ────────────────
// These attach to the SpeckNode and are NOT emitted as members.
// Format: `key: value` (string values may be quoted or bare).
// `author:`, `version:`, `license:` continue to be parsed as members
// (AuthorNode, etc.) for backward compatibility with the existing
// PROV-O / CycloneDX generators.
const metaMatch = line.match(/^(proto_package|go_package|event_suffix)\s*:\s*(.+)$/);
if (metaMatch) {
// Strip surrounding quotes if present
const value = metaMatch[2].trim().replace(/^['"]|['"]$/g, '');
if (metaMatch[1] === 'proto_package') {
metadata.protoPackage = value;
}
else if (metaMatch[1] === 'go_package') {
metadata.goPackage = value;
}
else if (metaMatch[1] === 'event_suffix') {
metadata.eventSuffix = value;
}
i++;
continue;
}
// Count braces on this line first // Count braces on this line first
const openCount = (rawLine.match(/{/g) || []).length; const openCount = (rawLine.match(/{/g) || []).length;
const closeCount = (rawLine.match(/}/g) || []).length; const closeCount = (rawLine.match(/}/g) || []).length;
// Check for block-opening members (those that open braces on the same line) // Check for block-opening members (those that open braces on the same line)
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ', const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
'state {', 'init {', 'verify ', 'constraint ', 'input:', 'output:', 'service ', 'oneof ', 'transition ', 'state {', 'init {', 'verify ', 'constraint '];
'state as '];
const isBlockStarter = blockStarters.some(s => line.startsWith(s)); const isBlockStarter = blockStarters.some(s => line.startsWith(s));
if (isBlockStarter && openCount > 0) { if (isBlockStarter && openCount > 0) {
// Multi-line block: parse it and skip to its end // Multi-line block: parse it and skip to its end
@ -114,8 +84,8 @@ function parseSpeck(lines, startIndex) {
continue; continue;
} }
// Handle constraint/verify blocks that may span multiple lines without braces // Handle constraint/verify blocks that may span multiple lines without braces
// (e.g. constraint Name: forall r in [0..4]:, verify: always(implies(\n ...\n))) // (e.g. constraint Name: forall r in [0..4]:)
if (line.startsWith('constraint ') || line.startsWith('verify ') || line.startsWith('verify:')) { if (line.startsWith('constraint ') || line.startsWith('verify ')) {
const member = parseMultiLineConstraintVerify(lines, i); const member = parseMultiLineConstraintVerify(lines, i);
if (member) { if (member) {
members.push(member); members.push(member);
@ -128,8 +98,7 @@ function parseSpeck(lines, startIndex) {
nextLine.startsWith('state') || nextLine.startsWith('init') || nextLine.startsWith('state') || nextLine.startsWith('init') ||
nextLine.startsWith('action ') || nextLine.startsWith('event ') || nextLine.startsWith('action ') || nextLine.startsWith('event ') ||
nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') || nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') ||
nextLine.startsWith('service ') || nextLine.startsWith('bom ') || nextLine.startsWith('bom ') || nextLine.startsWith('}') ||
nextLine.startsWith('}') ||
nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) { nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) {
break; break;
} }
@ -151,10 +120,7 @@ function parseSpeck(lines, startIndex) {
} }
i++; i++;
} }
return { type: 'speck', name, members, return { type: 'speck', name, members };
protoPackage: metadata.protoPackage,
goPackage: metadata.goPackage,
eventSuffix: metadata.eventSuffix };
} }
function findBlockEnd(lines, startIndex, startBraceCount) { function findBlockEnd(lines, startIndex, startBraceCount) {
let braceCount = startBraceCount; let braceCount = startBraceCount;
@ -203,12 +169,6 @@ function parseMemberBlock(lines, startIndex) {
if (firstLine.startsWith('state {') || firstLine === 'state') { if (firstLine.startsWith('state {') || firstLine === 'state') {
return parseStateBlockMultiline(lines, startIndex, startBraceCount); return parseStateBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('state as ')) {
// Cycle 63: `state as <MessageName> { ... }` form must dispatch
// through the same state-block parser so the `as` override on the
// first line is captured.
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('init:')) { if (firstLine.startsWith('init:')) {
return parseInitBlockMultiline(lines, startIndex, startBraceCount); return parseInitBlockMultiline(lines, startIndex, startBraceCount);
} }
@ -224,15 +184,6 @@ function parseMemberBlock(lines, startIndex) {
if (firstLine.startsWith('interface ')) { if (firstLine.startsWith('interface ')) {
return parseInterfaceBlockMultiline(lines, startIndex, startBraceCount); return parseInterfaceBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('oneof ')) {
return parseOneofBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('transition ')) {
return parseTransitionBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('service ')) {
return parseServiceBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('provenance ')) { if (firstLine.startsWith('provenance ')) {
return { type: 'provenance', clauses: [] }; return { type: 'provenance', clauses: [] };
} }
@ -245,64 +196,8 @@ function parseMemberBlock(lines, startIndex) {
if (firstLine.startsWith('constraint ')) { if (firstLine.startsWith('constraint ')) {
return parseConstraintBlockMultiline(lines, startIndex, startBraceCount); return parseConstraintBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('input:') || firstLine.startsWith('output:')) {
return parseInputOutputBlock(lines, startIndex, startBraceCount);
}
return null; return null;
} }
/**
* Parse a multi-line `input: { ... }` or `output: { ... }` block.
*
* The first line opens with `input: {` or `output: {` and the matching `}`
* may be many lines later (with field declarations on intermediate lines).
* We collect all lines up to the matching `}` (brace-counted) and join the
* inner content into a single record string that `parseTypeExpr` already
* knows how to handle.
*/
function parseInputOutputBlock(lines, startIndex, startBraceCount) {
const header = lines[startIndex].trim();
const isInput = header.startsWith('input:');
const kind = isInput ? 'input' : 'output';
// Collect inner content lines, brace-counting across the block.
// startBraceCount is the brace count on the header line (1 for `input: {`).
// We need to find the line where braceCount returns to 0 (i.e. the closing `}`).
const innerLines = [];
let braceCount = 0;
let i = startIndex;
// First pass: extract inner content from header line (everything after the first `{`).
const headerLine = lines[startIndex].trim();
const headerNoComment = headerLine.replace(/\/\/.*$/, '').trim();
const openIdx = headerNoComment.indexOf('{');
if (openIdx >= 0) {
const after = headerNoComment.substring(openIdx + 1).trim();
if (after)
innerLines.push(after);
}
braceCount = 1; // we're inside one `{` from the header
i = startIndex + 1;
while (i < lines.length && braceCount > 0) {
const raw = lines[i];
const stripped = raw.trim();
// Strip line comments (//...) — they cannot be inside a type expression.
const noComment = stripped.replace(/\/\/.*$/, '').trim();
for (const ch of noComment) {
if (ch === '{')
braceCount++;
else if (ch === '}')
braceCount--;
}
if (braceCount > 0 && noComment) {
// Inside the block — keep content (skip the closing `}` line itself).
innerLines.push(noComment);
}
i++;
}
// Join inner content with newlines; `parseTypeExpr`'s record branch
// splits on commas and matches `name: type` pairs.
const recordExpr = '{ ' + innerLines.join(' ') + ' }';
const typeExpr = parseTypeExpr(recordExpr);
return { type: kind, typeExpr };
}
function parseMember(line) { function parseMember(line) {
// input: // input:
if (line.startsWith('input:')) { if (line.startsWith('input:')) {
@ -342,14 +237,6 @@ function parseMember(line) {
if (line.startsWith('event ')) { if (line.startsWith('event ')) {
return parseEvent(line); return parseEvent(line);
} }
// oneof:
if (line.startsWith('oneof ')) {
return parseOneof(line);
}
// transition:
if (line.startsWith('transition ')) {
return parseTransition(line);
}
// provenance { // provenance {
if (line.startsWith('provenance ')) { if (line.startsWith('provenance ')) {
return { type: 'provenance', clauses: [] }; return { type: 'provenance', clauses: [] };
@ -626,14 +513,11 @@ function parseInterface(line) {
throw new Error(`Failed to parse interface: ${line}`); throw new Error(`Failed to parse interface: ${line}`);
} }
const name = match[1]; const name = match[1];
// Header-only; parseInterfaceBlockMultiline fills in methods/fields/kind // This is a simplified parser - in a real implementation, we'd need to handle multi-line interfaces
// by scanning the lines inside the { ... } block.
return { return {
type: 'interface', type: 'interface',
name, name,
kind: 'mixed',
methods: [], methods: [],
fields: [],
}; };
} }
function parseEvent(line) { function parseEvent(line) {
@ -649,32 +533,6 @@ function parseEvent(line) {
fields: [], fields: [],
}; };
} }
// Cycle 57: parse `oneof Name {` (header only; parseOneofBlockMultiline fills variants).
function parseOneof(line) {
// oneof Name {
const match = line.match(/^oneof\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse oneof: ${line}`);
}
return {
type: 'oneof',
name: match[1],
variants: [],
};
}
// Cycle 58: parse `transition Name {` (header only; parseTransitionBlockMultiline fills fields + payload-oneof).
function parseTransition(line) {
// transition Name {
const match = line.match(/^transition\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse transition: ${line}`);
}
return {
type: 'transition',
name: match[1],
fields: [],
};
}
function parseProvenanceBlock(lines, line) { function parseProvenanceBlock(lines, line) {
// This is a simplified parser - in a real implementation, we'd parse the full block // This is a simplified parser - in a real implementation, we'd parse the full block
return { return {
@ -752,12 +610,6 @@ function parseSource(line) {
}; };
} }
function parseStateBlockMultiline(lines, startIndex, startBraceCount) { function parseStateBlockMultiline(lines, startIndex, startBraceCount) {
// Cycle 59: support `state as <MessageName> { ... }` to override the
// generated .proto message name. Default (no `as`) keeps the existing
// `message <SpeckName>State { ... }` convention.
const headerLine = lines[startIndex].trim();
const asMatch = headerLine.match(/^state\s+as\s+(\w+)\s*{/);
const messageName = asMatch ? asMatch[1] : undefined;
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount); const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*')); const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
// State blocks separate fields with commas or newlines/semicolons. // State blocks separate fields with commas or newlines/semicolons.
@ -777,10 +629,7 @@ function parseStateBlockMultiline(lines, startIndex, startBraceCount) {
} }
return acc + ' ' + line; return acc + ' ' + line;
}, ''); }, '');
const result = parseStateBlock(inner); return parseStateBlock(inner);
if (messageName !== undefined)
result.messageName = messageName;
return result;
} }
function parseInitBlockMultiline(lines, startIndex, startBraceCount) { function parseInitBlockMultiline(lines, startIndex, startBraceCount) {
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount); const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
@ -964,24 +813,7 @@ function parseEventBlockMultiline(lines, startIndex, startBraceCount) {
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*')); const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const fields = []; const fields = [];
for (const line of innerLines) { for (const line of innerLines) {
// Cycle 62: strip inline `//` line-comments from the type expression const match = line.match(/^(\w+)\s*:\s*(.+?),?$/);
// before parsing. Without this, an event field like
// mesh_ip: Bytes // 4 bytes (IPv4 overlay)
// produces a TypeExpr whose name includes the comment text, which
// the .proto generator emits verbatim:
// bytes // 4 bytes (IPv4 overlay) mesh_ip = 2;
// (broken syntax — comment is in the type position).
const noComment = line.replace(/\/\/.*$/, '').trim();
// Cycle 65: strip default-value suffix `= <expr>` from the type
// expression. The federated-meetup speckdl has fields like
// initial_mesh_peers: List<InitialMeshPeer> = []
// where the default is meaningful in Speckl semantics (a state-
// machine init) but the .proto wire format doesn't carry a
// default — it's a generator concern. Without this, the type
// expression was emitted as `List<InitialMeshPeer> = []` and
// protoc rejects the resulting syntax.
const noDefault = noComment.replace(/\s*=\s*[^,]+$/, '').trim();
const match = noDefault.match(/^(\w+)\s*:\s*(.+?),?$/);
if (match) { if (match) {
fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) }); fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) });
} }
@ -994,20 +826,12 @@ function parseInterfaceBlockMultiline(lines, startIndex, startBraceCount) {
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount); const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*')); const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const methods = []; const methods = [];
const fields = [];
for (const line of innerLines) { for (const line of innerLines) {
// Cycle 62: strip inline `//` line-comments from each line before // name-only: enum-style values (e.g., "Idle", "Idle, Parsing" comma-separated)
// token-splitting. Without this, a field like // Split on comma and take each trimmed token
// mesh_ip: Bytes // 4 bytes (IPv4 overlay) const tokens = line.split(',').map(s => s.trim()).filter(Boolean);
// has its comment text bleed into the parsed type expression,
// which the .proto generator emits verbatim — broken syntax.
const noComment = line.replace(/\/\/.*$/, '').trim();
if (!noComment)
continue;
// Split on comma so multi-variant lines like "Idle, Parsing, Done" all parse
const tokens = noComment.split(',').map(s => s.trim()).filter(Boolean);
for (const token of tokens) { for (const token of tokens) {
// Check 1: method signature form: name(params) -> returnType // Check if it’s a name(params) -> returnType method signature
const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/); const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/);
if (methodMatch) { if (methodMatch) {
const name = methodMatch[1]; const name = methodMatch[1];
@ -1024,135 +848,14 @@ function parseInterfaceBlockMultiline(lines, startIndex, startBraceCount) {
} }
} }
methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) }); methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) });
continue;
} }
// Check 2: field declaration form: field_name: TypeName else if (/^\w+$/.test(token)) {
// Lowercase-starting identifier followed by ':' — record-style interface // Name-only (enum-style) — treat as a method with no params and void return
const fieldMatch = token.match(/^(\w+)\s*:\s*(.+)$/);
if (fieldMatch && /^[a-z_]/.test(fieldMatch[1])) {
fields.push({ name: fieldMatch[1], type: parseTypeExpr(fieldMatch[2].trim()) });
continue;
}
// Check 3: bare identifier (enum variant) — name only, no params
if (/^\w+$/.test(token)) {
methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') }); methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') });
} }
} }
} }
// Determine the kind based on what we collected return { ...header, methods };
let kind = 'mixed';
if (fields.length > 0 && methods.length === 0) {
kind = 'record';
}
else if (methods.length > 0 && fields.length === 0) {
// Distinguish enum (all methods have empty params and Void return) from service
const allEnumLike = methods.every(m => m.params.length === 0 && m.returnType.name === 'Void');
kind = allEnumLike ? 'enum' : 'service';
}
return { ...header, kind, methods, fields };
}
// Cycle 57: parse a `oneof Name { ... }` block. Each non-empty, non-comment
// inner line is `field_name: TypeName`. The wire field_name follows
// lowerCamelCase convention (TypeScript/Connect) and is emitted to .proto
// as snake_case by the generator.
function parseOneofBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
const header = parseOneof(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const variants = [];
for (const line of innerLines) {
// Strip trailing comma or semicolon (proto-style "create_group: CreateGroup," is valid).
const trimmed = line.replace(/[,;]\s*$/, '');
const m = trimmed.match(/^(\w+)\s*:\s*(\w+)\s*$/);
if (m) {
variants.push({ fieldName: m[1], typeName: m[2] });
}
}
return { ...header, variants };
}
// Cycle 58: parse a `transition Name { ... }` block. Each non-empty,
// non-comment inner line is `field_name: TypeName`. Two field names
// have special meaning:
// - `payload: <OneofName>` — references a sibling `oneof` block;
// the proto generator will emit the variants inline as
// `oneof payload { ... }` inside the message body
// - `type: <EnumName>` — the discriminator enum for the variants
// Other fields are emitted as ordinary proto message fields.
function parseTransitionBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
const header = parseTransition(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const fields = [];
let payloadOneof;
let typeDiscriminator;
for (const line of innerLines) {
const trimmed = line.replace(/[,;]\s*$/, '');
const m = trimmed.match(/^(\w+)\s*:\s*(.+)$/);
if (!m)
continue;
const fieldName = m[1];
const typeStr = m[2].trim();
if (fieldName === 'payload') {
// The type is the name of a sibling oneof block.
payloadOneof = typeStr;
// Don't add a regular field for payload — it becomes the oneof.
continue;
}
if (fieldName === 'type') {
// The type is the name of a discriminator enum.
typeDiscriminator = typeStr;
// Don't add a regular field for type — it's a special discriminator.
continue;
}
fields.push({ name: fieldName, type: parseTypeExpr(typeStr) });
}
const result = { ...header, fields };
if (payloadOneof !== undefined)
result.payloadOneof = payloadOneof;
if (typeDiscriminator !== undefined)
result.typeDiscriminator = typeDiscriminator;
return result;
}
function parseServiceBlockMultiline(lines, startIndex, startBraceCount) {
// service Name {
const firstLine = lines[startIndex].trim();
const match = firstLine.match(/^service\s+(\w+)\s*{?/);
const name = match ? match[1] : 'UnnamedService';
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const rpcs = [];
for (const line of innerLines) {
// rpc MethodName(RequestType) returns (ResponseType);
// Also support streaming: rpc M(stream R) returns (S); or rpc M(R) returns (stream S);
const rpcMatch = line.match(/^rpc\s+(\w+)\s*\(\s*(stream\s+)?(\w+)\s*\)\s*returns\s*\(\s*(stream\s+)?(\w+)\s*\)\s*;?$/);
if (rpcMatch) {
const methodName = rpcMatch[1];
const clientStream = !!rpcMatch[2];
const requestType = rpcMatch[3];
const serverStream = !!rpcMatch[4];
const responseType = rpcMatch[5];
rpcs.push({
name: methodName,
requestType,
responseType,
clientStreaming: clientStream,
serverStreaming: serverStream,
});
}
else {
// Cycle 73: error on unrecognized lines inside service blocks.
// Previously, a typo like `rc_purchase_ticket(...)` (missing the `p`
// in `rpc`) was silently swallowed — the line didn't match the
// rpc regex, so it was skipped without error. Silent data loss in
// a spec compiler is unacceptable; the whole point is that the
// spec is the source of truth.
throw new Error(`Parse error in service block: unrecognized line "${line}". ` +
`Expected: rpc MethodName(RequestType) returns (ResponseType);`);
}
}
return { type: 'service', name, rpcs };
} }
// --- Multi-line constraint/verify parsing (no braces needed) --- // --- Multi-line constraint/verify parsing (no braces needed) ---
/** /**
@ -1170,128 +873,11 @@ function parseMultiLineConstraintVerify(lines, startIndex) {
if (line.startsWith('verify ')) { if (line.startsWith('verify ')) {
return parseVerifyAnyForm(lines, startIndex); return parseVerifyAnyForm(lines, startIndex);
} }
// Multi-line `verify:` form: verify: always(implies(\n ...\n))
// The body opens parens that span multiple lines; collect continuation
// lines until parens balance to zero, then return the joined string as
// the temporalExpr. speckl#54.
if (line.startsWith('verify:')) {
return parseVerifyColonBlock(lines, startIndex);
}
if (line.startsWith('constraint ')) { if (line.startsWith('constraint ')) {
return parseConstraintAnyForm(lines, startIndex); return parseConstraintAnyForm(lines, startIndex);
} }
return null; return null;
} }
/**
* Parse the `verify: <expr>` form (speckl#54) where the body can span
* multiple lines:
*
* verify: always(implies(
* cond1,
* cond2
* ))
*
* The whole expression (the part after `verify:`) is collected by
* appending subsequent non-empty, non-keyword-starting lines until
* parens/brackets/braces balance to zero. The joined string is stored
* in `temporalExpr` so the downstream LTL translator (typescript-state-machine
* verifyN()) sees a well-formed formula.
*
* The `name` is derived from the LTL operator's argument when it matches
* `always(Name)` / `eventually(Name)`. When the body is a richer expression
* (e.g. `always(implies(...))`) we fall back to `unnamed` — the generator
* still emits a working verifyN() that uses the full expression.
*/
function parseVerifyColonBlock(lines, startIndex) {
const firstLine = lines[startIndex].trim();
// Strip the `verify:` prefix.
const head = firstLine.substring(firstLine.indexOf(':') + 1).trim();
if (!head)
return null;
// If the head is already balanced on its own (single-line verify: expr),
// just return it directly — no continuation needed.
if (isExpressionComplete(head)) {
const nameMatch = head.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
return {
type: 'verify',
name: nameMatch ? nameMatch[1] : 'unnamed',
temporalExpr: head,
};
}
// Multi-line: collect continuation lines until parens balance. The same
// break-condition list used in the parseSpeck skip-loop applies (don't
// swallow the next member's keyword). We additionally stop at any
// standalone `}` so a verify inside a brace-block still terminates.
const parts = [head];
let parens = 0, brackets = 0, braces = 0;
for (const ch of head) {
if (ch === '(')
parens++;
else if (ch === ')')
parens--;
else if (ch === '[')
brackets++;
else if (ch === ']')
brackets--;
else if (ch === '{')
braces++;
else if (ch === '}')
braces--;
}
let lastConsumed = startIndex;
for (let j = startIndex + 1; j < lines.length; j++) {
const raw = lines[j];
const nl = raw.trim();
if (!nl) {
// Empty line still updates counters (none) and advances lastConsumed
lastConsumed = j;
continue;
}
if (nl.startsWith('//') || nl.startsWith('/*')) {
// Skip standalone comments but treat them as part of the block
// (the LTL translator doesn't care about comments in temporalExpr).
lastConsumed = j;
continue;
}
// Stop at a new top-level member keyword — that's the next member.
if (nl.startsWith('constraint ') || nl.startsWith('verify ') ||
nl.startsWith('constraint:') || nl.startsWith('verify:') ||
nl.startsWith('state') || nl.startsWith('init') ||
nl.startsWith('action ') || nl.startsWith('event ') ||
nl.startsWith('interface ') || nl.startsWith('provenance ') ||
nl.startsWith('bom ') || nl === '}' ||
nl.startsWith('next:') || nl.startsWith('invariant ')) {
break;
}
// Update depth counters.
for (const ch of raw) {
if (ch === '(')
parens++;
else if (ch === ')')
parens--;
else if (ch === '[')
brackets++;
else if (ch === ']')
brackets--;
else if (ch === '{')
braces++;
else if (ch === '}')
braces--;
}
parts.push(nl);
lastConsumed = j;
if (parens === 0 && brackets === 0 && braces === 0) {
break;
}
}
const joined = parts.join(' ').replace(/\s+/g, ' ').trim();
const nameMatch = joined.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
return {
type: 'verify',
name: nameMatch ? nameMatch[1] : 'unnamed',
temporalExpr: joined,
};
}
function parseConstraintAnyForm(lines, startIndex) { function parseConstraintAnyForm(lines, startIndex) {
const line = lines[startIndex].trim(); const line = lines[startIndex].trim();
const namedMatch = line.match(/^constraint\s+(\w+):(.*)$/); const namedMatch = line.match(/^constraint\s+(\w+):(.*)$/);

2
compiler/dist/parser.js.map vendored
View file

File diff suppressed because one or more lines are too long

2
compiler/node_modules/.vite/vitest/results.json generated vendored
View file

@ -1 +1 @@
{"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":58.32899300000008,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":7758.09763,"failed":false}]]} {"version":"2.1.9","results":[[":__tests__/parser.test.ts",{"duration":31.455063999999993,"failed":false}],[":src/__tests__/compiler.test.ts",{"duration":12.627537000000018,"failed":false}]]}

14
compiler/src/__tests__/ifblock-smoke/ConditionalToggle.prov.jsonld → compiler/out/speckl-compile/SpecklCompiler.prov.jsonld
View file

@ -7,15 +7,23 @@
"@graph": [ "@graph": [
{ {
"@type": "prov:Entity", "@type": "prov:Entity",
"@id": "speck:ConditionalToggle", "@id": "speck:SpecklCompiler",
"prov:qualifiedGeneration": { "prov:qualifiedGeneration": {
"@type": "prov:Generation", "@type": "prov:Generation",
"prov:activity": { "prov:activity": {
"@type": "prov:Activity", "@type": "prov:Activity",
"prov:startTime": "2026-07-19T08:31:19.208Z" "prov:startTime": "2026-05-03T21:19:53.222Z"
} }
}, },
"rdfs:label": "ConditionalToggle" "rdfs:label": "SpecklCompiler",
"prov:wasAttributedTo": {
"@id": "agent:sscoble"
}
},
{
"@type": "prov:Agent",
"@id": "agent:sscoble",
"rdfs:label": "sscoble"
} }
] ]
} }

30
compiler/out/speckl-compile/SpecklCompiler.specbom.cdx.json Normal file
View file

@ -0,0 +1,30 @@
{
"bomFormat": "CycloneDX",
"specVersion": "1.6",
"components": [],
"metadata": {
"tools": [],
"component": {
"type": "application",
"name": "SpecklCompiler",
"version": "0.2.0",
"properties": []
}
},
"annotations": [
{
"subject": "speck:SpecklCompiler",
"annotations": [
{
"type": "tag",
"value": "provenanceType",
"text": "author"
}
],
"author": {
"name": "sscoble"
},
"timestamp": "2026-05-03T21:19:53.229Z"
}
]
}

42
compiler/out/speckl-compile/SpecklCompiler.specbom.spdx.json Normal file
View file

@ -0,0 +1,42 @@
{
"@context": [
"https://spdx.github.io/spdx-v3/spdx-context.jsonld",
{
"speckl": "https://speckl.scoble.me/ns/v0.2#"
}
],
"@type": "spdx:Document",
"spdx": {
"@id": "spdx:SpecklCompiler",
"@type": "spdx:Snippet",
"name": "SpecklCompiler",
"spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0",
"creationInfo": {
"created": "2026-05-03T21:19:53.229Z",
"createdBy": [
"Organization: Speckl",
"tool: speckl-compile-0.2.0"
]
}
},
"builtBy": [],
"relationships": [
{
"from": {
"@id": "spdx:SpecklCompiler"
},
"to": {
"@id": "spdx:agent:sscoble"
},
"relationshipType": "spdx:wasAttributedTo"
}
],
"elements": [
{
"@type": "spdx:Person",
"@id": "spdx:agent:sscoble",
"name": "sscoble"
}
]
}

153
compiler/out/speckl-compile/SpecklCompiler.ts Normal file
View file

@ -0,0 +1,153 @@
// Auto-generated by speckl-compile from SpecklCompiler
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
export const SpecklCompilerCompilerPhase = {
BOMsGenerated: 'bomsgenerated',
Idle: 'idle',
Parsed: 'parsed',
Parsing: 'parsing',
ProvenanceGenerated: 'provenancegenerated',
TypeScriptGenerated: 'typescriptgenerated',
WASMGenerated: 'wasmgenerated',
} as const;
export type SpecklCompilerCompilerPhase = typeof SpecklCompilerCompilerPhase[keyof typeof SpecklCompilerCompilerPhase];
export const SpecklCompilerArtifactKind = {
CycloneDX: 'cyclonedx',
Done: 'done',
Provenance: 'provenance',
SPDX: 'spdx',
TypeScript: 'typescript',
WebAssembly: 'webassembly',
} as const;
export type SpecklCompilerArtifactKind = typeof SpecklCompilerArtifactKind[keyof typeof SpecklCompilerArtifactKind];
export interface CompilationStarted {
source: string;
output: string;
at: string;
}
export interface PhaseCompleted {
phase: SpecklCompilerCompilerPhase;
durationMs: number;
at: string;
}
export interface ArtifactGenerated {
kind: SpecklCompilerArtifactKind;
path: string;
bytes: number;
at: string;
}
export interface ErrorEmitted {
phase: SpecklCompilerCompilerPhase;
message: string;
line: number;
col: number;
at: string;
}
export class SpecklCompilerMachine {
phase: SpecklCompilerCompilerPhase;
sourcePath: String;
outputDir: String;
ast: any;
errors: String[];
artifacts: any;
decisionLog: CompilationStarted[] = [];
constructor() {
this.phase = SpecklCompilerCompilerPhase.Idle;
this.sourcePath = "";
this.outputDir = "./out";
this.ast = {};
this.errors = [];
this.artifacts = {};
}
compile(sourcePath: string, outputDir: string) {
if (!(this.phase === SpecklCompilerCompilerPhase.Idle)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.Idle');
if (!(sourcePath.length > 0)) throw new Error('Guard failed: sourcePath.length > 0');
this.decisionLog.push({
source: sourcePath,
output: outputDir,
at: Date.now()
} as CompilationStarted);
}
parse() {
if (!(this.phase === SpecklCompilerCompilerPhase.Parsing)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.Parsing');
if (!(this.sourcePath.length > 0)) throw new Error('Guard failed: this.sourcePath.length > 0');
this.decisionLog.push({
phase: SpecklCompilerCompilerPhase.Parsing,
durationMs: 0,
at: Date.now()
} as PhaseCompleted);
}
generateProvenance() {
if (!(this.phase === SpecklCompilerCompilerPhase.Parsed || this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.WASMGenerated)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.Parsed || this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.WASMGenerated');
this.decisionLog.push({
kind: SpecklCompilerCompilerPhase.Provenance,
path: join(this.outputDir,
bytes: 0,
at: Date.now()
} as ArtifactGenerated);
}
generateBOMs() {
if (!(this.phase === SpecklCompilerCompilerPhase.ProvenanceGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.ProvenanceGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed');
this.decisionLog.push({
kind: SpecklCompilerCompilerPhase.CycloneDX,
path: join(this.outputDir,
bytes: 0,
at: Date.now()
} as ArtifactGenerated);
this.decisionLog.push({
kind: SpecklCompilerCompilerPhase.SPDX,
path: join(this.outputDir,
bytes: 0,
at: Date.now()
} as ArtifactGenerated);
}
generateTypeScript() {
if (!(this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed');
this.decisionLog.push({
kind: SpecklCompilerCompilerPhase.TypeScript,
path: join(this.outputDir,
bytes: 0,
at: Date.now()
} as ArtifactGenerated);
}
generateWASM() {
if (!(this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.Parsed');
this.decisionLog.push({
kind: SpecklCompilerCompilerPhase.WebAssembly,
path: join(this.outputDir,
bytes: 0,
at: Date.now()
} as ArtifactGenerated);
}
report() {
if (!(this.phase === SpecklCompilerCompilerPhase.ProvenanceGenerated || this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.WASMGenerated)) throw new Error('Guard failed: this.phase === SpecklCompilerCompilerPhase.ProvenanceGenerated || this.phase === SpecklCompilerCompilerPhase.BOMsGenerated || this.phase === SpecklCompilerCompilerPhase.TypeScriptGenerated || this.phase === SpecklCompilerCompilerPhase.WASMGenerated');
this.decisionLog.push({
phase: SpecklCompilerCompilerPhase.Done,
durationMs: 0,
at: Date.now()
} as PhaseCompleted);
}
reset() {
}
}

151
compiler/out/speckl-compile/SpecklCompiler.wat Normal file
View file

@ -0,0 +1,151 @@
;; Auto-generated by speckl-compile from SpecklCompiler
;; Compile: wat2wasm SpecklCompiler.wat -o SpecklCompiler.wasm
(module
;; Host imports for Map/Set/alloc
(import "speckl" "map_create" (func $map_create (result i32)))
(import "speckl" "map_set" (func $map_set (param i32 i32 i32)))
(import "speckl" "map_get" (func $map_get (param i32 i32) (result i32)))
(import "speckl" "map_has" (func $map_has (param i32 i32) (result i32)))
(import "speckl" "map_remove" (func $map_remove (param i32 i32)))
(import "speckl" "set_create" (func $set_create (result i32)))
(import "speckl" "set_add" (func $set_add (param i32 i32)))
(import "speckl" "set_has" (func $set_has (param i32 i32) (result i32)))
(import "speckl" "set_size" (func $set_size (param i32) (result i32)))
(import "speckl" "alloc" (func $alloc (param i32) (result i32)))
(import "speckl" "write_i32" (func $write_i32 (param i32 i32)))
(import "speckl" "write_f64" (func $write_f64 (param i32 f64)))
;; Linear memory (exported so host can read state)
(memory (export "memory") 1)
;; State globals
(global $phase (mut i32) (i32.const 0))
(global $sourcePath (mut i32) (i32.const 0))
(global $outputDir (mut i32) (i32.const 0))
(global $ast (mut i32) (i32.const 0))
(global $errors (mut i32) (i32.const 0))
(global $artifacts (mut i32) (i32.const 0))
;; ---- init ----
(func $init (export "init")
(i32.const 0)
(global.set $phase)
(i32.const 0)
(global.set $sourcePath)
(i32.const 0)
(global.set $outputDir)
(i32.const 0)
(global.set $ast)
(i32.const 0)
(global.set $errors)
(i32.const 0)
(global.set $artifacts)
)
;; ---- Actions ----
;; action: compile
(func $compile (export "compile") (param $sourcePath i32) (param $outputDir i32) (result i32)
;; require: phase === Idle
;; Complex right-hand side not compiled: phase === Idle
;; require: len(sourcePath) > 0
;; Complex guard not compiled: len(sourcePath) > 0
;; emit CompilationStarted { ... }
(i32.const 1)
)
;; action: parse
(func $parse (export "parse") (result i32)
;; require: phase === Parsing
;; Complex right-hand side not compiled: phase === Parsing
;; require: len(sourcePath) > 0
;; Complex guard not compiled: len(sourcePath) > 0
;; emit PhaseCompleted { ... }
(i32.const 1)
)
;; action: generateProvenance
(func $generateProvenance (export "generateProvenance") (result i32)
;; require: phase === Parsed || phase === TypeScriptGenerated || phase === WASMGenerated
;; Complex right-hand side not compiled: phase === Parsed || phase === TypeScriptGenerated || phase === WASMGenerated
;; emit ArtifactGenerated { ... }
(i32.const 1)
)
;; action: generateBOMs
(func $generateBOMs (export "generateBOMs") (result i32)
;; require: phase === ProvenanceGenerated || phase === Parsed
;; Complex right-hand side not compiled: phase === ProvenanceGenerated || phase === Parsed
;; emit ArtifactGenerated { ... }
;; emit ArtifactGenerated { ... }
(i32.const 1)
)
;; action: generateTypeScript
(func $generateTypeScript (export "generateTypeScript") (result i32)
;; require: phase === BOMsGenerated || phase === Parsed
;; Complex right-hand side not compiled: phase === BOMsGenerated || phase === Parsed
;; emit ArtifactGenerated { ... }
(i32.const 1)
)
;; action: generateWASM
(func $generateWASM (export "generateWASM") (result i32)
;; require: phase === TypeScriptGenerated || phase === BOMsGenerated || phase === Parsed
;; Complex right-hand side not compiled: phase === TypeScriptGenerated || phase === BOMsGenerated || phase === Parsed
;; emit ArtifactGenerated { ... }
(i32.const 1)
)
;; action: report
(func $report (export "report") (result i32)
;; require: phase === ProvenanceGenerated || phase === BOMsGenerated || phase === TypeScriptGenerated || phase === WASMGenerated
;; Complex right-hand side not compiled: phase === ProvenanceGenerated || phase === BOMsGenerated || phase === TypeScriptGenerated || phase === WASMGenerated
;; emit PhaseCompleted { ... }
(i32.const 1)
)
;; action: reset
(func $reset (export "reset") (result i32)
(i32.const 1)
)
;; ---- getState ----
(func $getState (export "getState") (result i32 i32)
(i32.const 0)
(global.get $phase)
(i32.store)
(i32.const 4)
(global.get $sourcePath)
(i32.store)
(i32.const 8)
(global.get $outputDir)
(i32.store)
(i32.const 12)
(global.get $ast)
(i32.store)
(i32.const 16)
(global.get $errors)
(i32.store)
(i32.const 20)
(global.get $artifacts)
(i32.store)
(i32.const 0)
(i32.const 24)
)
;; checkConstraints — runtime constraint evaluation stub
(func $checkConstraints (export "checkConstraints") (result i32)
;; TODO: evaluate constraint expressions at runtime
(i32.const 1)
)
)

253
compiler/src/__tests__/compiler.test.ts
View file

@ -1,15 +1,11 @@
import { describe, it, expect, beforeAll } from 'vitest'; import { describe, it, expect, beforeAll } from 'vitest';
import fs from 'fs'; import fs from 'fs';
import path from 'path'; import path from 'path';
import { fileURLToPath } from 'url';
import { execSync } from 'child_process';
import { parseSpeckFile } from '../parser.js'; import { parseSpeckFile } from '../parser.js';
import { generateProvenanceGraph } from '../generators/provenance.js'; import { generateProvenanceGraph } from '../generators/provenance.js';
import { generateCycloneDX } from '../generators/cyclonedx.js'; import { generateCycloneDX } from '../generators/cyclonedx.js';
import { generateSPDX } from '../generators/spdx.js'; import { generateSPDX } from '../generators/spdx.js';
const __dirname = path.dirname(fileURLToPath(import.meta.url));
describe('Compiler E2E', () => { describe('Compiler E2E', () => {
let ast: any; let ast: any;
const testOutputDir = './test-output'; const testOutputDir = './test-output';
@ -22,7 +18,7 @@ describe('Compiler E2E', () => {
}); });
it('should parse RetryHandler.speck', () => { it('should parse RetryHandler.speck', () => {
const specPath = path.join(__dirname, '..', '..', '..', 'examples', 'RetryHandler.speck'); const specPath = path.join(process.cwd(), '..', 'examples', 'RetryHandler.speck');
ast = parseSpeckFile(specPath); ast = parseSpeckFile(specPath);
expect(ast).toBeDefined(); expect(ast).toBeDefined();
@ -74,251 +70,4 @@ describe('Compiler E2E', () => {
expect(spdx['@context']).toBeDefined(); expect(spdx['@context']).toBeDefined();
expect(spdx.spdx).toBeDefined(); expect(spdx.spdx).toBeDefined();
}); });
it('should generate protobuf schema', () => {
// Compile RetryHandler.speck with --target protobuf and assert the
// generated .proto contains the expected protobuf constructs.
const specPath = path.join(__dirname, '..', '..', '..', 'examples', 'RetryHandler.speck');
const protoOutDir = path.join(testOutputDir, 'proto-smoke');
if (!fs.existsSync(protoOutDir)) {
fs.mkdirSync(protoOutDir, { recursive: true });
}
execSync(
`npx tsx src/index.ts ${specPath} -t protobuf -o ${protoOutDir}`,
{ cwd: COMPILER_DIR, stdio: 'pipe' },
);
const protoFiles = fs.readdirSync(protoOutDir).filter(f => f.endsWith('.proto'));
expect(protoFiles.length).toBeGreaterThanOrEqual(1);
const protoContent = fs.readFileSync(path.join(protoOutDir, protoFiles[0]), 'utf-8');
expect(protoContent).toContain('syntax = "proto3";');
expect(protoContent).toMatch(/\bmessage\s+\w+/);
// RetryHandler has events with fields — assert at least one field line
expect(protoContent).toMatch(/\w+\s+\w+\s*=\s*\d+;/);
});
}); });
describe('ifblock code generation', () => {
it('should emit real TypeScript if/else from a SpeckDL ifblock', () => {
// Compile ConditionalToggle.speck (has an if/else action body) and assert
// the generated TS contains a real `if (` with a brace block, not the old
// TODO stub comment.
const specPath = path.join(__dirname, '..', '..', '..', 'examples', 'ConditionalToggle.speck');
const outDir = path.join(__dirname, 'ifblock-smoke');
if (!fs.existsSync(outDir)) {
fs.mkdirSync(outDir, { recursive: true });
}
execSync(
`npx tsx src/index.ts ${specPath} -t typescript -o ${outDir}`,
{ cwd: COMPILER_DIR, stdio: 'pipe' },
);
const tsFile = path.join(outDir, 'ConditionalToggle.ts');
expect(fs.existsSync(tsFile)).toBe(true);
const tsContent = fs.readFileSync(tsFile, 'utf-8');
// Should contain a real if statement
expect(tsContent).toMatch(/\bif\s*\(/);
// Should contain a brace block body
expect(tsContent).toContain('{ ');
expect(tsContent).toContain(' }');
// Should NOT contain the old TODO stub
expect(tsContent).not.toContain('TODO: SpeckDL conditional block');
// Should contain an else clause (our spec has if/else)
expect(tsContent).toMatch(/\belse\b/);
});
});
// ---------------------------------------------------------------------------
// Regression tests for Z3 / TypeScript / Rust expression translation fixes.
//
// These tests compile the FederatedMeetupProduct spec against each backend
// (z3, typescript, rust) and assert that the generated output contains the
// expected translated patterns. They guard against regressions in:
// - implies() argument preservation (Z3 + TS + Rust)
// - multi-level field access flattening (Z3)
// - len()/length() normalization (Z3)
// - nil → speckl_nil translation (Z3)
// - != → (distinct X Y) wrapping (Z3)
// - constraint checks emitting real every() / iter().all() (TS + Rust)
// - 'in' operator → .has() in verify expressions (TS)
// - multiple verify blocks all emitted (memberKey dedup fix) (TS + Rust)
// ---------------------------------------------------------------------------
const SPEC_PATH = '/home/sscoble/projects/federated-meetup/specs/FederatedMeetupProduct.speckdl';
const OUT_DIR = './out'; // CLI writes to ./out relative to compiler cwd
const COMPILER_DIR = '/home/sscoble/speckl/compiler';
describe('Z3 / TS / Rust expression translation regressions', () => {
let z3Output: string;
let tsOutput: string;
let rustOutput: string;
beforeAll(() => {
// Clean out directory to avoid stale output
execSync(`rm -rf ${OUT_DIR}`, { cwd: COMPILER_DIR });
execSync(`mkdir -p ${OUT_DIR}`, { cwd: COMPILER_DIR });
// Compile to all three targets
execSync(
`npx tsx src/index.ts ${SPEC_PATH} --target z3 --output ${OUT_DIR}`,
{ cwd: COMPILER_DIR, stdio: 'pipe' },
);
z3Output = fs.readFileSync(
path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct.smt2'),
'utf-8',
);
execSync(
`npx tsx src/index.ts ${SPEC_PATH} --target typescript --output ${OUT_DIR}`,
{ cwd: COMPILER_DIR, stdio: 'pipe' },
);
tsOutput = fs.readFileSync(
path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct.ts'),
'utf-8',
);
execSync(
`npx tsx src/index.ts ${SPEC_PATH} --target rust --output ${OUT_DIR}`,
{ cwd: COMPILER_DIR, stdio: 'pipe' },
);
rustOutput = fs.readFileSync(
path.join(COMPILER_DIR, OUT_DIR, 'FederatedMeetupProduct', 'src', 'lib.rs'),
'utf-8',
);
}, 120_000);
// 1. Z3: implies() preserves both arguments → (=> P Q) not (=> true true)
it('Z3: implies() emits (=> P Q) preserving both arguments', () => {
expect(z3Output).toContain('(=>');
expect(z3Output).toContain('(=> (= o_status Refunded) (distinct o_refunded_at speckl_nil))');
// Ensure we did NOT regress to (=> true true)
expect(z3Output).not.toContain('(=> true true)');
expect(z3Output).not.toContain('(=> true');
});
// 2. Z3: multi-level field access m.price.amount → m_price_amount
it('Z3: multi-level field access m.price.amount flattens to m_price_amount', () => {
expect(z3Output).toContain('m_price_amount');
// Ensure we did NOT regress to single-level m_price or bare m.price.amount
expect(z3Output).not.toContain('m.price.amount');
// The constraint m_price_amount >= 0 should be present
expect(z3Output).toContain('(>= m_price_amount 0)');
});
// 3. Z3: len() handled same as length() → speckl_len_Int
it('Z3: len() is translated to speckl_len_Int (same as length())', () => {
// The spec uses len(m.price.currency) — should become speckl_len_Int
expect(z3Output).toContain('(speckl_len_Int m_price_currency)');
// Ensure we did NOT regress to bare len() or length()
expect(z3Output).not.toMatch(/\blen\s*\(/);
expect(z3Output).not.toMatch(/\blength\s*\(/);
});
// 4. Z3: nil translated to speckl_nil
it('Z3: nil is translated to speckl_nil sentinel', () => {
expect(z3Output).toContain('(declare-const speckl_nil Int)');
expect(z3Output).toContain('speckl_nil');
// Ensure we did NOT regress to bare nil / null
expect(z3Output).not.toMatch(/\bnil\b/);
});
// 5. Z3: != produces (distinct X Y) not bare 'distinct'
it('Z3: != produces wrapped (distinct X Y) not bare distinct', () => {
// The constraint g.hosting_tier != Free should emit (distinct g_hosting_tier Free)
expect(z3Output).toContain('(distinct g_hosting_tier Free)');
// Ensure we did NOT regress to bare 'distinct g_hosting_tier Free' without parens
// (the fix wraps the operator in parens)
// A bare distinct would look like "g_hosting_tier distinct Free" without surrounding parens
expect(z3Output).not.toMatch(/[^(]\w+\s+distinct\s+\w+/);
});
// 6. TS: implies(p,q) → (!p || q) not (p || q)
it('TS: implies(p, q) translates to (!p || q), not (p || q)', () => {
// constraint 6: implies(o.status == Refunded, o.refunded_at != nil)
// Should become (!(o.status === ...) || (o.refunded_at !== ...))
expect(tsOutput).toContain('(!(');
expect(tsOutput).toContain('||');
// The specific pattern: (!(o.status === ... || (o.refunded_at !== nil))
expect(tsOutput).toMatch(/!\(o\.status === .* \|\| \(o\.refunded_at !== /);
// Ensure the CODE (not comments) has negation on p.
// A regression would have `return this.orders.every((o: any) => (o.status ===`
// (without the `!(` negation before `o.status`).
// Strip comments to avoid matching the original spec text in comments.
const tsNoComments = tsOutput.replace(/^\s*\/\/.*$/gm, '');
// Positive: the every() body starts with (!(o.status — the (! is the negation
expect(tsNoComments).toMatch(/every\(\(o:\s*any\)\s*=>\s*\(!\(o\.status/);
// Negative: a regression would have every((o: any) => (o.status without the ! negation
expect(tsNoComments).not.toMatch(/every\(\(o:\s*any\)\s*=>\s*\(o\.status/);
});
// 7. TS: constraint checks emit real every() not return true
it('TS: constraint checks emit real .every() calls, not return true', () => {
expect(tsOutput).toContain('.every(');
// Multiple constraints use every() — at least 8 constraints
const everyCount = (tsOutput.match(/\.every\(/g) || []).length;
expect(everyCount).toBeGreaterThanOrEqual(8);
// Ensure we did NOT regress to `return true` stubs
// A stub would have checkConstraintN() { return true; }
expect(tsOutput).not.toMatch(/checkConstraint\d+\(\):\s*boolean\s*\{\s*return\s*true\s*;\s*\}/);
});
// 8. TS: 'in' operator in verify expressions → .has() not raw 'in'
it('TS: "in" operator in verify expressions translates to .has(), not raw in', () => {
// V1: always(implies(event == PurchaseTicket, ticket_id in tickets))
// Should become tickets.has(ticket_id)
expect(tsOutput).toContain('.has(');
expect(tsOutput).toContain('tickets.has(ticket_id)');
// Ensure we did NOT regress to raw 'in' operator (JS `in` checks property keys, not membership).
// A regression would look like `ticket_id in tickets` in CODE (not comments).
// Strip comments to avoid matching the original spec text in comments.
const tsNoComments = tsOutput.replace(/^\s*\/\/.*$/gm, '');
expect(tsNoComments).not.toMatch(/\bticket_id\s+in\s+tickets\b/);
});
// 9. TS/Rust: multiple verify blocks all emitted (memberKey dedup fix)
it('TS: all 6 verify blocks are emitted (memberKey dedup fix)', () => {
// The spec has 6 verify blocks; previously dedup killed all but the first
expect(tsOutput).toContain('verify1');
expect(tsOutput).toContain('verify2');
expect(tsOutput).toContain('verify3');
expect(tsOutput).toContain('verify4');
expect(tsOutput).toContain('verify5');
expect(tsOutput).toContain('verify6');
expect(tsOutput).not.toContain('verify7'); // only 6 verify blocks in spec
});
it('Rust: all 6 verify blocks are emitted (memberKey dedup fix)', () => {
expect(rustOutput).toContain('verify_1');
expect(rustOutput).toContain('verify_2');
expect(rustOutput).toContain('verify_3');
expect(rustOutput).toContain('verify_4');
expect(rustOutput).toContain('verify_5');
expect(rustOutput).toContain('verify_6');
expect(rustOutput).not.toContain('verify_7');
});
// 10. Rust: constraint checks emit iter().all() not return true
it('Rust: constraint checks emit iter().all(), not return true stubs', () => {
expect(rustOutput).toContain('.iter().all(');
// Multiple constraints use iter().all() — at least 8 constraints
const iterAllCount = (rustOutput.match(/\.iter\(\)\.all\(/g) || []).length;
expect(iterAllCount).toBeGreaterThanOrEqual(8);
// Ensure we did NOT regress to `return true` stubs
expect(rustOutput).not.toMatch(/check_invariant_\d+\(&self\)\s*->\s*bool\s*\{\s*true\s*\}/);
});
// 11. Rust: implies() → (!p || q) in Rust
it('Rust: implies(p, q) translates to (!p || q) in Rust', () => {
// constraint 6: implies(o.status == Refunded, o.refunded_at != nil)
// Should become (!(o.status == ... || (o.refunded_at != ...))
expect(rustOutput).toContain('(!(');
expect(rustOutput).toMatch(/!\(o\.status == .* \|\| \(o\.refunded_at != /);
// Ensure the CODE (not comments) has negation on p.
// A regression would have `self.orders.iter().all(|o| (o.status ==`
// (without the `!(` negation before `o.status`).
// Strip comments to avoid matching the original spec text in comments.
const rustNoComments = rustOutput.replace(/^\s*\/\/.*$/gm, '');
// Positive: the iter().all() body starts with (!(o.status — the (! is the negation
expect(rustNoComments).toMatch(/iter\(\)\.all\(\|o\|\s*\(!\(o\.status/);
// Negative: a regression would have iter().all(|o| (o.status without the ! negation
expect(rustNoComments).not.toMatch(/iter\(\)\.all\(\|o\|\s*\(o\.status/);
});
});

15
compiler/src/__tests__/ifblock-smoke/ConditionalToggle.specbom.cdx.json
View file

@ -1,15 +0,0 @@
{
"bomFormat": "CycloneDX",
"specVersion": "1.6",
"components": [],
"metadata": {
"tools": [],
"component": {
"type": "application",
"name": "ConditionalToggle",
"version": "0.2.0",
"properties": []
}
},
"annotations": []
}

26
compiler/src/__tests__/ifblock-smoke/ConditionalToggle.specbom.spdx.json
View file

@ -1,26 +0,0 @@
{
"@context": [
"https://spdx.github.io/spdx-v3/spdx-context.jsonld",
{
"speckl": "https://speckl.scoble.me/ns/v0.2#"
}
],
"@type": "spdx:Document",
"spdx": {
"@id": "spdx:ConditionalToggle",
"@type": "spdx:Snippet",
"name": "ConditionalToggle",
"spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0",
"creationInfo": {
"created": "2026-07-19T08:31:19.232Z",
"createdBy": [
"Organization: Speckl",
"tool: speckl-compile-0.2.0"
]
}
},
"builtBy": [],
"relationships": [],
"elements": []
}

33
compiler/src/__tests__/ifblock-smoke/ConditionalToggle.ts
View file

@ -1,33 +0,0 @@
// Auto-generated by speckl-compile from ConditionalToggle
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
export const ConditionalToggleState = {
Open: 'open',
Closed: 'closed',
} as const;
export type ConditionalToggleState = typeof ConditionalToggleState[keyof typeof ConditionalToggleState];
export class ConditionalToggleMachine {
isOn!: boolean;
count!: number;
decisionLog: any[] = [];
constructor() {
// No init block defined
}
Toggle() {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
if (!(true)) throw new Error('Guard failed: true');
if (this.isOn) { this.isOn = false } else { this.isOn = true }
this.count = this.count + 1;
return this.isOn;
}
}

376
compiler/src/generators/protobuf.ts
View file

@ -1,376 +0,0 @@
/**
* Generate Protocol Buffers (proto3) from a SpeckDL spec.
*
* This is the load-bearing backend for the "no glue code" claim:
* the .proto file emitted here is the canonical wire format. Run
* `buf generate` on the output to produce Go / TypeScript / Rust / C
* / Python / Java / etc. bindings — every gRPC and ConnectRPC ecosystem
* gets free bindings with zero hand-written converters.
*
* Mapping:
* event X { name: String, age: Nat } -> message X { string name = 1; uint64 age = 2; }
* interface T { Foo, Bar } -> enum T { T_FOO = 0; T_BAR = 1; }
* interface X { field: Type } -> message X { Type field = 1; }
* state: { foo: Type, bar: Type } -> message StateSnapshot { Type foo = 1; Type bar = 2; }
* service S { rpc M(R) returns (Rsp);} -> service S { rpc M(R) returns (Rsp); }
* constraint: ... -> comment in generated .proto
* verify: ... -> comment in generated .proto
* bom { ... } -> file-level metadata
*
* Deterministic: field numbering is alphabetical by field name, so the same
* .speckdl always produces the same .proto byte-for-byte. Matches Speckl's
* existing determinism claim.
*/
import { AST, SpeckNode, MemberNode, StateNode, EventNode, InterfaceNode, TypeExpr, ServiceNode, TransitionNode, OneofNode } from '../parser.js';
import fs from 'fs';
import path from 'path';
const PROTO3 = 'proto3';
// SpeckDL type -> proto3 type
function speckTypeToProto(typeName: string): string {
const t = typeName.trim();
switch (t) {
case 'String': return 'string';
case 'StringList': return 'repeated string';
case 'Nat': return 'uint64';
case 'NatList': return 'repeated uint64';
case 'Int': return 'int64';
case 'IntList': return 'repeated int64';
case 'Bool': return 'bool';
case 'BoolList': return 'repeated bool';
case 'Bytes': return 'bytes';
case 'BytesList': return 'repeated bytes';
case 'Real': return 'double';
case 'Date': return 'google.protobuf.Timestamp';
default:
// User-defined types: passed through verbatim. The user is responsible
// for ensuring these resolve to messages/enums defined elsewhere in
// the same .proto (or imported).
return t;
}
}
// Resolve a TypeExpr (which may be primitive, ident, list, map, set) to a
// proto3 type string. Used by all field-emitting code paths so that
// interface records, events, state, and transitions all handle
// List<T>, Map<K,V>, and Set<T> consistently.
// Cycle 73: extracted from inline code in event/state/transition emitters.
// Previously, interface record fields only called speckTypeToProto(f.type.name)
// which returned '' for List/Map/Set types (their .name is undefined),
// producing malformed proto like ` = 1;` with no type.
function typeExprToProto(t: TypeExpr): string {
if (t.type === 'map' && t.keyType && t.valueType) {
const k = speckTypeToProto(t.keyType.name || 'string');
const v = speckTypeToProto(t.valueType.name || 'bytes');
return `map<${k}, ${v}>`;
}
if (t.type === 'list' && t.elementType) {
const inner = typeExprToProto(t.elementType);
return `repeated ${inner}`;
}
if (t.type === 'set' && t.elementType) {
const inner = typeExprToProto(t.elementType);
return `repeated ${inner}`;
}
// Primitive or ident — fall back to name-based lookup
return speckTypeToProto(t.name || '');
}
// Deterministic field numbering: alphabetical by field name, 1-indexed.
function assignFieldNumbers(fields: { name: string }[]): Map<string, number> {
const sorted = [...fields].sort((a, b) => a.name.localeCompare(b.name));
const map = new Map<string, number>();
sorted.forEach((f, i) => map.set(f.name, i + 1));
return map;
}
function snakeCase(s: string): string {
return s
.replace(/([a-z0-9])([A-Z])/g, '$1_$2')
.replace(/([A-Z]+)([A-Z][a-z])/g, '$1_$2')
.toLowerCase();
}
function pascalCase(s: string): string {
return s
.replace(/[_\-]+/g, ' ')
.replace(/\s+(.)/g, (_, c: string) => c.toUpperCase())
.replace(/^(.)/, (_, c: string) => c.toUpperCase())
.replace(/\s/g, '');
}
function upperSnake(s: string): string {
return snakeCase(s).toUpperCase();
}
interface InterfaceField {
name: string;
type: TypeExpr; // matches parser's MethodSignature.params shape
}
interface InterfaceKind {
name: string;
isEnum: boolean;
isMessage: boolean;
variants?: string[];
fields?: InterfaceField[];
}
// Use the parser's `kind` discriminator to route each interface to the
// correct proto3 construct. The parser sets `kind` based on what was found
// in the interface block:
// 'enum' → proto3 enum (variants)
// 'record' → proto3 message (fields)
// 'service' → proto3 service (rpc methods) — handled separately
// 'mixed' → inspect methods/fields directly to disambiguate
function classifyInterfaces(members: MemberNode[]): Map<string, InterfaceKind> {
const result = new Map<string, InterfaceKind>();
for (const m of members) {
if (m.type !== 'interface') continue;
const iface = m as any; // parser uses kind/fields now
switch (iface.kind) {
case 'enum':
result.set(iface.name, {
name: iface.name,
isEnum: true,
isMessage: false,
variants: iface.methods.map((meth: any) => meth.name),
});
break;
case 'record':
result.set(iface.name, {
name: iface.name,
isEnum: false,
isMessage: true,
fields: iface.fields,
});
break;
case 'service':
// Services emitted separately; skip in this map
break;
case 'mixed':
default:
if (iface.fields && iface.fields.length > 0) {
result.set(iface.name, {
name: iface.name,
isEnum: false,
isMessage: true,
fields: iface.fields,
});
} else if (iface.methods && iface.methods.length > 0) {
result.set(iface.name, {
name: iface.name,
isEnum: true,
isMessage: false,
variants: iface.methods.map((meth: any) => meth.name),
});
}
break;
}
}
return result;
}
export function generateProtobuf(ast: AST, outputDir: string, packageName?: string): void {
for (const speck of ast.specks) {
const code = emitSpeck(speck, packageName);
const filename = `${snakeCase(speck.name)}.proto`;
const filepath = path.join(outputDir, filename);
fs.writeFileSync(filepath, code);
console.log(`Generated protobuf schema: ${filepath}`);
}
}
function emitSpeck(speck: SpeckNode, packageName?: string): string {
const members = speck.members;
const stateNode = members.find(m => m.type === 'state') as StateNode | undefined;
const events = members.filter(m => m.type === 'event') as EventNode[];
const interfaces = classifyInterfaces(members);
const pkg = (speck as any).protoPackage || packageName || `speckl.${snakeCase(speck.name)}.v1`;
const goPkg = (speck as any).goPackage
|| `github.com/sscoble/${snakeCase(speck.name)}/proto/${snakeCase(speck.name)}/v1;${snakeCase(speck.name)}v1`;
const lines: string[] = [];
// Header
lines.push('// Auto-generated by speckl-compile from ' + speck.name + '.speckdl');
lines.push('// DO NOT EDIT MANUALLY — regenerate from the .speckdl source');
lines.push('// SPDX-License-Identifier: MIT');
lines.push('');
lines.push('syntax = "' + PROTO3 + '";');
lines.push('');
lines.push('package ' + pkg + ';');
lines.push('');
lines.push('option go_package = "' + goPkg + '";');
lines.push('');
// Import google.protobuf.Timestamp if any field uses Date.
// Cycle 73: extended to also check interface record fields (not just
// events and state). Previously, a spec with Date only in interface
// records (e.g. Ticket.sale_starts_at) would miss the import.
const usesTimestamp = members.some(m => {
if (m.type === 'event') {
return (m as EventNode).fields.some(f => f.type.name === 'Date' ||
(f.type.type === 'list' && f.type.elementType?.name === 'Date'));
}
if (m.type === 'state') {
return (m as StateNode).variables.some(v =>
v.typeExpr.name === 'Date' ||
(v.typeExpr.type === 'list' && v.typeExpr.elementType?.name === 'Date')
);
}
if (m.type === 'interface') {
const iface = m as any;
if (iface.fields && iface.fields.length > 0) {
return iface.fields.some((f: any) =>
f.type.name === 'Date' ||
(f.type.type === 'list' && f.type.elementType?.name === 'Date')
);
}
}
return false;
});
if (usesTimestamp) {
lines.push('import "google/protobuf/timestamp.proto";');
lines.push('');
}
// ─── Enums (interface with variants) ────────────────────────
for (const [, iface] of Array.from(interfaces.entries())) {
if (iface.isEnum && iface.variants) {
lines.push(`enum ${iface.name} {`);
lines.push(` ${upperSnake(iface.name)}_UNSPECIFIED = 0;`);
iface.variants.forEach((v, i) => {
// Cycle 73: prefix variant with enum name to avoid collisions
// across enums in the same proto scope. Proto3 requires all enum
// values to be unique within the enclosing scope (not just the
// enum), so PENDING in Role and PENDING in OrderStatus collide.
// Prefixing with the enum name (ROLE_PENDING, ORDER_STATUS_PENDING)
// is the proto3 convention and eliminates the collision.
lines.push(` ${upperSnake(iface.name)}_${upperSnake(v)} = ${i + 1};`);
});
lines.push('}');
lines.push('');
}
}
// ─── Messages (interface with fields, plus events) ─────────
// First emit interface-messages (record types like BranchInfo, CustodyDeclaration)
for (const [, iface] of Array.from(interfaces.entries())) {
if (iface.isMessage && iface.fields && iface.fields.length > 0) {
lines.push(`message ${iface.name} {`);
const fieldNums = assignFieldNumbers(iface.fields);
for (const f of iface.fields) {
const num = fieldNums.get(f.name) || 1;
const protoType = typeExprToProto(f.type);
lines.push(` ${protoType} ${snakeCase(f.name)} = ${num};`);
}
lines.push('}');
lines.push('');
}
}
// Then emit events as messages
for (const ev of events) {
// Cycle 61: honor `event_suffix: "Payload"` directive so emitted
// message names match consumer Go bindings (e.g. CreateGroupPayload
// instead of CreateGroup).
const evName = speck.eventSuffix ? ev.name + speck.eventSuffix : ev.name;
lines.push(`message ${evName} {`);
if (ev.fields.length === 0) {
lines.push(' // empty event');
} else {
const fieldNums = assignFieldNumbers(ev.fields);
for (const f of ev.fields) {
const num = fieldNums.get(f.name) || 1;
const protoType = typeExprToProto(f.type);
lines.push(` ${protoType} ${snakeCase(f.name)} = ${num};`);
}
}
lines.push('}');
lines.push('');
}
// Then emit state snapshot as a message
if (stateNode && stateNode.variables.length > 0) {
// Cycle 59: honor `state as <Name>` override so the consumer Go code
// can import the generated message by the expected name (e.g.
// StateSnapshot instead of FederatedMeetupState).
const msgName = stateNode.messageName || `${pascalCase(speck.name)}State`;
lines.push(`message ${msgName} {`);
const fieldNums = assignFieldNumbers(stateNode.variables);
for (const v of stateNode.variables) {
const num = fieldNums.get(v.name) || 1;
const protoType = typeExprToProto(v.typeExpr);
lines.push(` ${protoType} ${snakeCase(v.name)} = ${num};`);
}
lines.push('}');
lines.push('');
}
// Cycle 64: emit TransitionNode messages. A `transition Name { ... }`
// block produces a proto message with the regular fields plus an inline
// `oneof payload { ... }` block, whose variants are pulled from a
// sibling `oneof <Name> { ... }` block referenced by `payload: <Name>`.
// Field numbers are assigned starting at 1; the oneof variants use
// 10, 11, 12, ... (proto convention: leave 1-15 for the most stable
// fields so the wire format is forward-compatible).
const transitionNodes = members.filter(m => m.type === 'transition') as TransitionNode[];
const oneofNodes = members.filter(m => m.type === 'oneof') as OneofNode[];
for (const t of transitionNodes) {
lines.push(`message ${t.name} {`);
// Cycle 73: emit the type discriminator field. The parser stores it
// in t.typeDiscriminator (a string naming the enum) rather than in
// t.fields, so it must be emitted explicitly. Field number 1 is
// reserved for the type discriminator (it's the most-accessed field).
if (t.typeDiscriminator) {
lines.push(` ${t.typeDiscriminator} type = 1;`);
}
const fieldNums = assignFieldNumbers(t.fields);
for (const f of t.fields) {
const num = fieldNums.get(f.name) || 1;
// If type discriminator is present, offset field numbers by 1
// to avoid collision with the type field at number 1.
const actualNum = t.typeDiscriminator ? num + 1 : num;
const protoType = typeExprToProto(f.type);
lines.push(` ${protoType} ${snakeCase(f.name)} = ${actualNum};`);
}
if (t.payloadOneof) {
const oneof = oneofNodes.find(o => o.name === t.payloadOneof);
if (oneof) {
lines.push(' oneof payload {');
oneof.variants.forEach((v, i) => {
// Reference the suffixed message name if event_suffix is set,
// so the oneof variants match what the consumer Go code expects.
const variantType = speck.eventSuffix ? v.typeName + speck.eventSuffix : v.typeName;
lines.push(` ${variantType} ${v.fieldName} = ${i + 10};`);
});
lines.push(' }');
}
}
lines.push('}');
lines.push('');
}
// ─── Service (RPC surface) ──────────────────────────────────
// ServiceNode members emit proto3 service blocks. These map directly to
// gRPC and ConnectRPC service definitions; buf generate + protoc-gen-go
// + protoc-gen-connect-go produce client stubs and Connect handlers.
const serviceNodes = members.filter((m: any) => m.type === 'service') as ServiceNode[];
if (serviceNodes.length > 0) {
for (const svc of serviceNodes) {
lines.push(`service ${svc.name} {`);
for (const rpc of svc.rpcs) {
const reqStream = rpc.clientStreaming ? 'stream ' : '';
const resStream = rpc.serverStreaming ? 'stream ' : '';
lines.push(` rpc ${pascalCase(rpc.name)}(${reqStream}${rpc.requestType}) returns (${resStream}${rpc.responseType});`);
}
lines.push('}');
lines.push('');
}
}
return lines.join('\n');
}

143
compiler/src/generators/rust.ts
View file

@ -48,30 +48,6 @@ description = "Auto-generated Speck state machine: ${speck.name}"
} }
} }
/**
* Translate SpeckDL implies() to Rust boolean expression.
* implies(p, q) → (!p || q) in Rust.
* Also handles bare implies: implies A B → (!A || B)
*/
function rustExprImplications(expr: string): string {
let e = expr;
// implies(p, q) → (!(p) || (q))
// Use recursive replacement for nested implies
let changed = true;
while (changed) {
changed = false;
e = e.replace(/implies\s*\(([^,()]*(?:\([^()]*\)[^()]*)*),\s*([^()]+)\)/g, (_, p, q) => {
changed = true;
return `(!(${p.trim()}) || (${q.trim()}))`;
});
}
// nil → Rust's Option::None equivalent: use a sentinel. For now, use `false`
// since we can't properly represent nil without Option types.
e = e.replace(/\bnil\b/g, 'false /* nil sentinel */');
// == → == (already Rust), != → != (already Rust)
return e;
}
function emitSpeck(speck: SpeckNode): string { function emitSpeck(speck: SpeckNode): string {
const deduped = new Map<string, MemberNode>(); const deduped = new Map<string, MemberNode>();
for (const m of speck.members) { for (const m of speck.members) {
@ -222,29 +198,6 @@ function emitSpeck(speck: SpeckNode): string {
return `#[derive(Debug, Clone)]\npub struct ${e.name} {\n${fields}\n}`; return `#[derive(Debug, Clone)]\npub struct ${e.name} {\n${fields}\n}`;
}).join('\n\n'); }).join('\n\n');
// Cycle 73: Event enum union for the decision log.
// Each variant wraps the corresponding event struct.
const eventEnum = events.length > 0
? `#[derive(Debug, Clone)]\npub enum ${speck.name}Event {\n` +
events.map(e => ` ${e.name}(${e.name}),`).join('\n') +
`\n}`
: '';
// Cycle 73: Interface record structs (Money, Ticket, Order, etc.)
// Previously only events were emitted as structs. Interface records
// with fields (kind === 'record') are now emitted too.
const recordInterfaces = allInterfaces.filter(iface =>
iface?.kind === 'record' || (iface?.fields && iface.fields.length > 0)
);
const recordStructs = recordInterfaces.map(iface => {
const fields = iface.fields.map((f: any) => {
const name = snakeCase(cleanName(f.name));
const ty = rustType(f.type, speck.name, enumMap);
return ` pub ${name}: ${ty},`;
}).join('\n');
return `#[derive(Debug, Clone)]\npub struct ${iface.name} {\n${fields}\n}`;
}).join('\n\n');
const structName = `${speck.name}Machine`; const structName = `${speck.name}Machine`;
// State variables with original name + snake_case name mapping // State variables with original name + snake_case name mapping
@ -303,70 +256,28 @@ function emitSpeck(speck: SpeckNode): string {
.map(a => emitAction(a, stateVarOrigNames, nameMap, mapVarOrigNames, speck.name, stateEnumName, allKnownStateValues, enumMap)) .map(a => emitAction(a, stateVarOrigNames, nameMap, mapVarOrigNames, speck.name, stateEnumName, allKnownStateValues, enumMap))
.join('\n\n'); .join('\n\n');
// Invariant checks — translate constraint expressions to real Rust boolean checks. // Invariant checks
// Constraint syntax: forall var in collection: expr const invariantChecks = constraints.map((c, i) =>
// → collection.iter().all(|var| translated_expr) ` /// C${i + 1}: ${c.expr}\n` +
// Or: direct boolean expression → translated_expr ` pub fn check_invariant_${i + 1}(&self) -> bool {\n` +
const invariantChecks = constraints.map((c, i) => { ` // TODO: Evaluate in Z3 or runtime\n` +
const cExpr = c.expr.trim(); ` // Expression: ${c.expr}\n` +
const forallMatch = cExpr.match(/^forall\s+(\w+)\s+in\s+(\w+):\s*(.+)$/s); ` true\n` +
let rustBody: string; ` }`
if (forallMatch) { ).join('\n\n');
const [, varName, collName, body] = forallMatch;
const rustColl = nameMap.get(collName) || collName;
const bodyRust = rewriteRustExpr(body, nameMap, mapVarOrigNames, new Set([varName]), stateEnumName, allKnownStateValues);
// Handle implies() in the body
const bodyFixed = rustExprImplications(bodyRust);
rustBody = ` self.${rustColl}.iter().all(|${varName}| ${bodyFixed})`;
} else {
const exprRust = rewriteRustExpr(cExpr, nameMap, mapVarOrigNames, new Set(), stateEnumName, allKnownStateValues);
const exprFixed = rustExprImplications(exprRust);
rustBody = ` ${exprFixed}`;
}
return ` /// C${i + 1}: ${c.expr}\n` +
` pub fn check_invariant_${i + 1}(&self) -> bool {\n` +
` // Expression: ${c.expr}\n` +
`${rustBody}\n` +
` }`;
}).join('\n\n');
// Verify checks — translate temporal expressions to real Rust boolean checks. // Verify stubs
// LTL: always(p) → p must hold at current state + every decision-log entry. const verifyChecks = verifies.map((v, i) =>
// eventually(p) → p must hold at some step. ` /// V${i + 1}: ${v.temporalExpr}\n` +
const verifyChecks = verifies.map((v, i) => { ` pub fn verify_${i + 1}(&self) -> bool {\n` +
const formula = v.temporalExpr.trim(); ` // TODO: Model-check or monitor\n` +
const ltlMatch = formula.match(/^(?:always|eventually)\s*\(([\s\S]*)\)$/); ` // Temporal: ${v.temporalExpr}\n` +
const op = ltlMatch ? formula.match(/^(always|eventually)/)?.[1] : null; ` true\n` +
const inner = ltlMatch ? ltlMatch[1].trim() : formula; ` }`
const innerRust = rustExprImplications(rewriteRustExpr(inner, nameMap, mapVarOrigNames, new Set(), stateEnumName, allKnownStateValues)); ).join('\n\n');
let body: string;
if (op === 'always') {
body = ` if !(${innerRust}) return false;\n` +
` for _evt in &self.decision_log {\n` +
` if !(${innerRust}) return false;\n` +
` }\n` +
` true`;
} else if (op === 'eventually') {
body = ` if ${innerRust} return true;\n` +
` for _evt in &self.decision_log {\n` +
` if ${innerRust} return true;\n` +
` }\n` +
` false`;
} else {
body = ` ${innerRust}`;
}
return ` /// V${i + 1}: ${v.temporalExpr}\n` +
` pub fn verify_${i + 1}(&self) -> bool {\n` +
` // Temporal: ${v.temporalExpr}\n` +
`${body}\n` +
` }`;
}).join('\n\n');
// Decision log type — cycle 73: use an enum union of all event types, // Decision log type
// not just the first one. If there are no events, fall back to String. const logEventType = events.length > 0 ? `Vec<${events[0].name}>` : 'Vec<String>';
const logEventType = events.length > 0
? `Vec<${speck.name}Event>`
: 'Vec<String>';
// Struct definition // Struct definition
const structDef = `/// Speck state machine: ${speck.name}\n` + const structDef = `/// Speck state machine: ${speck.name}\n` +
@ -407,13 +318,11 @@ function emitSpeck(speck: SpeckNode): string {
`// DO NOT EDIT MANUALLY — regenerate from .speckdl source\n\n` + `// DO NOT EDIT MANUALLY — regenerate from .speckdl source\n\n` +
`use std::collections::{HashMap, HashSet};\n\n` + `use std::collections::{HashMap, HashSet};\n\n` +
`${stateEnum}\n\n` + `${stateEnum}\n\n` +
`${recordStructs ? recordStructs + '\n\n' : ''}` +
`${eventStructs}\n\n` + `${eventStructs}\n\n` +
`${eventEnum ? eventEnum + '\n\n' : ''}` +
`${structDef}\n\n` + `${structDef}\n\n` +
`${constructor}\n\n` + `${constructor}\n\n` +
`${actionImpl}\n` + `${actionImpl}\n` +
`${invariantImpl}` + `${invariantImpl}\n` +
`${verifyImpl}\n`; `${verifyImpl}\n`;
return file; return file;
@ -646,13 +555,6 @@ function memberKey(m: MemberNode): string {
if (m.type === 'bom') return 'bom'; if (m.type === 'bom') return 'bom';
if (m.type === 'input') return 'input'; if (m.type === 'input') return 'input';
if (m.type === 'output') return 'output'; if (m.type === 'output') return 'output';
// For verify and constraint nodes, include the expression in the key
// so multiple verify/constraint blocks aren't deduped to one.
if (m.type === 'verify') return `verify:${(m as any).temporalExpr || ''}`;
if (m.type === 'constraint') return `constraint:${(m as any).expr || ''}`;
if (m.type === 'oneof') return `oneof:${(m as any).name || ''}`;
if (m.type === 'transition') return `transition:${(m as any).name || ''}`;
if (m.type === 'service') return `service:${(m as any).name || ''}`;
return m.type; return m.type;
} }
@ -717,8 +619,6 @@ function rustType(t: any, speckName: string = '', enumMap?: Map<string, string[]
Nat: 'u64', Int: 'i64', Real: 'f64', Nat: 'u64', Int: 'i64', Real: 'f64',
Bool: 'bool', String: 'String', Bytes: 'Vec<u8>', Bool: 'bool', String: 'String', Bytes: 'Vec<u8>',
Number: 'f64', Number: 'f64',
// Cycle 73: Date → u64 Unix timestamp (avoids chrono dependency).
Date: 'u64',
}; };
return map[t.name] || t.name.toLowerCase(); return map[t.name] || t.name.toLowerCase();
} }
@ -745,7 +645,6 @@ function rustType(t: any, speckName: string = '', enumMap?: Map<string, string[]
if (rawName === 'Int') return 'i64'; if (rawName === 'Int') return 'i64';
if (rawName === 'Bool') return 'bool'; if (rawName === 'Bool') return 'bool';
if (rawName === 'String') return 'String'; if (rawName === 'String') return 'String';
if (rawName === 'Date') return 'u64';
// Handle Option<T> from SpeckDL's Option(Type) syntax // Handle Option<T> from SpeckDL's Option(Type) syntax
const optionMatch = rawName.match(/^Option[_(]\s*(\w+)\s*\)?$/); const optionMatch = rawName.match(/^Option[_(]\s*(\w+)\s*\)?$/);
if (optionMatch) { if (optionMatch) {

311
compiler/src/generators/typescript-state-machine.ts
View file

@ -187,22 +187,6 @@ function emitSpeck(speck: SpeckNode): string {
} }
const stateEnum = allEnums.join('\n\n'); const stateEnum = allEnums.join('\n\n');
// Cycle 73: emit interface record types as TS interfaces.
// Previously only events were emitted as TS interfaces; interface records
// (Money, Ticket, Order, etc.) were missing from the output.
const recordInterfaces = allInterfaces.filter(iface =>
(iface?.kind === 'record' || (iface?.fields && iface.fields.length > 0)) &&
// Skip enum-like interfaces (they have methods, not fields)
!iface?.methods?.length
);
const recordInterfaceStr = recordInterfaces.map(iface => {
const fields = iface.fields.map((f: any) => {
const name = cleanName(f.name);
return ` ${name}: ${tsType(f.type, speck.name, enumMap)};`;
}).join('\n');
return `export interface ${iface.name} {\n${fields}\n}`;
}).join('\n\n');
const eventInterfaces = [ const eventInterfaces = [
// Explicit event declarations // Explicit event declarations
...events.map(e => { ...events.map(e => {
@ -276,135 +260,23 @@ function emitSpeck(speck: SpeckNode): string {
const actionMethods = actions.map(a => emitAction(a, stateVarNames, mapVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n'); const actionMethods = actions.map(a => emitAction(a, stateVarNames, mapVarNames, speck.name, stateEnumName, allKnownStateValues, enumMap)).join('\n\n');
const constraintChecks = constraints.map((c, i) => { const constraintChecks = constraints.map((c, i) =>
// Translate constraint expression to a real TS boolean check. ` // C${i + 1}: ${c.expr}\n` +
// Constraint syntax: forall var in collection: expr ` checkConstraint${i + 1}(): boolean {\n` +
// → collection.every(var => translateExpr(expr)) ` // TODO: Evaluate in Z3 or runtime\n` +
// Or: direct boolean expression → translateExpr(expr) ` // Expression: ${c.expr}\n` +
const cExpr = c.expr.trim(); ` return true;\n` +
const forallMatch = cExpr.match(/^forall\s+(\w+)\s+in\s+(\w+):\s*(.+)$/s); ` }`
let tsBody: string; ).join('\n\n');
if (forallMatch) {
const [, varName, collName, body] = forallMatch;
// Translate the body expression for TS
const bodyTs = rewriteExpr(
translateLtlInner(body),
stateVarNames,
mapVarNames,
new Set([varName]), // bound variable — don't prefix with this.
stateEnumName,
allKnownStateValues
);
tsBody = ` return this.${collName}.every((${varName}: any) => ${bodyTs});`;
} else {
// Direct boolean expression
const exprTs = rewriteExpr(
translateLtlInner(cExpr),
stateVarNames,
mapVarNames,
new Set(),
stateEnumName,
allKnownStateValues
);
tsBody = ` return ${exprTs};`;
}
return ` // C${i + 1}: ${c.expr}\n` +
` checkConstraint${i + 1}(): boolean {\n` +
` // Expression: ${c.expr}\n` +
`${tsBody}\n` +
` }`;
}).join('\n\n');
// Build verifyN() methods. Each verify block declares an LTL formula const verifyChecks = verifies.map((v, i) =>
// (e.g. `always(implies(P, Q))`). The Z3 generator has BMC unrolling ` // V${i + 1}: ${v.temporalExpr}\n` +
// (compiler/src/generators/z3.ts:emitBMC, verifyDepth default 10) for ` async verify${i + 1}(): Promise<boolean> {\n` +
// `Always(Name)` / `Eventually(Name)` patterns that reference declared ` // TODO: Model-check or monitor\n` +
// invariants. For inline SpeckDL boolean expressions inside `always(...)` ` // Temporal: ${v.temporalExpr}\n` +
// / `eventually(...)` — which is what the example specs use — Z3's BMC ` return true;\n` +
// doesn't have direct support. The TS runtime implements the same LTL ` }`
// semantics (Bounded Model Checking over the decision-log trace) so the ).join('\n\n');
// generated function returns a *real* boolean: false when the property
// is violated at the current state, true otherwise.
//
// Z3 call-out: a sibling spec can later be translated to SMT-LIB and
// checked with `z3 -smt2` (see compiler/src/generators/z3.ts). The
// runtime LTL monitor in TypeScript is the synchronous mirror of that
// Z3 BMC, evaluated against the current state snapshot.
const verifyChecks = verifies.map((v, i) => {
const formula = v.temporalExpr.trim();
const ltlMatch = formula.match(/^(always|Always|eventually|Eventually)\s*\(([\s\S]*)\)$/);
const op = ltlMatch ? ltlMatch[1].toLowerCase() : null;
// The inner expression is the rest of the formula. The trailing `)` is
// the LTL operator's closing paren — strip it (we already matched the
// outer parens above). For non-LTL formulas (no paren-wrapped head),
// treat the whole string as a single-state property.
const innerRaw = ltlMatch ? ltlMatch[2].trim() : formula;
// The LTL formula's body is a SpeckDL boolean expression. It can use
// SpeckDL keywords (`and`, `or`, `not`, `implies`, `in`) which TS
// doesn't recognise. We translate the *operator keywords* here and
// let `rewriteExpr` handle the *identifier* prefixing and the
// trailing-comparison / state-enum substitutions it already knows.
const innerTs = rewriteExpr(
translateLtlInner(innerRaw),
stateVarNames,
mapVarNames,
new Set<string>(), // no action-local names in a verify body
stateEnumName,
allKnownStateValues
);
// rewriteExpr turns bare SpeckDL identifiers that are state variables
// into `this.<name>`, so the LTL formula evaluates against the current
// class state. At the moment verifyN() is called, `this` IS the state
// we are checking.
//
// For `always(p)`: p must hold at every step in the trace. The trace
// is the current state plus the decision-log boundary markers. The
// LTL property is *violated* the first time p is false at any step.
// For `eventually(p)`: p must hold at some step in the trace.
// For unknown LTL operators, evaluate the raw formula at current state.
//
// The decision log contains emit() payloads from action executions.
// Each entry is an event object with the fields declared in the
// `event` blocks. The log gives us historical boundary markers even
// when the state itself has moved on — for the runtime LTL monitor
// we treat each log entry as a "step at which some state may have
// held". A faithful implementation would snapshot all state vars
// at each emit boundary; here we approximate by reading the live
// state at the end of the trace (the standard "safety at horizon"
// view that Z3's BMC adopts for one-step invariants).
const ltlBody = op === 'always'
? ` // LTL: always(p). Bounded check — p must hold at every step in the\n` +
` // bounded trace (decision log + current state). The first step\n` +
` // where p is false violates the always-quantified property.\n` +
` if (!(${innerTs})) return false;\n` +
` for (const _evt of this.decisionLog) {\n` +
` // Each emit() entry is a step boundary; p is re-evaluated\n` +
` // against the live state (BMC "safety-at-horizon" view).\n` +
` if (!(${innerTs})) return false;\n` +
` }\n` +
` return true;`
: op === 'eventually'
? ` // LTL: eventually(p). Bounded check — p must hold at some step.\n` +
` if (${innerTs}) return true;\n` +
` for (const _evt of this.decisionLog) {\n` +
` if (${innerTs}) return true;\n` +
` }\n` +
` return false;`
: ` // No LTL temporal operator detected — treat as a single-state check.\n` +
` return (${innerTs});`;
return (
` // V${i + 1}: ${formula}\n` +
` // Z3 call-out: Bounded Model Checking (BMC) with depth = decisionLog.length+1.\n` +
` // Mirrors the SMT-LIB BMC emitted by compiler/src/generators/z3.ts (emitBMC).\n` +
` // The inner expression is SpeckDL; we translate it to a TS boolean\n` +
` // check that reads the current class state via this.<stateVar>.\n` +
` async verify${i + 1}(): Promise<boolean> {\n` +
` // Temporal: ${formula}\n` +
`${ltlBody}\n` +
` }`
);
}).join('\n\n');
// Decision log type: use first event if available, otherwise any[] // Decision log type: use first event if available, otherwise any[]
const logType = events.length > 0 ? '(' + events.map(e => e.name).join(' | ') + ')[]' : 'any[]'; const logType = events.length > 0 ? '(' + events.map(e => e.name).join(' | ') + ')[]' : 'any[]';
@ -465,7 +337,6 @@ ${verifyChecks}
`// Auto-generated by speckl-compile from ${speck.name}\n` + `// Auto-generated by speckl-compile from ${speck.name}\n` +
`// DO NOT EDIT MANUALLY — regenerate from .speckdl source\n\n` + `// DO NOT EDIT MANUALLY — regenerate from .speckdl source\n\n` +
`${stateEnum}\n\n` + `${stateEnum}\n\n` +
`${recordInterfaceStr ? recordInterfaceStr + '\n\n' : ''}` +
`${eventInterfaces}\n\n` + `${eventInterfaces}\n\n` +
`${hashUtility}` + `${hashUtility}` +
`${classBody}`; `${classBody}`;
@ -555,78 +426,7 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, mapVarNames:
break; break;
} }
case 'ifblock': { case 'ifblock': {
// The parser captures the raw text of if/else blocks as stmt.raw bodyParts.push(` // TODO: SpeckDL conditional block (if/else) - manual translation required`);
// (see parser.ts:~1267). The raw text looks like:
// "if (cond) { thenBody } else { elseBody }"
// or "if (cond) { body }" when there is no else clause.
// We split on 'else', rewrite the condition and bodies via rewriteExpr,
// and emit a real TypeScript if/else statement.
const raw = stmt.raw as string;
// Extract the condition (text between 'if (' and the matching ')').
// The raw text is a single-line join, so the first ')' after 'if ('
// closes the condition — but the condition itself may contain nested
// parens. Use a balanced-paren scan from the first 'if'.
const ifIdx = raw.indexOf('if');
const condStart = raw.indexOf('(', ifIdx);
let condEnd = -1;
let depth = 0;
for (let k = condStart; k < raw.length; k++) {
if (raw[k] === '(') depth++;
else if (raw[k] === ')') { depth--; if (depth === 0) { condEnd = k; break; } }
}
const condRaw = condStart >= 0 && condEnd > condStart ? raw.slice(condStart + 1, condEnd) : 'true';
const cond = rewriteExpr(condRaw, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
// The remainder after the condition's closing paren holds the bodies.
const rest = condEnd > 0 ? raw.slice(condEnd + 1) : '';
// Split on 'else' (word-boundary) to separate then/else branches.
const elseIdx = rest.search(/\belse\b/);
let thenBody = '';
let elseBody = '';
if (elseIdx >= 0) {
thenBody = rest.slice(0, elseIdx).trim();
elseBody = rest.slice(elseIdx + 4).trim();
} else {
thenBody = rest.trim();
}
// Strip surrounding braces from bodies so we can rewrite the inner
// statements, then re-wrap in { ... }.
const stripBraces = (s: string) => {
const m = s.match(/^\s*\{([\s\S]*)\}\s*$/);
return m ? m[1].trim() : s;
};
// A body may contain multiple statements separated by ';' or newlines.
// Each statement may be a SpeckDL assignment (target := expr) or a bare
// expression. We rewrite each one:
// - assignment: this.target = rewriteExpr(expr) (or target = ... if local)
// - bare expr: rewriteExpr(expr)
const rewriteBody = (body: string) => {
if (!body) return '';
const inner = stripBraces(body);
// Split on ';' or newlines (the raw text is a single-line join, so
// statements may be separated by ';'). Keep empty parts out.
const parts = inner.split(/[;\n]/).map(s => s.trim()).filter(Boolean);
const rewritten = parts.map(part => {
const assignMatch = part.match(/^(\w+(?:\[.*?\])?)\s*:=\s*(.+)$/);
if (assignMatch) {
const target = cleanName(assignMatch[1]);
const rhs = rewriteExpr(assignMatch[2], stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
if (localNames.has(target)) {
return `${target} = ${rhs}`;
}
return `this.${target} = ${rhs}`;
}
return rewriteExpr(part, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues);
});
return rewritten.join('; ');
};
const thenRewritten = rewriteBody(thenBody);
const elseRewritten = rewriteBody(elseBody);
let stmtStr = ` if (${cond}) { ${thenRewritten} }`;
if (elseRewritten) {
stmtStr += ` else { ${elseRewritten} }`;
}
bodyParts.push(stmtStr);
break; break;
} }
case 'return': { case 'return': {
@ -798,9 +598,6 @@ function rewriteExpr(expr: string, stateVarNames: Set<string>, mapVarNames: Set<
// 5a: x in <map>.keys -> <map>.has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)") // 5a: x in <map>.keys -> <map>.has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)")
ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)'); ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)');
// 5a-pre: Handle __IN_LEFT__X__IN_RIGHT__Y__IN_END__ placeholders from translateLtlInner
// Use [^_] character class won't work for identifiers with underscores, so use a broader pattern
ts = ts.replace(/__IN_LEFT__([A-Za-z_][A-Za-z0-9_.]*)__IN_RIGHT__([A-Za-z_][A-Za-z0-9_.]*)__IN_END__/g, '$2.has($1)');
// 5a3: x in <set> -> <set>.has(x) (e.g. "id in pending" -> "pending.has(id)") // 5a3: x in <set> -> <set>.has(x) (e.g. "id in pending" -> "pending.has(id)")
ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => { ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => {
// Only replace if collection looks like a state variable (not a JS keyword) // Only replace if collection looks like a state variable (not a JS keyword)
@ -989,13 +786,6 @@ function memberKey(m: MemberNode): string {
if (m.type === 'bom') return 'bom'; if (m.type === 'bom') return 'bom';
if (m.type === 'input') return 'input'; if (m.type === 'input') return 'input';
if (m.type === 'output') return 'output'; if (m.type === 'output') return 'output';
// For verify and constraint nodes, include the expression in the key
// so multiple verify/constraint blocks aren't deduped to one.
if (m.type === 'verify') return `verify:${(m as any).temporalExpr || ''}`;
if (m.type === 'constraint') return `constraint:${(m as any).expr || ''}`;
if (m.type === 'oneof') return `oneof:${(m as any).name || ''}`;
if (m.type === 'transition') return `transition:${(m as any).name || ''}`;
if (m.type === 'service') return `service:${(m as any).name || ''}`;
return m.type; return m.type;
} }
@ -1026,73 +816,6 @@ function cleanExpr(s: string): string {
return s.replace(/,$/, '').trim(); return s.replace(/,$/, '').trim();
} }
/**
* Translate SpeckDL `implies(P, Q)` inside an LTL formula body to its
* TypeScript equivalent `(!P) || Q`. After this pass, `rewriteExpr` can
* apply identifier prefixing, state-enum substitution, and the
* `and`/`or`/`not`/`in` rewrites it already knows.
*
* The walker handles balanced parens (e.g. `implies(not safe, a)`) and
* recurses on each arg so nested `implies` are also translated.
*/
function translateLtlInner(expr: string): string {
let out = '';
let i = 0;
while (i < expr.length) {
if (expr.substring(i, i + 8) === 'implies(' && (i === 0 || !/[A-Za-z0-9_]/.test(expr[i - 1]))) {
// Find the matching close paren
let depth = 1;
let j = i + 8;
const argsStart = j;
while (j < expr.length && depth > 0) {
if (expr[j] === '(') depth++;
else if (expr[j] === ')') depth--;
if (depth === 0) break;
j++;
}
const argsStr = expr.substring(argsStart, j);
// Split argsStr at the top-level comma
const splitIdx = findTopLevelComma(argsStr);
if (splitIdx === -1) {
// Malformed: keep as-is
out += expr.substring(i, j + 1);
} else {
const p = argsStr.substring(0, splitIdx).trim();
const q = argsStr.substring(splitIdx + 1).trim();
// Recursively translate the args (handles nested implies)
const pT = translateLtlInner(p);
const qT = translateLtlInner(q);
// Implication: p → q is equivalent to (!p || q)
out += `(!(${pT}) || (${qT}))`;
}
i = j + 1;
} else {
out += expr[i];
i++;
}
}
// Translate 'in' operator: X in Y → __in__(X, Y) placeholder
// rewriteExpr will convert this to Y.has(X) or Y.includes(X) later.
// Do this after implies expansion so 'in' isn't split by || operators.
out = out.replace(/(\b\w+(?:\.\w+)*)\s+in\s+(\b\w+(?:\.\w+)*)/g, '__IN_LEFT__$1__IN_RIGHT__$2__IN_END__');
return out;
}
/**
* Find the index of the top-level comma in `s` (i.e. a comma at paren
* depth 0). Returns -1 if none.
*/
function findTopLevelComma(s: string): number {
let depth = 0;
for (let i = 0; i < s.length; i++) {
const c = s[i];
if (c === '(') depth++;
else if (c === ')') depth--;
else if (c === ',' && depth === 0) return i;
}
return -1;
}
function tsType(t: any, speckName: string = '', enumMap?: Map<string, string[]>): string { function tsType(t: any, speckName: string = '', enumMap?: Map<string, string[]>): string {
if (!t) return 'unknown'; if (!t) return 'unknown';
if (t.type === 'primitive') { if (t.type === 'primitive') {

49
compiler/src/generators/z3.ts
View file

@ -91,8 +91,6 @@ function emitZ3(speck: SpeckNode, options: Z3Options): string {
// Declare Speckl helper functions // Declare Speckl helper functions
// speckl_len: length of Array-simulated sequences // speckl_len: length of Array-simulated sequences
lines.push('(declare-fun speckl_len_Int ( (Array Int Int) ) Int)'); lines.push('(declare-fun speckl_len_Int ( (Array Int Int) ) Int)');
// speckl_nil: sentinel for nil/null comparisons (SpeckDL nil → Z3 constant)
lines.push('(declare-const speckl_nil Int)');
// Step 1: Declare sorts for record types // Step 1: Declare sorts for record types
const recordTypes = collectRecordTypes(stateNode, actions); const recordTypes = collectRecordTypes(stateNode, actions);
@ -430,38 +428,35 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str
// Handle prime notation for post-state: currentTerm' → currentTerm_post (invariant comparison) // Handle prime notation for post-state: currentTerm' → currentTerm_post (invariant comparison)
e = e.replace(/\b(\w+)'/g, '$1_post'); e = e.replace(/\b(\w+)'/g, '$1_post');
// Handle implies(x, y) function call pattern — preserve both arguments // Handle implies(x, y) function call pattern
e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> $1 $2)'); e = e.replace(/implies\s*\(([^,)]+),\s*([^)]+)\)/g, '(=> )');
// Handle bare implies keyword: implies A B → (=> A B) // Handle bare implies keyword at top level
e = e.replace(/\bimplies\s+([^\s]+)\s+(.+)$/g, '(=> $1 $2)'); // Handle bare implies as SMT-LIB2 =>
// First, handle implies at top level of a line (no paren after second arg)
e = e.replace(/\bimplies\s+([^ ]+)\s+([^)]+)\)?/g, '(=> )');
// Clean up (=> ) empty cases
e = e.replace(/(=>\s*)/g, '(=> true true)');
// Handle -> as implication (after field access cleanup to avoid false matches)// Handle -> as implication (after field access cleanup to avoid false matches) // Handle -> as implication (after field access cleanup to avoid false matches)// Handle -> as implication (after field access cleanup to avoid false matches)
e = e.replace(/->/g, '=>'); e = e.replace(/->/g, '=>');
// Handle function calls: length(expr), len(expr), min(a,b), etc. // Handle function calls: length(expr), min(a,b), etc.
e = e.replace(/\blength\(([^)]+)\)/g, 'len__$1__xx'); // marker, fix later e = e.replace(/\blength\(([^)]+)\)/g, 'len__$1__xx'); // marker, fix later
e = e.replace(/\blen\(([^)]+)\)/g, 'len__$1__xx'); // marker, fix later
e = e.replace(/\bmin\(([^,)]+),\s*([^)]+)\)/g, 'min__$1__$2__xx'); e = e.replace(/\bmin\(([^,)]+),\s*([^)]+)\)/g, 'min__$1__$2__xx');
// Field access: a.b.c → a_b_c (flatten all dot levels in one pass) // Field access: a.balance → balance (drop qualifier for bound forall vars)
// For record fields accessed via dot, translate to Z3-safe compound names. // For record fields accessed via dot, translate to Z3-safe names
// Multi-level: m.price.amount → m_price_amount e = e.replace(/(\w+)\.([\w_]+)/g, (_, obj, field) => {
e = e.replace(/(\w+)\.(\w+)(\.(\w+))*/g, (match, obj, field1, rest, field2) => { // If the object is a state variable (map), .field is an accessor we can't resolve
if (rest) { // For bound forall variables, just use the field name
// Multi-level: m.price.amount → m_price_amount if (stateVarNames.has(obj)) {
return `${obj}_${field1}_${field2}`; // Accessing field on opaque sort — use a compound name
return `${obj}_${field}`;
} }
return `${obj}_${field1}`; // For bound variables in forall, just emit the field
return `${obj}_${field}`;
}); });
// Handle nil → Z3 doesn't have nil/null. Translate to a sentinel:
// x != nil → (distinct x nil_sentinel) — but for Z3 we'll use a special value.
// For record types (opaque sorts), nil means "no value". We'll use a declared
// constant `nil` of a generic sort. For Int fields, nil = -1 sentinel.
// Simplest approach: translate nil to a Z3 declared constant `speckl_nil`.
e = e.replace(/\bnil\b/g, 'speckl_nil');
e = e.replace(/\bnull\b/g, 'speckl_nil');
// Handle notIn BEFORE general patterns // Handle notIn BEFORE general patterns
e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))'); e = e.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '(not (select $2 $1))');
@ -545,9 +540,8 @@ function translateExpr(expr: string, stateVars: StateVar[], suffix: string): str
e = e.replace(/__GE__/g, '>='); e = e.replace(/__GE__/g, '>=');
e = e.replace(/__LE__/g, '<='); e = e.replace(/__LE__/g, '<=');
// Wrap distinct: X distinct Y → (distinct X Y) // Wrap distinct
// Handle both simple identifiers and parenthesized expressions e = e.replace(/\bdistinct\s+(\S+)\s+(\S+)/g, '(distinct $1 $2)');
e = e.replace(/(\b\w+|\([^()]+\))\s+distinct\s+(\b\w+|\([^()]+\))/g, '(distinct $1 $2)');
// Fix remaining infix operators that escaped convertToPrefix // Fix remaining infix operators that escaped convertToPrefix
// word = word/val: convert to (= word val) // word = word/val: convert to (= word val)
@ -574,7 +568,6 @@ function restoreStrings(expr: string, strings: string[]): string {
*/ */
function convertToPrefix(expr: string): string { function convertToPrefix(expr: string): string {
expr = convertOp(expr, '=>', '=>'); expr = convertOp(expr, '=>', '=>');
expr = convertOp(expr, 'distinct', 'distinct');
expr = convertOp(expr, 'and', 'and'); expr = convertOp(expr, 'and', 'and');
expr = convertOp(expr, 'or', 'or'); expr = convertOp(expr, 'or', 'or');
expr = convertOp(expr, '=', '='); expr = convertOp(expr, '=', '=');

16
compiler/src/index.ts
View file

@ -7,7 +7,6 @@ import { generateProvenanceGraph } from './generators/provenance.js';
import { generateCycloneDX } from './generators/cyclonedx.js'; import { generateCycloneDX } from './generators/cyclonedx.js';
import { generateSPDX } from './generators/spdx.js'; import { generateSPDX } from './generators/spdx.js';
import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js'; import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
import { generateProtobuf } from './generators/protobuf.js';
import { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js'; import { generateZ3, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
import { generateRust } from './generators/rust.js'; import { generateRust } from './generators/rust.js';
import fs from 'fs'; import fs from 'fs';
@ -16,7 +15,7 @@ import path from 'path';
interface CompileOptions { interface CompileOptions {
outputDir: string; outputDir: string;
bomFormat: 'cdx' | 'spdx' | 'both'; bomFormat: 'cdx' | 'spdx' | 'both';
target: 'typescript' | 'z3' | 'rust' | 'protobuf' | 'all'; target: 'typescript' | 'z3' | 'all';
verifyDepth: number; verifyDepth: number;
} }
@ -51,7 +50,7 @@ async function main() {
alias: 't', alias: 't',
describe: 'Compilation target', describe: 'Compilation target',
type: 'string', type: 'string',
choices: ['typescript', 'z3', 'rust', 'protobuf', 'all'], choices: ['typescript', 'z3', 'rust', 'all'],
default: 'typescript' as const, default: 'typescript' as const,
}) })
.option('verify-depth', { .option('verify-depth', {
@ -75,7 +74,7 @@ async function main() {
const options = { const options = {
outputDir: argv.outputDir as string, outputDir: argv.outputDir as string,
bomFormat: argv.bomFormat as 'cdx' | 'spdx' | 'both', bomFormat: argv.bomFormat as 'cdx' | 'spdx' | 'both',
target: argv.target as 'typescript' | 'z3' | 'rust' | 'protobuf' | 'all', target: argv.target as 'typescript' | 'z3' | 'rust' | 'all',
verifyDepth: argv.verifyDepth as number, verifyDepth: argv.verifyDepth as number,
}; };
@ -102,15 +101,6 @@ async function main() {
generateRust(ast, options.outputDir); generateRust(ast, options.outputDir);
} }
// Generate protobuf schema if target is protobuf or all
// This is the load-bearing backend for the "no glue code" claim:
// the emitted .proto is the canonical wire format. Run `buf generate`
// on the output to produce Go/TS/Rust/C/Python/Java bindings.
if (options.target === 'protobuf' || options.target === 'all') {
console.log('\nGenerating protobuf schema (.proto)...');
generateProtobuf(ast, options.outputDir);
}
// Always generate provenance (it's the core output) if not z3-only or rust-only // Always generate provenance (it's the core output) if not z3-only or rust-only
if (options.target !== 'z3' && options.target !== 'rust') { if (options.target !== 'z3' && options.target !== 'rust') {
console.log('\nGenerating provenance graph (PROV-O JSON-LD)...'); console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');

600
compiler/src/parser.ts
View file

@ -6,22 +6,6 @@ export interface SpeckNode {
type: 'speck'; type: 'speck';
name: string; name: string;
members: MemberNode[]; members: MemberNode[];
// Optional metadata from top-of-file directives (version:, author:, license:, proto_package:, go_package:).
// Undefined when not specified in the source.
version?: string;
author?: string;
license?: string;
// Protobuf-specific overrides. If unset, generator uses sensible defaults.
// proto_package: e.g. "federated_meetup.v1"
// go_package: e.g. "github.com/sscoble/federated-meetup/proto/federated_meetup/v1;federatedmeetupv1"
protoPackage?: string;
goPackage?: string;
// Cycle 61: optional event-name suffix. When set, the .proto generator
// appends this string to every `event` block's message name (e.g. an
// event CreateGroup with event_suffix: "Payload" emits
// `message CreateGroupPayload { ... }`). Matches the federated-meetup
// convention where every transition payload is named XxxPayload.
eventSuffix?: string;
} }
export interface ImportNode { export interface ImportNode {
@ -55,37 +39,10 @@ export interface VerifyNode {
depth?: number; depth?: number;
} }
export interface InterfaceField {
name: string;
type: TypeExpr;
}
export interface RpcMethod {
name: string;
requestType: string;
responseType: string;
// Streaming flags for gRPC/ConnectRPC
clientStreaming?: boolean;
serverStreaming?: boolean;
}
export interface ServiceNode {
type: 'service';
name: string;
rpcs: RpcMethod[];
}
export interface InterfaceNode { export interface InterfaceNode {
type: 'interface'; type: 'interface';
name: string; name: string;
// Discriminator: which form does this interface take?
// 'enum' → only methods[] populated with variant names (returnType: Void)
// 'record' → only fields[] populated with name: Type entries
// 'service' → methods[] populated with method signatures (name(params) -> Type)
// 'mixed' → ambiguous; generators should inspect both
kind: 'enum' | 'record' | 'service' | 'mixed';
methods: MethodSignature[]; methods: MethodSignature[];
fields: InterfaceField[];
} }
export interface MethodSignature { export interface MethodSignature {
@ -100,42 +57,6 @@ export interface EventNode {
fields: { name: string; type: TypeExpr }[]; fields: { name: string; type: TypeExpr }[];
} }
// oneof: discriminated-union variant for proto wire-format compatibility.
// Cycle 57 — emits `oneof payload { TypeName field_name = N; ... }` when
// compiled to .proto. Variants reference top-level event/interface types;
// field_name is the snake_case wire name (lowerCamelCase convention from
// TypeScript).
export interface OneofNode {
type: 'oneof';
name: string;
variants: OneofVariant[];
}
export interface OneofVariant {
fieldName: string; // wire name, e.g. "create_group"
typeName: string; // referenced type, e.g. "CreateGroup"
}
// Cycle 58: Transition envelope — a proto message that wraps a oneof payload
// along with metadata fields (prior_state, signatures, hlc, branch_id, etc).
// Distinct from `event` because:
// - payload field references a OneofNode (not a regular message type)
// - generator emits a `oneof payload { ... }` block inside the message body
// - the discriminator field uses a proto enum (TransitionType)
// This is the shape federated-meetup needs for its `Transition` message.
export interface TransitionNode {
type: 'transition';
name: string;
fields: TransitionField[];
payloadOneof?: string; // name of the OneofNode whose variants go inside the oneof payload block
typeDiscriminator?: string; // name of the enum used to discriminate variants
}
export interface TransitionField {
name: string;
type: TypeExpr;
}
export interface ProvenanceNode { export interface ProvenanceNode {
type: 'provenance'; type: 'provenance';
clauses: ProvenanceClause[]; clauses: ProvenanceClause[];
@ -190,15 +111,6 @@ export interface BOMNode {
export interface StateNode { export interface StateNode {
type: 'state'; type: 'state';
variables: StateVar[]; variables: StateVar[];
// Cycle 59: optional message-name override. When set, the .proto
// generator emits `message <messageName> { ... }` instead of
// `message <SpeckName>State { ... }`. This matches the consumer's
// expected binding name (e.g. StateSnapshot instead of
// FederatedMeetupState), so the Speckl-generated proto is a drop-in
// for the handwritten one. See:
// .hermes/skills/spec-compiler-dogfood/references/
// speckl-federated-meetup-protobuf-migration.md
messageName?: string;
} }
export interface StateVar { export interface StateVar {
@ -229,27 +141,24 @@ export type ActionStatement =
| { type: 'return'; expr: string } | { type: 'return'; expr: string }
| { type: 'ifblock'; raw: string }; | { type: 'ifblock'; raw: string };
export type MemberNode = export type MemberNode =
| ImportNode | ImportNode
| InputNode | InputNode
| OutputNode | OutputNode
| ConstraintNode | ConstraintNode
| VerifyNode | VerifyNode
| InterfaceNode | InterfaceNode
| EventNode | EventNode
| OneofNode | ProvenanceNode
| TransitionNode | ReviewNode
| ProvenanceNode | DerivesNode
| ReviewNode | SatisfiesNode
| DerivesNode | AuthorNode
| SatisfiesNode | SourceNode
| AuthorNode
| SourceNode
| BOMNode | BOMNode
| StateNode | StateNode
| InitNode | InitNode
| ActionNode | ActionNode;
| ServiceNode;
export interface TypeExpr { export interface TypeExpr {
type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident'; type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident';
@ -324,14 +233,6 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
const name = headerMatch[1]; const name = headerMatch[1];
const members: MemberNode[] = []; const members: MemberNode[] = [];
// Cycle 73: refactored from static-field hack to local-object pattern.
// Previously, proto_package / go_package / event_suffix were stored
// on (parseSpeck as any)._protoPackage etc — static function fields
// that leaked between parse calls. Now collected in a local metadata
// object and spread into the return value. No reset needed because
// the object is local to this invocation.
const metadata: { protoPackage?: string; goPackage?: string; eventSuffix?: string } = {};
let i = startIndex + 1; let i = startIndex + 1;
let braceCount = 1; let braceCount = 1;
@ -344,35 +245,13 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
continue; continue;
} }
// ── Top-of-file protobuf metadata directives ────────────────
// These attach to the SpeckNode and are NOT emitted as members.
// Format: `key: value` (string values may be quoted or bare).
// `author:`, `version:`, `license:` continue to be parsed as members
// (AuthorNode, etc.) for backward compatibility with the existing
// PROV-O / CycloneDX generators.
const metaMatch = line.match(/^(proto_package|go_package|event_suffix)\s*:\s*(.+)$/);
if (metaMatch) {
// Strip surrounding quotes if present
const value = metaMatch[2].trim().replace(/^['"]|['"]$/g, '');
if (metaMatch[1] === 'proto_package') {
metadata.protoPackage = value;
} else if (metaMatch[1] === 'go_package') {
metadata.goPackage = value;
} else if (metaMatch[1] === 'event_suffix') {
metadata.eventSuffix = value;
}
i++;
continue;
}
// Count braces on this line first // Count braces on this line first
const openCount = (rawLine.match(/{/g) || []).length; const openCount = (rawLine.match(/{/g) || []).length;
const closeCount = (rawLine.match(/}/g) || []).length; const closeCount = (rawLine.match(/}/g) || []).length;
// Check for block-opening members (those that open braces on the same line) // Check for block-opening members (those that open braces on the same line)
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ', const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
'state {', 'init {', 'verify ', 'constraint ', 'input:', 'output:', 'service ', 'oneof ', 'transition ', 'state {', 'init {', 'verify ', 'constraint '];
'state as '];
const isBlockStarter = blockStarters.some(s => line.startsWith(s)); const isBlockStarter = blockStarters.some(s => line.startsWith(s));
if (isBlockStarter && openCount > 0) { if (isBlockStarter && openCount > 0) {
@ -392,8 +271,8 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
} }
// Handle constraint/verify blocks that may span multiple lines without braces // Handle constraint/verify blocks that may span multiple lines without braces
// (e.g. constraint Name: forall r in [0..4]:, verify: always(implies(\n ...\n))) // (e.g. constraint Name: forall r in [0..4]:)
if (line.startsWith('constraint ') || line.startsWith('verify ') || line.startsWith('verify:')) { if (line.startsWith('constraint ') || line.startsWith('verify ')) {
const member = parseMultiLineConstraintVerify(lines, i); const member = parseMultiLineConstraintVerify(lines, i);
if (member) { if (member) {
members.push(member); members.push(member);
@ -406,8 +285,7 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
nextLine.startsWith('state') || nextLine.startsWith('init') || nextLine.startsWith('state') || nextLine.startsWith('init') ||
nextLine.startsWith('action ') || nextLine.startsWith('event ') || nextLine.startsWith('action ') || nextLine.startsWith('event ') ||
nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') || nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') ||
nextLine.startsWith('service ') || nextLine.startsWith('bom ') || nextLine.startsWith('bom ') || nextLine.startsWith('}') ||
nextLine.startsWith('}') ||
nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) { nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) {
break; break;
} }
@ -432,10 +310,7 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
i++; i++;
} }
return { type: 'speck', name, members, return { type: 'speck', name, members };
protoPackage: metadata.protoPackage,
goPackage: metadata.goPackage,
eventSuffix: metadata.eventSuffix };
} }
function findBlockEnd(lines: string[], startIndex: number, startBraceCount: number): number { function findBlockEnd(lines: string[], startIndex: number, startBraceCount: number): number {
@ -481,12 +356,6 @@ function parseMemberBlock(lines: string[], startIndex: number): MemberNode | nul
if (firstLine.startsWith('state {') || firstLine === 'state') { if (firstLine.startsWith('state {') || firstLine === 'state') {
return parseStateBlockMultiline(lines, startIndex, startBraceCount); return parseStateBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('state as ')) {
// Cycle 63: `state as <MessageName> { ... }` form must dispatch
// through the same state-block parser so the `as` override on the
// first line is captured.
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('init:')) { if (firstLine.startsWith('init:')) {
return parseInitBlockMultiline(lines, startIndex, startBraceCount); return parseInitBlockMultiline(lines, startIndex, startBraceCount);
} }
@ -502,15 +371,6 @@ function parseMemberBlock(lines: string[], startIndex: number): MemberNode | nul
if (firstLine.startsWith('interface ')) { if (firstLine.startsWith('interface ')) {
return parseInterfaceBlockMultiline(lines, startIndex, startBraceCount); return parseInterfaceBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('oneof ')) {
return parseOneofBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('transition ')) {
return parseTransitionBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('service ')) {
return parseServiceBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('provenance ')) { if (firstLine.startsWith('provenance ')) {
return { type: 'provenance', clauses: [] }; return { type: 'provenance', clauses: [] };
} }
@ -523,70 +383,10 @@ function parseMemberBlock(lines: string[], startIndex: number): MemberNode | nul
if (firstLine.startsWith('constraint ')) { if (firstLine.startsWith('constraint ')) {
return parseConstraintBlockMultiline(lines, startIndex, startBraceCount); return parseConstraintBlockMultiline(lines, startIndex, startBraceCount);
} }
if (firstLine.startsWith('input:') || firstLine.startsWith('output:')) {
return parseInputOutputBlock(lines, startIndex, startBraceCount);
}
return null; return null;
} }
/**
* Parse a multi-line `input: { ... }` or `output: { ... }` block.
*
* The first line opens with `input: {` or `output: {` and the matching `}`
* may be many lines later (with field declarations on intermediate lines).
* We collect all lines up to the matching `}` (brace-counted) and join the
* inner content into a single record string that `parseTypeExpr` already
* knows how to handle.
*/
function parseInputOutputBlock(
lines: string[],
startIndex: number,
startBraceCount: number,
): MemberNode | null {
const header = lines[startIndex].trim();
const isInput = header.startsWith('input:');
const kind: 'input' | 'output' = isInput ? 'input' : 'output';
// Collect inner content lines, brace-counting across the block.
// startBraceCount is the brace count on the header line (1 for `input: {`).
// We need to find the line where braceCount returns to 0 (i.e. the closing `}`).
const innerLines: string[] = [];
let braceCount = 0;
let i = startIndex;
// First pass: extract inner content from header line (everything after the first `{`).
const headerLine = lines[startIndex].trim();
const headerNoComment = headerLine.replace(/\/\/.*$/, '').trim();
const openIdx = headerNoComment.indexOf('{');
if (openIdx >= 0) {
const after = headerNoComment.substring(openIdx + 1).trim();
if (after) innerLines.push(after);
}
braceCount = 1; // we're inside one `{` from the header
i = startIndex + 1;
while (i < lines.length && braceCount > 0) {
const raw = lines[i];
const stripped = raw.trim();
// Strip line comments (//...) — they cannot be inside a type expression.
const noComment = stripped.replace(/\/\/.*$/, '').trim();
for (const ch of noComment) {
if (ch === '{') braceCount++;
else if (ch === '}') braceCount--;
}
if (braceCount > 0 && noComment) {
// Inside the block — keep content (skip the closing `}` line itself).
innerLines.push(noComment);
}
i++;
}
// Join inner content with newlines; `parseTypeExpr`'s record branch
// splits on commas and matches `name: type` pairs.
const recordExpr = '{ ' + innerLines.join(' ') + ' }';
const typeExpr = parseTypeExpr(recordExpr);
return { type: kind, typeExpr };
}
function parseMember(line: string): MemberNode | null { function parseMember(line: string): MemberNode | null {
// input: // input:
if (line.startsWith('input:')) { if (line.startsWith('input:')) {
@ -633,16 +433,6 @@ function parseMember(line: string): MemberNode | null {
if (line.startsWith('event ')) { if (line.startsWith('event ')) {
return parseEvent(line); return parseEvent(line);
} }
// oneof:
if (line.startsWith('oneof ')) {
return parseOneof(line);
}
// transition:
if (line.startsWith('transition ')) {
return parseTransition(line);
}
// provenance { // provenance {
if (line.startsWith('provenance ')) { if (line.startsWith('provenance ')) {
@ -945,17 +735,14 @@ function parseInterface(line: string): InterfaceNode {
if (!match) { if (!match) {
throw new Error(`Failed to parse interface: ${line}`); throw new Error(`Failed to parse interface: ${line}`);
} }
const name = match[1]; const name = match[1];
// Header-only; parseInterfaceBlockMultiline fills in methods/fields/kind // This is a simplified parser - in a real implementation, we'd need to handle multi-line interfaces
// by scanning the lines inside the { ... } block.
return { return {
type: 'interface', type: 'interface',
name, name,
kind: 'mixed',
methods: [], methods: [],
fields: [],
}; };
} }
@ -965,9 +752,9 @@ function parseEvent(line: string): EventNode {
if (!match) { if (!match) {
throw new Error(`Failed to parse event: ${line}`); throw new Error(`Failed to parse event: ${line}`);
} }
const name = match[1]; const name = match[1];
return { return {
type: 'event', type: 'event',
name, name,
@ -975,34 +762,6 @@ function parseEvent(line: string): EventNode {
}; };
} }
// Cycle 57: parse `oneof Name {` (header only; parseOneofBlockMultiline fills variants).
function parseOneof(line: string): OneofNode {
// oneof Name {
const match = line.match(/^oneof\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse oneof: ${line}`);
}
return {
type: 'oneof',
name: match[1],
variants: [],
};
}
// Cycle 58: parse `transition Name {` (header only; parseTransitionBlockMultiline fills fields + payload-oneof).
function parseTransition(line: string): TransitionNode {
// transition Name {
const match = line.match(/^transition\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse transition: ${line}`);
}
return {
type: 'transition',
name: match[1],
fields: [],
};
}
function parseProvenanceBlock(lines: string[], line: string): ProvenanceNode { function parseProvenanceBlock(lines: string[], line: string): ProvenanceNode {
// This is a simplified parser - in a real implementation, we'd parse the full block // This is a simplified parser - in a real implementation, we'd parse the full block
return { return {
@ -1094,13 +853,6 @@ function parseSource(line: string): SourceNode {
} }
function parseStateBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): StateNode { function parseStateBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): StateNode {
// Cycle 59: support `state as <MessageName> { ... }` to override the
// generated .proto message name. Default (no `as`) keeps the existing
// `message <SpeckName>State { ... }` convention.
const headerLine = lines[startIndex].trim();
const asMatch = headerLine.match(/^state\s+as\s+(\w+)\s*{/);
const messageName = asMatch ? asMatch[1] : undefined;
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount); const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*')); const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
// State blocks separate fields with commas or newlines/semicolons. // State blocks separate fields with commas or newlines/semicolons.
@ -1119,9 +871,7 @@ function parseStateBlockMultiline(lines: string[], startIndex: number, startBrac
} }
return acc + ' ' + line; return acc + ' ' + line;
}, ''); }, '');
const result = parseStateBlock(inner); return parseStateBlock(inner);
if (messageName !== undefined) result.messageName = messageName;
return result;
} }
function parseInitBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): InitNode { function parseInitBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): InitNode {
@ -1210,7 +960,7 @@ function parseActionBlockMultiline(lines: string[], startIndex: number, startBra
if (nextLine.startsWith('precondition:') || nextLine.startsWith('postcondition:') || if (nextLine.startsWith('precondition:') || nextLine.startsWith('postcondition:') ||
nextLine.startsWith('require ') || nextLine.startsWith('return ') || nextLine.startsWith('require ') || nextLine.startsWith('return ') ||
nextLine.startsWith('emit ') || nextLine.startsWith('let ') || nextLine.startsWith('emit ') || nextLine.startsWith('let ') ||
nextLine.startsWith('if ') || nextLine.includes(':=')) { nextLine.includes(':=')) {
break; break;
} }
i++; i++;
@ -1299,24 +1049,7 @@ function parseEventBlockMultiline(lines: string[], startIndex: number, startBrac
const fields: { name: string; type: TypeExpr }[] = []; const fields: { name: string; type: TypeExpr }[] = [];
for (const line of innerLines) { for (const line of innerLines) {
// Cycle 62: strip inline `//` line-comments from the type expression const match = line.match(/^(\w+)\s*:\s*(.+?),?$/);
// before parsing. Without this, an event field like
// mesh_ip: Bytes // 4 bytes (IPv4 overlay)
// produces a TypeExpr whose name includes the comment text, which
// the .proto generator emits verbatim:
// bytes // 4 bytes (IPv4 overlay) mesh_ip = 2;
// (broken syntax — comment is in the type position).
const noComment = line.replace(/\/\/.*$/, '').trim();
// Cycle 65: strip default-value suffix `= <expr>` from the type
// expression. The federated-meetup speckdl has fields like
// initial_mesh_peers: List<InitialMeshPeer> = []
// where the default is meaningful in Speckl semantics (a state-
// machine init) but the .proto wire format doesn't carry a
// default — it's a generator concern. Without this, the type
// expression was emitted as `List<InitialMeshPeer> = []` and
// protoc rejects the resulting syntax.
const noDefault = noComment.replace(/\s*=\s*[^,]+$/, '').trim();
const match = noDefault.match(/^(\w+)\s*:\s*(.+?),?$/);
if (match) { if (match) {
fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) }); fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) });
} }
@ -1332,20 +1065,12 @@ function parseInterfaceBlockMultiline(lines: string[], startIndex: number, start
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*')); const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const methods: MethodSignature[] = []; const methods: MethodSignature[] = [];
const fields: InterfaceField[] = [];
for (const line of innerLines) { for (const line of innerLines) {
// Cycle 62: strip inline `//` line-comments from each line before // name-only: enum-style values (e.g., "Idle", "Idle, Parsing" comma-separated)
// token-splitting. Without this, a field like // Split on comma and take each trimmed token
// mesh_ip: Bytes // 4 bytes (IPv4 overlay) const tokens = line.split(',').map(s => s.trim()).filter(Boolean);
// has its comment text bleed into the parsed type expression,
// which the .proto generator emits verbatim — broken syntax.
const noComment = line.replace(/\/\/.*$/, '').trim();
if (!noComment) continue;
// Split on comma so multi-variant lines like "Idle, Parsing, Done" all parse
const tokens = noComment.split(',').map(s => s.trim()).filter(Boolean);
for (const token of tokens) { for (const token of tokens) {
// Check 1: method signature form: name(params) -> returnType // Check if it’s a name(params) -> returnType method signature
const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/); const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/);
if (methodMatch) { if (methodMatch) {
const name = methodMatch[1]; const name = methodMatch[1];
@ -1362,148 +1087,13 @@ function parseInterfaceBlockMultiline(lines: string[], startIndex: number, start
} }
} }
methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) }); methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) });
continue; } else if (/^\w+$/.test(token)) {
} // Name-only (enum-style) — treat as a method with no params and void return
// Check 2: field declaration form: field_name: TypeName
// Lowercase-starting identifier followed by ':' — record-style interface
const fieldMatch = token.match(/^(\w+)\s*:\s*(.+)$/);
if (fieldMatch && /^[a-z_]/.test(fieldMatch[1])) {
fields.push({ name: fieldMatch[1], type: parseTypeExpr(fieldMatch[2].trim()) });
continue;
}
// Check 3: bare identifier (enum variant) — name only, no params
if (/^\w+$/.test(token)) {
methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') }); methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') });
} }
} }
} }
return { ...header, methods };
// Determine the kind based on what we collected
let kind: 'enum' | 'record' | 'service' | 'mixed' = 'mixed';
if (fields.length > 0 && methods.length === 0) {
kind = 'record';
} else if (methods.length > 0 && fields.length === 0) {
// Distinguish enum (all methods have empty params and Void return) from service
const allEnumLike = methods.every(m => m.params.length === 0 && m.returnType.name === 'Void');
kind = allEnumLike ? 'enum' : 'service';
}
return { ...header, kind, methods, fields };
}
// Cycle 57: parse a `oneof Name { ... }` block. Each non-empty, non-comment
// inner line is `field_name: TypeName`. The wire field_name follows
// lowerCamelCase convention (TypeScript/Connect) and is emitted to .proto
// as snake_case by the generator.
function parseOneofBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): OneofNode {
const firstLine = lines[startIndex].trim();
const header = parseOneof(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const variants: OneofVariant[] = [];
for (const line of innerLines) {
// Strip trailing comma or semicolon (proto-style "create_group: CreateGroup," is valid).
const trimmed = line.replace(/[,;]\s*$/, '');
const m = trimmed.match(/^(\w+)\s*:\s*(\w+)\s*$/);
if (m) {
variants.push({ fieldName: m[1], typeName: m[2] });
}
}
return { ...header, variants };
}
// Cycle 58: parse a `transition Name { ... }` block. Each non-empty,
// non-comment inner line is `field_name: TypeName`. Two field names
// have special meaning:
// - `payload: <OneofName>` — references a sibling `oneof` block;
// the proto generator will emit the variants inline as
// `oneof payload { ... }` inside the message body
// - `type: <EnumName>` — the discriminator enum for the variants
// Other fields are emitted as ordinary proto message fields.
function parseTransitionBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): TransitionNode {
const firstLine = lines[startIndex].trim();
const header = parseTransition(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const fields: TransitionField[] = [];
let payloadOneof: string | undefined;
let typeDiscriminator: string | undefined;
for (const line of innerLines) {
const trimmed = line.replace(/[,;]\s*$/, '');
const m = trimmed.match(/^(\w+)\s*:\s*(.+)$/);
if (!m) continue;
const fieldName = m[1];
const typeStr = m[2].trim();
if (fieldName === 'payload') {
// The type is the name of a sibling oneof block.
payloadOneof = typeStr;
// Don't add a regular field for payload — it becomes the oneof.
continue;
}
if (fieldName === 'type') {
// The type is the name of a discriminator enum.
typeDiscriminator = typeStr;
// Don't add a regular field for type — it's a special discriminator.
continue;
}
fields.push({ name: fieldName, type: parseTypeExpr(typeStr) });
}
const result: TransitionNode = { ...header, fields };
if (payloadOneof !== undefined) result.payloadOneof = payloadOneof;
if (typeDiscriminator !== undefined) result.typeDiscriminator = typeDiscriminator;
return result;
}
function parseServiceBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): ServiceNode {
// service Name {
const firstLine = lines[startIndex].trim();
const match = firstLine.match(/^service\s+(\w+)\s*{?/);
const name = match ? match[1] : 'UnnamedService';
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const rpcs: RpcMethod[] = [];
for (const line of innerLines) {
// rpc MethodName(RequestType) returns (ResponseType);
// Also support streaming: rpc M(stream R) returns (S); or rpc M(R) returns (stream S);
const rpcMatch = line.match(/^rpc\s+(\w+)\s*\(\s*(stream\s+)?(\w+)\s*\)\s*returns\s*\(\s*(stream\s+)?(\w+)\s*\)\s*;?$/);
if (rpcMatch) {
const methodName = rpcMatch[1];
const clientStream = !!rpcMatch[2];
const requestType = rpcMatch[3];
const serverStream = !!rpcMatch[4];
const responseType = rpcMatch[5];
rpcs.push({
name: methodName,
requestType,
responseType,
clientStreaming: clientStream,
serverStreaming: serverStream,
});
} else {
// Cycle 73: error on unrecognized lines inside service blocks.
// Previously, a typo like `rc_purchase_ticket(...)` (missing the `p`
// in `rpc`) was silently swallowed — the line didn't match the
// rpc regex, so it was skipped without error. Silent data loss in
// a spec compiler is unacceptable; the whole point is that the
// spec is the source of truth.
throw new Error(
`Parse error in service block: unrecognized line "${line}". ` +
`Expected: rpc MethodName(RequestType) returns (ResponseType);`
);
}
}
return { type: 'service', name, rpcs };
} }
// --- Multi-line constraint/verify parsing (no braces needed) --- // --- Multi-line constraint/verify parsing (no braces needed) ---
@ -1520,130 +1110,18 @@ function parseServiceBlockMultiline(lines: string[], startIndex: number, startBr
*/ */
function parseMultiLineConstraintVerify(lines: string[], startIndex: number): MemberNode | null { function parseMultiLineConstraintVerify(lines: string[], startIndex: number): MemberNode | null {
const line = lines[startIndex].trim(); const line = lines[startIndex].trim();
if (line.startsWith('verify ')) { if (line.startsWith('verify ')) {
return parseVerifyAnyForm(lines, startIndex); return parseVerifyAnyForm(lines, startIndex);
} }
// Multi-line `verify:` form: verify: always(implies(\n ...\n))
// The body opens parens that span multiple lines; collect continuation
// lines until parens balance to zero, then return the joined string as
// the temporalExpr. speckl#54.
if (line.startsWith('verify:')) {
return parseVerifyColonBlock(lines, startIndex);
}
if (line.startsWith('constraint ')) { if (line.startsWith('constraint ')) {
return parseConstraintAnyForm(lines, startIndex); return parseConstraintAnyForm(lines, startIndex);
} }
return null; return null;
} }
/**
* Parse the `verify: <expr>` form (speckl#54) where the body can span
* multiple lines:
*
* verify: always(implies(
* cond1,
* cond2
* ))
*
* The whole expression (the part after `verify:`) is collected by
* appending subsequent non-empty, non-keyword-starting lines until
* parens/brackets/braces balance to zero. The joined string is stored
* in `temporalExpr` so the downstream LTL translator (typescript-state-machine
* verifyN()) sees a well-formed formula.
*
* The `name` is derived from the LTL operator's argument when it matches
* `always(Name)` / `eventually(Name)`. When the body is a richer expression
* (e.g. `always(implies(...))`) we fall back to `unnamed` — the generator
* still emits a working verifyN() that uses the full expression.
*/
function parseVerifyColonBlock(lines: string[], startIndex: number): VerifyNode | null {
const firstLine = lines[startIndex].trim();
// Strip the `verify:` prefix.
const head = firstLine.substring(firstLine.indexOf(':') + 1).trim();
if (!head) return null;
// If the head is already balanced on its own (single-line verify: expr),
// just return it directly — no continuation needed.
if (isExpressionComplete(head)) {
const nameMatch = head.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
return {
type: 'verify',
name: nameMatch ? nameMatch[1] : 'unnamed',
temporalExpr: head,
};
}
// Multi-line: collect continuation lines until parens balance. The same
// break-condition list used in the parseSpeck skip-loop applies (don't
// swallow the next member's keyword). We additionally stop at any
// standalone `}` so a verify inside a brace-block still terminates.
const parts: string[] = [head];
let parens = 0, brackets = 0, braces = 0;
for (const ch of head) {
if (ch === '(') parens++;
else if (ch === ')') parens--;
else if (ch === '[') brackets++;
else if (ch === ']') brackets--;
else if (ch === '{') braces++;
else if (ch === '}') braces--;
}
let lastConsumed = startIndex;
for (let j = startIndex + 1; j < lines.length; j++) {
const raw = lines[j];
const nl = raw.trim();
if (!nl) {
// Empty line still updates counters (none) and advances lastConsumed
lastConsumed = j;
continue;
}
if (nl.startsWith('//') || nl.startsWith('/*')) {
// Skip standalone comments but treat them as part of the block
// (the LTL translator doesn't care about comments in temporalExpr).
lastConsumed = j;
continue;
}
// Stop at a new top-level member keyword — that's the next member.
if (
nl.startsWith('constraint ') || nl.startsWith('verify ') ||
nl.startsWith('constraint:') || nl.startsWith('verify:') ||
nl.startsWith('state') || nl.startsWith('init') ||
nl.startsWith('action ') || nl.startsWith('event ') ||
nl.startsWith('interface ') || nl.startsWith('provenance ') ||
nl.startsWith('bom ') || nl === '}' ||
nl.startsWith('next:') || nl.startsWith('invariant ')
) {
break;
}
// Update depth counters.
for (const ch of raw) {
if (ch === '(') parens++;
else if (ch === ')') parens--;
else if (ch === '[') brackets++;
else if (ch === ']') brackets--;
else if (ch === '{') braces++;
else if (ch === '}') braces--;
}
parts.push(nl);
lastConsumed = j;
if (parens === 0 && brackets === 0 && braces === 0) {
break;
}
}
const joined = parts.join(' ').replace(/\s+/g, ' ').trim();
const nameMatch = joined.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
return {
type: 'verify',
name: nameMatch ? nameMatch[1] : 'unnamed',
temporalExpr: joined,
};
}
function parseConstraintAnyForm(lines: string[], startIndex: number): ConstraintNode | null { function parseConstraintAnyForm(lines: string[], startIndex: number): ConstraintNode | null {
const line = lines[startIndex].trim(); const line = lines[startIndex].trim();

16
compiler/test-ast.mjs
View file

@ -1,16 +0,0 @@
import { parseSpeckFile } from './dist/parser.js';
import fs from 'fs';
const ast = parseSpeckFile('/home/sscoble/speckl/examples/Raft.speck');
for (const speck of ast.specks) {
for (const m of speck.members) {
if (m.type === 'action') {
for (const s of (m.statements || [])) {
if (s.type === 'ifblock') {
console.log('--- ifblock in', m.name, '---');
console.log('raw:', s.raw.substring(0, 200));
}
}
}
}
}

2
compiler/test-output/RetryHandler.prov.jsonld
View file

@ -12,7 +12,7 @@
"@type": "prov:Generation", "@type": "prov:Generation",
"prov:activity": { "prov:activity": {
"@type": "prov:Activity", "@type": "prov:Activity",
"prov:startTime": "2026-07-19T08:31:16.455Z" "prov:startTime": "2026-05-11T17:13:39.546Z"
} }
}, },
"rdfs:label": "RetryHandler", "rdfs:label": "RetryHandler",

6
compiler/test-output/RetryHandler.specbom.cdx.json
View file

@ -38,7 +38,7 @@
"name": "Scott Scoble", "name": "Scott Scoble",
"email": "scott@scoble.me" "email": "scott@scoble.me"
}, },
"timestamp": "2026-07-19T08:31:16.458Z" "timestamp": "2026-05-11T17:13:39.549Z"
}, },
{ {
"subject": "speck:RetryHandler", "subject": "speck:RetryHandler",
@ -53,7 +53,7 @@
"name": "Speckl Compiler", "name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me" "email": "compiler@speckl.scoble.me"
}, },
"timestamp": "2026-07-19T08:31:16.458Z" "timestamp": "2026-05-11T17:13:39.549Z"
}, },
{ {
"subject": "speck:RetryHandler", "subject": "speck:RetryHandler",
@ -68,7 +68,7 @@
"name": "Speckl Compiler", "name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me" "email": "compiler@speckl.scoble.me"
}, },
"timestamp": "2026-07-19T08:31:16.458Z" "timestamp": "2026-05-11T17:13:39.549Z"
} }
] ]
} }

4
compiler/test-output/RetryHandler.specbom.spdx.json
View file

@ -13,7 +13,7 @@
"spdxVersion": "3.0.1", "spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0", "dataLicense": "CC0-1.0",
"creationInfo": { "creationInfo": {
"created": "2026-07-19T08:31:16.459Z", "created": "2026-05-11T17:13:39.551Z",
"createdBy": [ "createdBy": [
"Organization: Speckl", "Organization: Speckl",
"tool: speckl-compile-0.2.0" "tool: speckl-compile-0.2.0"
@ -27,7 +27,7 @@
"@type": "spdx:Tool", "@type": "spdx:Tool",
"name": "speckl-compile" "name": "speckl-compile"
}, },
"timestamp": "2026-07-19T08:31:16.459Z", "timestamp": "2026-05-11T17:13:39.551Z",
"comment": "Review type: manual" "comment": "Review type: manual"
} }
] ]

22
compiler/test-parser.mjs
View file

@ -1,22 +0,0 @@
import { parseActionStatements } from './dist/expr/stmt-parser.js';
const tests = [
['serverState[voter].currentTerm := req.term'],
['let newTerm := 5', 'newTerm := 6'],
['require foo == bar'],
['return 5'],
['emit VoteGranted { voter: voter, candidate: 1, term: 2 }'],
['if foo { x := 1 } else { y := 2 }'],
['x := 1', 'y := 2', 'return 5'],
];
for (const lines of tests) {
console.log('---');
console.log('input:', lines);
try {
const out = parseActionStatements(lines);
console.log('output:', JSON.stringify(out, null, 2).substring(0, 700));
} catch (e) {
console.log('error:', e.message);
}
}

29
examples/ConditionalToggle.speck
View file

@ -1,29 +0,0 @@
speck ConditionalToggle {
state {
isOn: Bool
count: Nat
}
init {
isOn == false
count == 0
}
invariant SwitchConsistent {
isOn in {true, false}
}
action Toggle {
require true
if (isOn) {
isOn := false
} else {
isOn := true
}
count := count + 1
return isOn
}
next: Toggle
}

1
node_modules/.vite/vitest/da39a3ee5e6b4b0d3255bfef95601890afd80709/results.json generated vendored
View file

@ -1 +0,0 @@
{"version":"4.1.9","results":[[":compiler/dist/__tests__/compiler.test.js",{"duration":21.732912999999996,"failed":false}],[":compiler/__tests__/parser.test.ts",{"duration":56.655685000000005,"failed":false}],[":compiler/src/__tests__/compiler.test.ts",{"duration":3388.7825,"failed":false}]]}

21
out_fresh/OAuth2AuthorizationCode.prov.jsonld
View file

@ -1,21 +0,0 @@
{
"@context": {
"prov": "http://www.w3.org/ns/prov#",
"speckl": "https://speckl.scoble.me/ns/v0.2#",
"rdfs": "http://www.w3.org/2000/01/rdf-schema#"
},
"@graph": [
{
"@type": "prov:Entity",
"@id": "speck:OAuth2AuthorizationCode",
"prov:qualifiedGeneration": {
"@type": "prov:Generation",
"prov:activity": {
"@type": "prov:Activity",
"prov:startTime": "2026-06-08T14:27:09.658Z"
}
},
"rdfs:label": "OAuth2AuthorizationCode"
}
]
}

15
out_fresh/OAuth2AuthorizationCode.specbom.cdx.json
View file

@ -1,15 +0,0 @@
{
"bomFormat": "CycloneDX",
"specVersion": "1.6",
"components": [],
"metadata": {
"tools": [],
"component": {
"type": "application",
"name": "OAuth2AuthorizationCode",
"version": "0.2.0",
"properties": []
}
},
"annotations": []
}

26
out_fresh/OAuth2AuthorizationCode.specbom.spdx.json
View file

@ -1,26 +0,0 @@
{
"@context": [
"https://spdx.github.io/spdx-v3/spdx-context.jsonld",
{
"speckl": "https://speckl.scoble.me/ns/v0.2#"
}
],
"@type": "spdx:Document",
"spdx": {
"@id": "spdx:OAuth2AuthorizationCode",
"@type": "spdx:Snippet",
"name": "OAuth2AuthorizationCode",
"spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0",
"creationInfo": {
"created": "2026-06-08T14:27:09.674Z",
"createdBy": [
"Organization: Speckl",
"tool: speckl-compile-0.2.0"
]
}
},
"builtBy": [],
"relationships": [],
"elements": []
}

192
out_fresh/OAuth2AuthorizationCode.ts
View file

@ -1,192 +0,0 @@
// Auto-generated by speckl-compile from OAuth2AuthorizationCode
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
export const OAuth2AuthorizationCodeOAuth2AuthorizationCodeState = {
Open: 'open',
Closed: 'closed',
} as const;
export type OAuth2AuthorizationCodeOAuth2AuthorizationCodeState = typeof OAuth2AuthorizationCodeOAuth2AuthorizationCodeState[keyof typeof OAuth2AuthorizationCodeOAuth2AuthorizationCodeState];
// Simple hash utility for SpeckDL hash() function
// In production, replace with a real crypto hash
function simpleHash(s: string, method?: string): string {
let h = 0;
for (let i = 0; i < s.length; i++) {
h = ((h << 5) - h + s.charCodeAt(i)) | 0;
}
return 'h_' + Math.abs(h).toString(16);
}
// Runtime type placeholders (opaque record types)
type AccessToken = any;
type AuthorizationCode = any;
type Bool }) = any;
type ClientId = any;
type ClientSecret = any;
type CodeChallenge = any;
type CodeVerifier = any;
type Map(AccessToken, { client_id: ClientId = any;
type Map(AuthorizationCode, { client_id: ClientId = any;
type Map(RefreshToken, { client_id: ClientId = any;
type Nat }) = any;
type RedirectUri = any;
type RefreshRequest = any;
type RefreshToken }) = any;
type Scope = any;
type SessionId = any;
type State = any;
type TokenRequest = any;
type UserId = any;
export class OAuth2AuthorizationCodeMachine {
clients!: Map<ClientId, { redirect_uris: Set<RedirectUri>; client_secret: ClientSecret }>;
authorizationCodes!: Map(AuthorizationCode, { client_id: ClientId;
redirect_uri!: RedirectUri;
state!: State;
code_challenge!: CodeChallenge;
code_challenge_method!: string;
scope!: Scope;
user_id!: UserId;
session_id!: SessionId;
created_at!: number;
used!: Bool });
accessTokens!: Map(AccessToken, { client_id: ClientId;
user_id!: UserId;
scope!: Scope;
expires_at!: number;
session_id!: SessionId;
refresh_token!: RefreshToken });
refreshTokens!: Map(RefreshToken, { client_id: ClientId;
user_id!: UserId;
scope!: Scope;
access_token!: AccessToken;
created_at!: Nat });
sessions!: Map<SessionId, { user_id: UserId }>;
stateNonces!: Map<State, { client_id: ClientId; redirect_uri: RedirectUri }>;
pkceChallenges!: Map<CodeChallenge, { code_verifier_hash: string; method: string }>;
currentTime!: number;
decisionLog: any[] = [];
constructor() {
// No init block defined
}
Authorize(client: ClientId, redirectUri: RedirectUri, scope: Scope, userId: UserId, sessionId: SessionId) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
const client_id: any = {} as any; // FIXME: parser dropped let/forall
const code_verifier_hash: any = {} as any; // FIXME: parser dropped let/forall
const __STR_LIT_0__: any = {} as any; // FIXME: parser dropped let/forall
const method: any = {} as any; // FIXME: parser dropped let/forall
const __STR_LIT_1__: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
if (!(this.clients.get(client)!.redirect_uris.has(redirectUri))) throw new Error('Guard failed: this.clients.get(client)!.redirect_uris.has(redirectUri)');
if (!(this.sessions.has(sessionId))) throw new Error('Guard failed: this.sessions.has(sessionId)');
if (!(this.sessions.get(sessionId)!.user_id === userId)) throw new Error('Guard failed: this.sessions.get(sessionId)!.user_id === userId');
const state = "state_" + simpleHash(client + redirectUri + this.currentTime);
const codeVerifier = "verifier_" + simpleHash(client + userId + this.currentTime);
const codeChallenge = simpleHash(codeVerifier, "S256");
this.stateNonces.set(state, { client_id: client, redirect_uri: redirectUri });
this.pkceChallenges.set(codeChallenge, { code_verifier_hash: simpleHash(codeVerifier, __STR_LIT_0__), method: __STR_LIT_1__ });
const authCode = "code_" + simpleHash(client + userId + this.currentTime);
this.authorizationCodes.set(authCode, { client_id: client, redirect_uri: redirectUri, state: state, code_challenge: codeChallenge, code_challenge_method: __STR_LIT_0__, scope: scope, user_id: userId, session_id: sessionId, created_at: this.currentTime, used: false });
}
ApproveAuthorization(code: AuthorizationCode, userId: UserId) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
const c = this.authorizationCodes.get(code)!;
if (!(c.user_id === userId)) throw new Error('Guard failed: c.user_id === userId');
if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
}
ExchangeCode(req: TokenRequest) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
const client_id: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.clients.has(req.client_id))) throw new Error('Guard failed: this.clients.has(req.client_id)');
if (!(this.authorizationCodes.has(req.code))) throw new Error('Guard failed: this.authorizationCodes.has(req.code)');
const c = this.authorizationCodes.get(req.code)!;
if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
if (!(c.client_id === req.client_id)) throw new Error('Guard failed: c.client_id === req.client_id');
if (!(c.redirect_uri === req.redirect_uri)) throw new Error('Guard failed: c.redirect_uri === req.redirect_uri');
const expectedChallenge = simpleHash(req.code_verifier, c.code_challenge_method);
if (!(expectedChallenge === c.code_challenge)) throw new Error('Guard failed: expectedChallenge === c.code_challenge');
this.pkceChallenges.delete(c.code_challenge);
this.stateNonces.delete(c.state);
const accessToken = "access_" + simpleHash(req.client_id + c.user_id + this.currentTime);
const refreshToken = "refresh_" + simpleHash(req.client_id + c.user_id + this.currentTime);
const expiresAt = this.currentTime + 3600;
this.accessTokens.set(accessToken, { client_id: req.client_id, user_id: c.user_id, scope: c.scope, expires_at: expiresAt, session_id: c.session_id, refresh_token: refreshToken });
this.refreshTokens.set(refreshToken, { client_id: req.client_id, user_id: c.user_id, scope: c.scope, access_token: accessToken, created_at: this.currentTime });
}
RefreshToken(req: RefreshRequest) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
const client_id: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.clients.has(req.client_id))) throw new Error('Guard failed: this.clients.has(req.client_id)');
if (!(this.refreshTokens.has(req.refresh_token))) throw new Error('Guard failed: this.refreshTokens.has(req.refresh_token)');
const r = this.refreshTokens.get(req.refresh_token)!;
if (!(r.client_id === req.client_id)) throw new Error('Guard failed: r.client_id === req.client_id');
this.accessTokens.delete(r.access_token);
const newAccessToken = "access_" + simpleHash(req.client_id + r.user_id + this.currentTime);
const newRefreshToken = "refresh_" + simpleHash(req.client_id + r.user_id + this.currentTime);
const expiresAt = this.currentTime + 3600;
this.accessTokens.set(newAccessToken, { client_id: req.client_id, user_id: r.user_id, scope: req.scope.or(r.scope), expires_at: expiresAt, session_id: r.access_token.session_id, refresh_token: newRefreshToken });
this.refreshTokens.set(newRefreshToken, { client_id: req.client_id, user_id: r.user_id, scope: req.scope.or(r.scope), access_token: newAccessToken, created_at: this.currentTime });
this.refreshTokens.delete(req.refresh_token);
}
RevokeToken(client: ClientId, token: string, tokenType: string) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
const t: any = {} as any; // FIXME: parser dropped let/forall
const r: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.clients.has(client))) throw new Error('Guard failed: this.clients.has(client)');
if (tokenType === "access") {
if (!(this.accessTokens.has(token))) throw new Error('Guard failed: this.accessTokens.has(token)');
this.t = this.accessTokens.get(token)!;
if (!(t.client_id === client)) throw new Error('Guard failed: t.client_id === client');
this.s[token] = null;
this.s[t.refresh_token] = null;
} else {
if (tokenType === "refresh") {
if (!(this.refreshTokens.has(token))) throw new Error('Guard failed: this.refreshTokens.has(token)');
this.r = this.refreshTokens.get(token)!;
if (!(r.client_id === client)) throw new Error('Guard failed: r.client_id === client');
this.s[token] = null;
this.s[r.access_token] = null;
}
}
}
VerifyPKCE(code: AuthorizationCode, verifier: CodeVerifier) {
const xxx: any = {} as any; // FIXME: parser dropped let/forall
if (!(this.authorizationCodes.has(code))) throw new Error('Guard failed: this.authorizationCodes.has(code)');
const c = this.authorizationCodes.get(code)!;
if (!(c.used === false)) throw new Error('Guard failed: c.used === false');
const expectedChallenge = simpleHash(verifier, c.code_challenge_method);
if (!(expectedChallenge === c.code_challenge)) throw new Error('Guard failed: expectedChallenge === c.code_challenge');
}
// V1: Always(NoTokenLeakage)
// Z3 call-out: Bounded Model Checking (BMC) with depth = decisionLog.length+1.
// Mirrors the SMT-LIB BMC emitted by compiler/src/generators/z3.ts (emitBMC).
// The inner expression is SpeckDL; we translate it to a TS boolean
// check that reads the current class state via this.<stateVar>.
async verify1(): Promise<boolean> {
// Temporal: Always(NoTokenLeakage)
// LTL: always(p). Bounded check — p must hold at every step in the
// bounded trace (decision log + current state). The first step
// where p is false violates the always-quantified property.
if (!(NoTokenLeakage)) return false;
for (const _evt of this.decisionLog) {
// Each emit() entry is a step boundary; p is re-evaluated
// against the live state (BMC "safety-at-horizon" view).
if (!(NoTokenLeakage)) return false;
}
return true;
}
}

61
test-output/RetryHandler.prov.jsonld
View file

@ -1,61 +0,0 @@
{
"@context": {
"prov": "http://www.w3.org/ns/prov#",
"speckl": "https://speckl.scoble.me/ns/v0.2#",
"rdfs": "http://www.w3.org/2000/01/rdf-schema#"
},
"@graph": [
{
"@type": "prov:Entity",
"@id": "speck:RetryHandler",
"prov:qualifiedGeneration": {
"@type": "prov:Generation",
"prov:activity": {
"@type": "prov:Activity",
"prov:startTime": "2026-06-30T02:09:28.187Z"
}
},
"rdfs:label": "RetryHandler",
"prov:wasDerivedFrom": {
"@id": "speck:FaultHandler"
},
"rdfs:comment": "specialization for retry logic",
"speckl:satisfies": {
"@id": "requirement:RESILIENCE-REQ-01"
},
"prov:wasAttributedTo": {
"@id": "agent:Scott Scoble"
},
"prov:wasInformedBy": {
"@id": "source:architecture_review:AR-2024-0215"
}
},
{
"@type": "prov:Entity",
"@id": "speck:FaultHandler"
},
{
"@type": "prov:Entity",
"@id": "requirement:RESILIENCE-REQ-01",
"rdfs:label": "RESILIENCE-REQ-01",
"speckl:clause": "3.1.2"
},
{
"@type": "prov:Entity",
"@id": "requirement:RESILIENCE-REQ-02",
"rdfs:label": "RESILIENCE-REQ-02"
},
{
"@type": "prov:Agent",
"@id": "agent:Scott Scoble",
"rdfs:label": "Scott Scoble",
"foaf:email": "scott@scoble.me"
},
{
"@type": "prov:Activity",
"@id": "source:architecture_review:AR-2024-0215",
"prov:type": "architecture_review",
"rdfs:label": "architecture_review - AR-2024-0215"
}
]
}

74
test-output/RetryHandler.specbom.cdx.json
View file

@ -1,74 +0,0 @@
{
"bomFormat": "CycloneDX",
"specVersion": "1.6",
"components": [],
"metadata": {
"tools": [],
"component": {
"type": "application",
"name": "RetryHandler",
"version": "0.2.0",
"properties": [
{
"name": "speckl:derivesFrom",
"value": "FaultHandler"
},
{
"name": "speckl:satisfies",
"value": "RESILIENCE-REQ-01 clause 3.1.2"
},
{
"name": "speckl:satisfies",
"value": "RESILIENCE-REQ-02"
}
]
}
},
"annotations": [
{
"subject": "speck:RetryHandler",
"annotations": [
{
"type": "tag",
"value": "provenanceType",
"text": "author"
}
],
"author": {
"name": "Scott Scoble",
"email": "scott@scoble.me"
},
"timestamp": "2026-06-30T02:09:28.192Z"
},
{
"subject": "speck:RetryHandler",
"annotations": [
{
"type": "tag",
"value": "provenanceType",
"text": "source"
}
],
"author": {
"name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me"
},
"timestamp": "2026-06-30T02:09:28.192Z"
},
{
"subject": "speck:RetryHandler",
"annotations": [
{
"type": "tag",
"value": "reviewType",
"text": "manual"
}
],
"author": {
"name": "Speckl Compiler",
"email": "compiler@speckl.scoble.me"
},
"timestamp": "2026-06-30T02:09:28.192Z"
}
]
}

113
test-output/RetryHandler.specbom.spdx.json
View file

@ -1,113 +0,0 @@
{
"@context": [
"https://spdx.github.io/spdx-v3/spdx-context.jsonld",
{
"speckl": "https://speckl.scoble.me/ns/v0.2#"
}
],
"@type": "spdx:Document",
"spdx": {
"@id": "spdx:RetryHandler",
"@type": "spdx:Snippet",
"name": "RetryHandler",
"spdxVersion": "3.0.1",
"dataLicense": "CC0-1.0",
"creationInfo": {
"created": "2026-06-30T02:09:28.194Z",
"createdBy": [
"Organization: Speckl",
"tool: speckl-compile-0.2.0"
]
},
"annotations": [
{
"@type": "spdx:Annotation",
"annotationType": "spdx:REVIEW",
"annotator": {
"@type": "spdx:Tool",
"name": "speckl-compile"
},
"timestamp": "2026-06-30T02:09:28.194Z",
"comment": "Review type: manual"
}
]
},
"builtBy": [],
"relationships": [
{
"from": {
"@id": "spdx:RetryHandler"
},
"to": {
"@id": "spdx:speck:FaultHandler"
},
"relationshipType": "spdx:derivesFrom"
},
{
"from": {
"@id": "spdx:RetryHandler"
},
"to": {
"@id": "spdx:requirement:RESILIENCE-REQ-01"
},
"relationshipType": "speckl:satisfies",
"additionalProperties": [
{
"name": "speckl:clause",
"value": "3.1.2"
}
]
},
{
"from": {
"@id": "spdx:RetryHandler"
},
"to": {
"@id": "spdx:requirement:RESILIENCE-REQ-02"
},
"relationshipType": "speckl:satisfies"
},
{
"from": {
"@id": "spdx:RetryHandler"
},
"to": {
"@id": "spdx:agent:Scott Scoble"
},
"relationshipType": "spdx:wasAttributedTo"
},
{
"from": {
"@id": "spdx:RetryHandler"
},
"to": {
"@id": "spdx:source:architecture_review:AR-2024-0215"
},
"relationshipType": "spdx:wasInformedBy"
}
],
"elements": [
{
"@type": "spdx:Requirement",
"@id": "spdx:requirement:RESILIENCE-REQ-01",
"name": "RESILIENCE-REQ-01"
},
{
"@type": "spdx:Requirement",
"@id": "spdx:requirement:RESILIENCE-REQ-02",
"name": "RESILIENCE-REQ-02"
},
{
"@type": "spdx:Person",
"@id": "spdx:agent:Scott Scoble",
"name": "Scott Scoble",
"email": "scott@scoble.me"
},
{
"@type": "spdx:Activity",
"@id": "spdx:source:architecture_review:AR-2024-0215",
"name": "architecture_review - AR-2024-0215",
"type": "architecture_review"
}
]
}