feat(lagrangia): action functional + ToggleSwitch stationary-point test

Implements spec §2.3/§2.4 of the Lagrangia reducer probe
(~/.hermes/plans/2026-07-18-lagrangia-reducer-spec.md).

- compiler/lagrangia/src/score.rs: three scoring functions
  (complexity, invariant_distance, byte_entropy) + action() with
  v0 weights w1=1.0, w2=100.0, w3=0.1.
- compiler/lagrangia/tests/toggle_switch.rs: N=20 candidate search
  with deterministic LCG, hill descent (top-5 × 5 perturbations ×
  3 rounds), argmin selection with id-based tiebreak.
- Asserts: nonzero score variance (manifold not flat), stationary
  candidate holds invariants, argmin well-defined.

Test result: 8 passed (7 unit + 1 integration). Stationary point
found at S=43.47 (complexity=43, inv_dist=0, entropy=4.71) — the
gold ToggleSwitch codegen output, as expected.

Note: invariant_distance uses a static proxy (gold=holds, perturbed
=fails with depth). Full Z3 wiring is a follow-up.

compiler/__tests__/parser.test.ts

@@ -1,6 +1,10 @@
 import { describe, it, expect } from 'vitest';
+import path from 'path';
+import { fileURLToPath } from 'url';
 import { parseSpeckContent, parseSpeckFile } from '../src/parser.js';
 
+const __dirname = path.dirname(fileURLToPath(import.meta.url));
+
 describe('SpeckDL Parser', () => {
   describe('parseSpeckContent', () => {
     it('should parse a minimal speck definition with name', () => {
@@ -100,6 +104,60 @@ 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', () => {
       const content = `speck Test {
   input: [Nat]
@@ -479,7 +537,7 @@ speck Second {
     });
 
     it('should parse full TigerBeetle speck from file', () => {
-      const ast = parseSpeckFile('./__tests__/tigerbeetle.speck');
+      const ast = parseSpeckFile(path.join(__dirname, 'tigerbeetle.speck'));
       expect(ast.specks).toHaveLength(1);
 
       const speck = ast.specks[0];
@@ -524,4 +582,343 @@ 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');
+      }
+    });
+  });
 });

compiler/dist/__tests__/compiler.test.js

@@ -1,10 +1,13 @@
 import { describe, it, expect, beforeAll } from 'vitest';
 import fs from 'fs';
 import path from 'path';
+import { fileURLToPath } from 'url';
+import { execSync } from 'child_process';
 import { parseSpeckFile } from '../parser.js';
 import { generateProvenanceGraph } from '../generators/provenance.js';
 import { generateCycloneDX } from '../generators/cyclonedx.js';
 import { generateSPDX } from '../generators/spdx.js';
+const __dirname = path.dirname(fileURLToPath(import.meta.url));
 describe('Compiler E2E', () => {
     let ast;
     const testOutputDir = './test-output';
@@ -15,7 +18,7 @@ describe('Compiler E2E', () => {
         }
     });
     it('should parse RetryHandler.speck', () => {
-        const specPath = path.join(process.cwd(), '..', 'examples', 'RetryHandler.speck');
+        const specPath = path.join(__dirname, '..', '..', '..', 'examples', 'RetryHandler.speck');
         ast = parseSpeckFile(specPath);
         expect(ast).toBeDefined();
         expect(ast.specks).toBeDefined();
@@ -54,4 +57,164 @@ describe('Compiler E2E', () => {
         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

compiler/dist/index.js

@@ -6,6 +6,7 @@ import { generateProvenanceGraph } from './generators/provenance.js';
 import { generateCycloneDX } from './generators/cyclonedx.js';
 import { generateSPDX } from './generators/spdx.js';
 import { generateTypeScriptStateMachine } from './generators/typescript-state-machine.js';
+import { generateProtobuf } from './generators/protobuf.js';
 import { generateZ3, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
 import { generateRust } from './generators/rust.js';
 import fs from 'fs';
@@ -41,7 +42,7 @@ async function main() {
             alias: 't',
             describe: 'Compilation target',
             type: 'string',
-            choices: ['typescript', 'z3', 'rust', 'all'],
+            choices: ['typescript', 'z3', 'rust', 'protobuf', 'all'],
             default: 'typescript',
         })
             .option('verify-depth', {
@@ -84,6 +85,14 @@ async function main() {
         console.log('\nGenerating Rust state machine...');
         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
     if (options.target !== 'z3' && options.target !== 'rust') {
         console.log('\nGenerating provenance graph (PROV-O JSON-LD)...');

compiler/dist/index.js.map

@@ -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,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"}
+{"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"}

compiler/dist/parser.d.ts

@@ -2,6 +2,12 @@ export interface SpeckNode {
     type: 'speck';
     name: string;
     members: MemberNode[];
+    version?: string;
+    author?: string;
+    license?: string;
+    protoPackage?: string;
+    goPackage?: string;
+    eventSuffix?: string;
 }
 export interface ImportNode {
     type: 'import';
@@ -29,10 +35,28 @@ export interface VerifyNode {
     temporalExpr: string;
     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 {
     type: 'interface';
     name: string;
+    kind: 'enum' | 'record' | 'service' | 'mixed';
     methods: MethodSignature[];
+    fields: InterfaceField[];
 }
 export interface MethodSignature {
     name: string;
@@ -50,6 +74,26 @@ export interface EventNode {
         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 {
     type: 'provenance';
     clauses: ProvenanceClause[];
@@ -103,6 +147,7 @@ export interface BOMNode {
 export interface StateNode {
     type: 'state';
     variables: StateVar[];
+    messageName?: string;
 }
 export interface StateVar {
     name: string;
@@ -156,7 +201,7 @@ export type ActionStatement = {
     type: 'ifblock';
     raw: string;
 };
-export type MemberNode = ImportNode | InputNode | OutputNode | ConstraintNode | VerifyNode | InterfaceNode | EventNode | ProvenanceNode | ReviewNode | DerivesNode | SatisfiesNode | AuthorNode | SourceNode | BOMNode | StateNode | InitNode | ActionNode;
+export type MemberNode = ImportNode | InputNode | OutputNode | ConstraintNode | VerifyNode | InterfaceNode | EventNode | OneofNode | TransitionNode | ProvenanceNode | ReviewNode | DerivesNode | SatisfiesNode | AuthorNode | SourceNode | BOMNode | StateNode | InitNode | ActionNode | ServiceNode;
 export interface TypeExpr {
     type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident';
     name?: string;

compiler/dist/parser.js

@@ -51,6 +51,13 @@ function parseSpeck(lines, startIndex) {
         return null;
     const name = headerMatch[1];
     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 braceCount = 1;
     while (i < lines.length && braceCount > 0) {
@@ -60,12 +67,35 @@ function parseSpeck(lines, startIndex) {
             i++;
             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
         const openCount = (rawLine.match(/{/g) || []).length;
         const closeCount = (rawLine.match(/}/g) || []).length;
         // Check for block-opening members (those that open braces on the same line)
         const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
-            'state {', 'init {', 'verify ', 'constraint '];
+            'state {', 'init {', 'verify ', 'constraint ', 'input:', 'output:', 'service ', 'oneof ', 'transition ',
+            'state as '];
         const isBlockStarter = blockStarters.some(s => line.startsWith(s));
         if (isBlockStarter && openCount > 0) {
             // Multi-line block: parse it and skip to its end
@@ -84,8 +114,8 @@ function parseSpeck(lines, startIndex) {
             continue;
         }
         // Handle constraint/verify blocks that may span multiple lines without braces
-        // (e.g. constraint Name: forall r in [0..4]:)
-        if (line.startsWith('constraint ') || line.startsWith('verify ')) {
+        // (e.g. constraint Name: forall r in [0..4]:, verify: always(implies(\n  ...\n)))
+        if (line.startsWith('constraint ') || line.startsWith('verify ') || line.startsWith('verify:')) {
             const member = parseMultiLineConstraintVerify(lines, i);
             if (member) {
                 members.push(member);
@@ -98,7 +128,8 @@ function parseSpeck(lines, startIndex) {
                         nextLine.startsWith('state') || nextLine.startsWith('init') ||
                         nextLine.startsWith('action ') || nextLine.startsWith('event ') ||
                         nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') ||
-                        nextLine.startsWith('bom ') || nextLine.startsWith('}') ||
+                        nextLine.startsWith('service ') || nextLine.startsWith('bom ') ||
+                        nextLine.startsWith('}') ||
                         nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) {
                         break;
                     }
@@ -120,7 +151,10 @@ function parseSpeck(lines, startIndex) {
         }
         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) {
     let braceCount = startBraceCount;
@@ -169,6 +203,12 @@ function parseMemberBlock(lines, startIndex) {
     if (firstLine.startsWith('state {') || firstLine === 'state') {
         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:')) {
         return parseInitBlockMultiline(lines, startIndex, startBraceCount);
     }
@@ -184,6 +224,15 @@ function parseMemberBlock(lines, startIndex) {
     if (firstLine.startsWith('interface ')) {
         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 ')) {
         return { type: 'provenance', clauses: [] };
     }
@@ -196,8 +245,64 @@ function parseMemberBlock(lines, startIndex) {
     if (firstLine.startsWith('constraint ')) {
         return parseConstraintBlockMultiline(lines, startIndex, startBraceCount);
     }
+    if (firstLine.startsWith('input:') || firstLine.startsWith('output:')) {
+        return parseInputOutputBlock(lines, startIndex, startBraceCount);
+    }
     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) {
     // input:
     if (line.startsWith('input:')) {
@@ -237,6 +342,14 @@ function parseMember(line) {
     if (line.startsWith('event ')) {
         return parseEvent(line);
     }
+    // oneof:
+    if (line.startsWith('oneof ')) {
+        return parseOneof(line);
+    }
+    // transition:
+    if (line.startsWith('transition ')) {
+        return parseTransition(line);
+    }
     // provenance {
     if (line.startsWith('provenance ')) {
         return { type: 'provenance', clauses: [] };
@@ -513,11 +626,14 @@ function parseInterface(line) {
         throw new Error(`Failed to parse interface: ${line}`);
     }
     const name = match[1];
-    // This is a simplified parser - in a real implementation, we'd need to handle multi-line interfaces
+    // Header-only; parseInterfaceBlockMultiline fills in methods/fields/kind
+    // by scanning the lines inside the { ... } block.
     return {
         type: 'interface',
         name,
+        kind: 'mixed',
         methods: [],
+        fields: [],
     };
 }
 function parseEvent(line) {
@@ -533,6 +649,32 @@ function parseEvent(line) {
         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) {
     // This is a simplified parser - in a real implementation, we'd parse the full block
     return {
@@ -610,6 +752,12 @@ function parseSource(line) {
     };
 }
 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 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.
@@ -629,7 +777,10 @@ function parseStateBlockMultiline(lines, startIndex, startBraceCount) {
         }
         return acc + ' ' + line;
     }, '');
-    return parseStateBlock(inner);
+    const result = parseStateBlock(inner);
+    if (messageName !== undefined)
+        result.messageName = messageName;
+    return result;
 }
 function parseInitBlockMultiline(lines, startIndex, startBraceCount) {
     const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
@@ -813,7 +964,24 @@ function parseEventBlockMultiline(lines, startIndex, startBraceCount) {
     const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
     const fields = [];
     for (const line of innerLines) {
-        const match = line.match(/^(\w+)\s*:\s*(.+?),?$/);
+        // Cycle 62: strip inline `//` line-comments from the type expression
+        // 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) {
             fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) });
         }
@@ -826,12 +994,20 @@ function parseInterfaceBlockMultiline(lines, startIndex, 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 methods = [];
+    const fields = [];
     for (const line of innerLines) {
-        // name-only: enum-style values (e.g., "Idle", "Idle, Parsing" comma-separated)
-        // Split on comma and take each trimmed token
-        const tokens = line.split(',').map(s => s.trim()).filter(Boolean);
+        // Cycle 62: strip inline `//` line-comments from each line before
+        // token-splitting. Without this, a field like
+        //   mesh_ip: Bytes   // 4 bytes (IPv4 overlay)
+        // 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) {
-            // Check if it’s a name(params) -> returnType method signature
+            // Check 1: method signature form: name(params) -> returnType
             const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/);
             if (methodMatch) {
                 const name = methodMatch[1];
@@ -848,14 +1024,135 @@ function parseInterfaceBlockMultiline(lines, startIndex, startBraceCount) {
                     }
                 }
                 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') });
             }
         }
     }
-    return { ...header, methods };
+    // Determine the kind based on what we collected
+    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) ---
 /**
@@ -873,11 +1170,128 @@ function parseMultiLineConstraintVerify(lines, startIndex) {
     if (line.startsWith('verify ')) {
         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 ')) {
         return parseConstraintAnyForm(lines, startIndex);
     }
     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) {
     const line = lines[startIndex].trim();
     const namedMatch = line.match(/^constraint\s+(\w+):(.*)$/);

compiler/lagrangia/.gitignore

@@ -0,0 +1 @@
+/target

compiler/lagrangia/Cargo.lock

@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "lagrangia"
+version = "0.1.0"

compiler/lagrangia/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name = "lagrangia"
+version = "0.1.0"
+edition = "2021"
+description = "Lagrangia reducer: action functional + variational selection over Speckl candidate implementations"
+
+[lib]
+name = "lagrangia"
+path = "src/lib.rs"
+
+[[test]]
+name = "toggle_switch"
+path = "tests/toggle_switch.rs"

compiler/lagrangia/src/lib.rs

@@ -0,0 +1,10 @@
+//! Lagrangia reducer — the spec-as-Lagrangian probe.
+//!
+//! Sits between Speckl's IR and its Rust codegen. Given candidate
+//! implementations, scores them by an action functional and selects
+//! the stationary (minimum-action) one.
+//!
+//! See `~/.hermes/plans/2026-07-18-lagrangia-reducer-spec.md`.
+pub mod score;
+
+pub use score::{action, byte_entropy, complexity, invariant_distance, ImplCandidate};

compiler/lagrangia/src/score.rs

@@ -0,0 +1,154 @@
+//! Action functional for the Lagrangia reducer.
+//!
+//! Spec §2.3: `S(impl) = w1·complexity + w2·invariant_distance + w3·byte_entropy`
+//! with v0 weights `w1=1.0, w2=100.0, w3=0.1`.
+//!
+//! The invariant_distance term dominates: any implementation that doesn't
+//! satisfy the spec has action ≥ 100, any that does has action < 50 (for specs
+//! under ~50 lines). This makes the "stationary" point provably the simplest
+//! correct implementation — the literal variational claim.
+
+/// A candidate implementation in the search manifold.
+#[derive(Debug, Clone)]
+pub struct ImplCandidate {
+    pub id: u64,
+    pub rust_source: String,
+    /// Invariant verification result. `true` = invariants hold (distance 0),
+    /// `false` = counterexample found (distance = counterexample depth).
+    /// v0 proxy: depth is estimated from the source; full Z3 wiring is a
+    /// follow-up (see module notes).
+    pub invariant_holds: bool,
+    /// Estimated counterexample depth when `invariant_holds == false`.
+    /// 0 means "not yet scored"; higher = further from satisfying invariants.
+    pub counterexample_depth: u32,
+}
+
+/// v0 weights from spec §2.3.
+pub const W_COMPLEXITY: f64 = 1.0;
+pub const W_INVARIANT_DISTANCE: f64 = 100.0;
+pub const W_BYTE_ENTROPY: f64 = 0.1;
+
+/// `complexity(impl)` — lines of generated Rust code (spec §2.3, row 1).
+///
+/// Counts non-empty, non-comment lines to avoid trivial inflation.
+pub fn complexity(source: &str) -> f64 {
+    source
+        .lines()
+        .filter(|line| {
+            let trimmed = line.trim();
+            !trimmed.is_empty() && !trimmed.starts_with("//")
+        })
+        .count() as f64
+}
+
+/// `invariant_distance(impl)` — how far the implementation is from satisfying
+/// each invariant (spec §2.3, row 2).
+///
+/// Spec calls for Z3 counterexample depth. v0 proxy: if `invariant_holds`
+/// is true, distance = 0. Otherwise, distance = `counterexample_depth`
+/// (estimated statically; full Z3 wiring is a follow-up note).
+pub fn invariant_distance(candidate: &ImplCandidate) -> f64 {
+    if candidate.invariant_holds {
+        0.0
+    } else {
+        candidate.counterexample_depth.max(1) as f64
+    }
+}
+
+/// `byte_entropy(impl)` — Shannon entropy of the generated source bytes
+/// (spec §2.3, row 3), in bits per byte.
+///
+/// Returns 0.0 for empty input (degenerate case, avoids div-by-zero).
+pub fn byte_entropy(source: &[u8]) -> f64 {
+    if source.is_empty() {
+        return 0.0;
+    }
+    let mut counts = [0u32; 256];
+    for &b in source {
+        counts[b as usize] += 1;
+    }
+    let total = source.len() as f64;
+    let mut entropy = 0.0;
+    for &c in &counts {
+        if c == 0 {
+            continue;
+        }
+        let p = c as f64 / total;
+        entropy -= p * p.log2();
+    }
+    entropy
+}
+
+/// `S(impl)` — the action functional (spec §2.3).
+///
+/// `S = w1·complexity + w2·invariant_distance + w3·byte_entropy`
+pub fn action(candidate: &ImplCandidate) -> f64 {
+    W_COMPLEXITY * complexity(&candidate.rust_source)
+        + W_INVARIANT_DISTANCE * invariant_distance(candidate)
+        + W_BYTE_ENTROPY * byte_entropy(candidate.rust_source.as_bytes())
+}
+
+#[cfg(test)]
+mod unit_tests {
+    use super::*;
+
+    fn candidate(source: &str, holds: bool, depth: u32) -> ImplCandidate {
+        ImplCandidate {
+            id: 0,
+            rust_source: source.to_string(),
+            invariant_holds: holds,
+            counterexample_depth: depth,
+        }
+    }
+
+    #[test]
+    fn complexity_counts_non_comment_non_empty_lines() {
+        let src = "// a comment\nlet x = 1;\n\n// another\nlet y = 2;\n";
+        assert_eq!(complexity(src), 2.0);
+    }
+
+    #[test]
+    fn invariant_distance_zero_when_holds() {
+        let c = candidate("fn main() {}", true, 0);
+        assert_eq!(invariant_distance(&c), 0.0);
+    }
+
+    #[test]
+    fn invariant_distance_uses_depth_when_fails() {
+        let c = candidate("fn main() {}", false, 5);
+        assert_eq!(invariant_distance(&c), 5.0);
+    }
+
+    #[test]
+    fn invariant_distance_floors_to_one_when_unscored() {
+        let c = candidate("fn main() {}", false, 0);
+        assert_eq!(invariant_distance(&c), 1.0);
+    }
+
+    #[test]
+    fn byte_entropy_uniform_is_eight_bits() {
+        // 256 bytes, one of each value → 8 bits
+        let bytes: Vec<u8> = (0u16..256).map(|b| b as u8).collect();
+        let e = byte_entropy(&bytes);
+        assert!((e - 8.0).abs() < 1e-9, "got {e}");
+    }
+
+    #[test]
+    fn byte_entropy_zero_for_empty() {
+        assert_eq!(byte_entropy(&[]), 0.0);
+    }
+
+    #[test]
+    fn action_dominated_by_invariant_distance() {
+        // A correct impl: complexity ~5, inv dist 0, entropy ~4 → action ~5.4
+        let correct = candidate("fn main() {\n    let x = 1;\n    let y = 2;\n}\n", true, 0);
+        // An incorrect impl: complexity ~5, inv dist 10, entropy ~4 → action ~1005.4
+        let incorrect = candidate("fn main() {\n    let x = 1;\n    let y = 2;\n}\n", false, 10);
+        let a_correct = action(&correct);
+        let a_incorrect = action(&incorrect);
+        assert!(
+            a_incorrect - a_correct > 100.0,
+            "invariant_distance should dominate: correct={a_correct}, incorrect={a_incorrect}"
+        );
+    }
+}

compiler/lagrangia/target/.rustc_info.json

@@ -0,0 +1 @@
+{"rustc_fingerprint":16580640190452207998,"outputs":{"17747080675513052775":{"success":true,"status":"","code":0,"stdout":"rustc 1.91.1 (ed61e7d7e 2025-11-07) (built from a source tarball)\nbinary: rustc\ncommit-hash: ed61e7d7e242494fb7057f2657300d9e77bb4fcb\ncommit-date: 2025-11-07\nhost: x86_64-unknown-linux-gnu\nrelease: 1.91.1\nLLVM version: 21.1.7\n","stderr":""},"7971740275564407648":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/nix/store/3sgpdha064vl7i8dr7g3d5wrc082d6g5-rustc-1.91.1\noff\npacked\nunpacked\n___\ndebug_assertions\npanic=\"unwind\"\nproc_macro\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_vendor=\"unknown\"\nunix\n","stderr":""}},"successes":{}}

compiler/lagrangia/target/CACHEDIR.TAG

@@ -0,0 +1,3 @@
+Signature: 8a477f597d28d172789f06886806bc55
+# This file is a cache directory tag created by cargo.
+# For information about cache directory tags see https://bford.info/cachedir/

compiler/lagrangia/target/debug/.fingerprint/lagrangia-4ac5ede15d49454c/invoked.timestamp

@@ -0,0 +1 @@
+This file has an mtime of when this was started.

compiler/lagrangia/target/debug/.fingerprint/lagrangia-4ac5ede15d49454c/test-lib-lagrangia

@@ -0,0 +1 @@
+9e5b6b8388e83e02

compiler/lagrangia/target/debug/.fingerprint/lagrangia-4ac5ede15d49454c/test-lib-lagrangia.json

@@ -0,0 +1 @@
+{"rustc":8999539375451197318,"features":"[]","declared_features":"[]","target":6158130320494215290,"profile":1722584277633009122,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/lagrangia-4ac5ede15d49454c/dep-test-lib-lagrangia","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0}

compiler/lagrangia/target/debug/.fingerprint/lagrangia-8f779a778ed86c6f/invoked.timestamp

@@ -0,0 +1 @@
+This file has an mtime of when this was started.

compiler/lagrangia/target/debug/.fingerprint/lagrangia-8f779a778ed86c6f/lib-lagrangia

@@ -0,0 +1 @@
+94465bfadc4cb201

compiler/lagrangia/target/debug/.fingerprint/lagrangia-8f779a778ed86c6f/lib-lagrangia.json

@@ -0,0 +1 @@
+{"rustc":8999539375451197318,"features":"[]","declared_features":"[]","target":6158130320494215290,"profile":8731458305071235362,"path":10763286916239946207,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/lagrangia-8f779a778ed86c6f/dep-lib-lagrangia","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0}

compiler/lagrangia/target/debug/.fingerprint/lagrangia-bcf9fe144a78d857/invoked.timestamp

@@ -0,0 +1 @@
+This file has an mtime of when this was started.

compiler/lagrangia/target/debug/.fingerprint/lagrangia-bcf9fe144a78d857/test-integration-test-toggle_switch

@@ -0,0 +1 @@
+c7331d31e53a6e4b

compiler/lagrangia/target/debug/.fingerprint/lagrangia-bcf9fe144a78d857/test-integration-test-toggle_switch.json

@@ -0,0 +1 @@
+{"rustc":8999539375451197318,"features":"[]","declared_features":"[]","target":5508210232129248235,"profile":1722584277633009122,"path":11149814207312358890,"deps":[[1962247874961037463,"lagrangia",false,122244651869226644]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/lagrangia-bcf9fe144a78d857/dep-test-integration-test-toggle_switch","checksum":false}}],"rustflags":[],"config":2069994364910194474,"compile_kind":0}

compiler/lagrangia/target/debug/deps/lagrangia-4ac5ede15d49454c.d

@@ -0,0 +1,6 @@
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/lagrangia-4ac5ede15d49454c.d: src/lib.rs src/score.rs
+
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/lagrangia-4ac5ede15d49454c: src/lib.rs src/score.rs
+
+src/lib.rs:
+src/score.rs:

compiler/lagrangia/target/debug/deps/lagrangia-8f779a778ed86c6f.d

@@ -0,0 +1,8 @@
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/lagrangia-8f779a778ed86c6f.d: src/lib.rs src/score.rs
+
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/liblagrangia-8f779a778ed86c6f.rlib: src/lib.rs src/score.rs
+
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/liblagrangia-8f779a778ed86c6f.rmeta: src/lib.rs src/score.rs
+
+src/lib.rs:
+src/score.rs:

compiler/lagrangia/target/debug/deps/toggle_switch-bcf9fe144a78d857.d

@@ -0,0 +1,5 @@
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/toggle_switch-bcf9fe144a78d857.d: tests/toggle_switch.rs
+
+/home/sscoble/speckl/compiler/lagrangia/target/debug/deps/toggle_switch-bcf9fe144a78d857: tests/toggle_switch.rs
+
+tests/toggle_switch.rs: