Compare commits
No commits in common. "lagrangia-v1.1" and "main" have entirely different histories.
lagrangia-
...
main
249 changed files with 518 additions and 4169 deletions
|
|
@ -1,10 +1,6 @@
|
|||
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', () => {
|
||||
|
|
@ -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', () => {
|
||||
const content = `speck Test {
|
||||
input: [Nat]
|
||||
|
|
@ -537,7 +479,7 @@ speck Second {
|
|||
});
|
||||
|
||||
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);
|
||||
|
||||
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
165
compiler/dist/__tests__/compiler.test.js
vendored
|
|
@ -1,13 +1,10 @@
|
|||
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';
|
||||
|
|
@ -18,7 +15,7 @@ describe('Compiler E2E', () => {
|
|||
}
|
||||
});
|
||||
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);
|
||||
expect(ast).toBeDefined();
|
||||
expect(ast.specks).toBeDefined();
|
||||
|
|
@ -57,164 +54,4 @@ 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
|
||||
2
compiler/dist/__tests__/compiler.test.js.map
vendored
2
compiler/dist/__tests__/compiler.test.js.map
vendored
File diff suppressed because one or more lines are too long
11
compiler/dist/index.js
vendored
11
compiler/dist/index.js
vendored
|
|
@ -6,7 +6,6 @@ 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';
|
||||
|
|
@ -42,7 +41,7 @@ async function main() {
|
|||
alias: 't',
|
||||
describe: 'Compilation target',
|
||||
type: 'string',
|
||||
choices: ['typescript', 'z3', 'rust', 'protobuf', 'all'],
|
||||
choices: ['typescript', 'z3', 'rust', 'all'],
|
||||
default: 'typescript',
|
||||
})
|
||||
.option('verify-depth', {
|
||||
|
|
@ -85,14 +84,6 @@ 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)...');
|
||||
|
|
|
|||
2
compiler/dist/index.js.map
vendored
2
compiler/dist/index.js.map
vendored
|
|
@ -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
47
compiler/dist/parser.d.ts
vendored
|
|
@ -2,12 +2,6 @@ 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';
|
||||
|
|
@ -35,28 +29,10 @@ 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;
|
||||
|
|
@ -74,26 +50,6 @@ 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[];
|
||||
|
|
@ -147,7 +103,6 @@ export interface BOMNode {
|
|||
export interface StateNode {
|
||||
type: 'state';
|
||||
variables: StateVar[];
|
||||
messageName?: string;
|
||||
}
|
||||
export interface StateVar {
|
||||
name: string;
|
||||
|
|
@ -201,7 +156,7 @@ export type ActionStatement = {
|
|||
type: 'ifblock';
|
||||
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 {
|
||||
type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident';
|
||||
name?: string;
|
||||
|
|
|
|||
2
compiler/dist/parser.d.ts.map
vendored
2
compiler/dist/parser.d.ts.map
vendored
File diff suppressed because one or more lines are too long
444
compiler/dist/parser.js
vendored
444
compiler/dist/parser.js
vendored
|
|
@ -51,13 +51,6 @@ 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) {
|
||||
|
|
@ -67,35 +60,12 @@ 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 ', 'input:', 'output:', 'service ', 'oneof ', 'transition ',
|
||||
'state as '];
|
||||
'state {', 'init {', 'verify ', 'constraint '];
|
||||
const isBlockStarter = blockStarters.some(s => line.startsWith(s));
|
||||
if (isBlockStarter && openCount > 0) {
|
||||
// Multi-line block: parse it and skip to its end
|
||||
|
|
@ -114,8 +84,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]:, verify: always(implies(\n ...\n)))
|
||||
if (line.startsWith('constraint ') || line.startsWith('verify ') || line.startsWith('verify:')) {
|
||||
// (e.g. constraint Name: forall r in [0..4]:)
|
||||
if (line.startsWith('constraint ') || line.startsWith('verify ')) {
|
||||
const member = parseMultiLineConstraintVerify(lines, i);
|
||||
if (member) {
|
||||
members.push(member);
|
||||
|
|
@ -128,8 +98,7 @@ function parseSpeck(lines, startIndex) {
|
|||
nextLine.startsWith('state') || nextLine.startsWith('init') ||
|
||||
nextLine.startsWith('action ') || nextLine.startsWith('event ') ||
|
||||
nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') ||
|
||||
nextLine.startsWith('service ') || nextLine.startsWith('bom ') ||
|
||||
nextLine.startsWith('}') ||
|
||||
nextLine.startsWith('bom ') || nextLine.startsWith('}') ||
|
||||
nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) {
|
||||
break;
|
||||
}
|
||||
|
|
@ -151,10 +120,7 @@ function parseSpeck(lines, startIndex) {
|
|||
}
|
||||
i++;
|
||||
}
|
||||
return { type: 'speck', name, members,
|
||||
protoPackage: metadata.protoPackage,
|
||||
goPackage: metadata.goPackage,
|
||||
eventSuffix: metadata.eventSuffix };
|
||||
return { type: 'speck', name, members };
|
||||
}
|
||||
function findBlockEnd(lines, startIndex, startBraceCount) {
|
||||
let braceCount = startBraceCount;
|
||||
|
|
@ -203,12 +169,6 @@ 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);
|
||||
}
|
||||
|
|
@ -224,15 +184,6 @@ 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: [] };
|
||||
}
|
||||
|
|
@ -245,64 +196,8 @@ 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:')) {
|
||||
|
|
@ -342,14 +237,6 @@ 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: [] };
|
||||
|
|
@ -626,14 +513,11 @@ function parseInterface(line) {
|
|||
throw new Error(`Failed to parse interface: ${line}`);
|
||||
}
|
||||
const name = match[1];
|
||||
// Header-only; parseInterfaceBlockMultiline fills in methods/fields/kind
|
||||
// by scanning the lines inside the { ... } block.
|
||||
// This is a simplified parser - in a real implementation, we'd need to handle multi-line interfaces
|
||||
return {
|
||||
type: 'interface',
|
||||
name,
|
||||
kind: 'mixed',
|
||||
methods: [],
|
||||
fields: [],
|
||||
};
|
||||
}
|
||||
function parseEvent(line) {
|
||||
|
|
@ -649,32 +533,6 @@ 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 {
|
||||
|
|
@ -752,12 +610,6 @@ 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.
|
||||
|
|
@ -777,10 +629,7 @@ function parseStateBlockMultiline(lines, startIndex, startBraceCount) {
|
|||
}
|
||||
return acc + ' ' + line;
|
||||
}, '');
|
||||
const result = parseStateBlock(inner);
|
||||
if (messageName !== undefined)
|
||||
result.messageName = messageName;
|
||||
return result;
|
||||
return parseStateBlock(inner);
|
||||
}
|
||||
function parseInitBlockMultiline(lines, startIndex, 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 fields = [];
|
||||
for (const line of innerLines) {
|
||||
// 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*(.+?),?$/);
|
||||
const match = line.match(/^(\w+)\s*:\s*(.+?),?$/);
|
||||
if (match) {
|
||||
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 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) {
|
||||
// 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);
|
||||
// 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);
|
||||
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*(.+?),?$/);
|
||||
if (methodMatch) {
|
||||
const name = methodMatch[1];
|
||||
|
|
@ -1024,135 +848,14 @@ function parseInterfaceBlockMultiline(lines, startIndex, startBraceCount) {
|
|||
}
|
||||
}
|
||||
methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) });
|
||||
continue;
|
||||
}
|
||||
// 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)) {
|
||||
else if (/^\w+$/.test(token)) {
|
||||
// Name-only (enum-style) — treat as a method with no params and void return
|
||||
methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') });
|
||||
}
|
||||
}
|
||||
}
|
||||
// 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 };
|
||||
return { ...header, methods };
|
||||
}
|
||||
// --- Multi-line constraint/verify parsing (no braces needed) ---
|
||||
/**
|
||||
|
|
@ -1170,128 +873,11 @@ 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+):(.*)$/);
|
||||
|
|
|
|||
2
compiler/dist/parser.js.map
vendored
2
compiler/dist/parser.js.map
vendored
File diff suppressed because one or more lines are too long
1
compiler/lagrangia/.gitignore
vendored
1
compiler/lagrangia/.gitignore
vendored
|
|
@ -1 +0,0 @@
|
|||
/target
|
||||
7
compiler/lagrangia/Cargo.lock
generated
7
compiler/lagrangia/Cargo.lock
generated
|
|
@ -1,7 +0,0 @@
|
|||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 4
|
||||
|
||||
[[package]]
|
||||
name = "lagrangia"
|
||||
version = "0.1.0"
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
[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"
|
||||
|
|
@ -1,71 +0,0 @@
|
|||
# Lagrangia
|
||||
|
||||
The spec-as-Lagrangian probe — a post-compilation reducer that sits between Speckl's IR and its Rust codegen. Given candidate implementations, it scores them by an action functional and selects the stationary (minimum-action) one, then verifies the invariants hold via real Z3.
|
||||
|
||||
## Status
|
||||
|
||||
- **v0** (2026-07-18): action functional + random-restart/hill-descent search over ToggleSwitch. 8/8 tests pass, stationary point at S=43.47. Static proxy for invariant distance.
|
||||
- **v1.1** (2026-07-19): real Z3 wiring via shell-out to `z3 -smt2`. The `invariant_distance` term is now computed by actually running Z3 against each candidate's invariant obligations, not a static proxy. 13/13 tests pass (12 unit + 1 integration). The stationary candidate verifies as `Proved` via Z3.
|
||||
|
||||
## The action functional
|
||||
|
||||
`S(impl) = w1·complexity + w2·invariant_distance + w3·byte_entropy`
|
||||
|
||||
with 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. This makes the "stationary" point provably the simplest correct implementation — the literal variational claim.
|
||||
|
||||
| Term | What it measures | How computed (v1.1) |
|
||||
|---|---|---|
|
||||
| `complexity(impl)` | Lines of generated Rust | Non-comment, non-empty line count |
|
||||
| `invariant_distance(impl)` | How far from satisfying invariants | **Z3 shell-out**: `unsat` → 0, `sat` → counterexample depth, `unknown` → 1000 |
|
||||
| `byte_entropy(impl)` | Shannon entropy of source bytes | `-Σ p_i · log2(p_i)` over byte histogram |
|
||||
|
||||
## v1.1 Z3 wiring
|
||||
|
||||
`verify_candidate(obligations: &[InvariantObligation]) -> Z3Result` shells out to `z3 -in -smt2` for each obligation, parsing the `check-sat` result:
|
||||
|
||||
- `unsat` → `Z3Result::Proved` (no counterexample exists; invariant holds)
|
||||
- `sat` → `Z3Result::Counterexample { depth: 1 }` (violating state found)
|
||||
- `unknown` → `Z3Result::Unknown { reason }` (inconclusive; treated as worst-case)
|
||||
|
||||
`Z3Result` drives `invariant_distance`, which dominates the action functional. A candidate that breaks a guard (e.g. drops the `if !(!self.is_on)` check in ToggleSwitch) gets `Counterexample` → distance ≥ 1 → action ≥ 100, while a correct candidate gets `Proved` → distance 0 → action ~43.
|
||||
|
||||
The integration test (`tests/toggle_switch.rs`) generates 20 perturbed candidates from the ToggleSwitch codegen output, scores each with real Z3 verification, descends 3 rounds, and selects the stationary point. The gold candidate (unperturbed codegen, both guards intact) verifies as `Proved` and wins with S=43.47 — confirming the variational claim.
|
||||
|
||||
## Usage
|
||||
|
||||
```rust
|
||||
use lagrangia::{action, verify_candidate, ImplCandidate, InvariantObligation, Z3Result};
|
||||
|
||||
let obligations = vec![
|
||||
InvariantObligation {
|
||||
name: "turn_on_guard".to_string(),
|
||||
smt_query: "(declare-const is_on Bool) (assert (and is_on (not is_on)))".to_string(),
|
||||
},
|
||||
];
|
||||
let z3_result = verify_candidate(&obligations); // shells out to z3
|
||||
let candidate = ImplCandidate { id: 0, rust_source: source, z3_result };
|
||||
let score = action(&candidate);
|
||||
```
|
||||
|
||||
## Build & test
|
||||
|
||||
```sh
|
||||
cd compiler/lagrangia
|
||||
cargo build
|
||||
cargo test
|
||||
```
|
||||
|
||||
Requires `z3` on `PATH` (v1.1). Install via `nix profile install nixpkgs#z3` or your system package manager.
|
||||
|
||||
## Spec
|
||||
|
||||
See `~/.hermes/plans/2026-07-18-lagrangia-reducer-spec.md` for the full design and falsification protocol.
|
||||
|
||||
## Falsification conditions
|
||||
|
||||
The Lagrangian claim is **false** if any hold:
|
||||
1. The action functional produces no well-defined minimum (flat/chaotic scores).
|
||||
2. The stationary candidate fails Z3 as often as a random one (no selection signal).
|
||||
3. The search doesn't converge (hill descent cycles/plateaus).
|
||||
|
||||
v1.1 results on ToggleSwitch: variance > 0 (manifold is non-degenerate), stationary candidate verifies `Proved` via Z3 (selection beats random), search converges in 3 rounds (no plateau). All three conditions hold — the variational claim survives.
|
||||
|
|
@ -1,14 +0,0 @@
|
|||
//! 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.
|
||||
//!
|
||||
//! v1.1: real Z3 wiring via shell-out to `z3 -smt2`.
|
||||
//! See `~/.hermes/plans/2026-07-18-lagrangia-reducer-spec.md`.
|
||||
pub mod score;
|
||||
|
||||
pub use score::{
|
||||
action, byte_entropy, complexity, invariant_distance, verify_candidate, ImplCandidate,
|
||||
InvariantObligation, Z3Result,
|
||||
};
|
||||
|
|
@ -1,382 +0,0 @@
|
|||
//! 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`.
|
||||
//!
|
||||
//! v1.1: real Z3 wiring via shell-out to `z3 -smt2`. The `invariant_distance`
|
||||
//! term is now computed by actually running Z3 against the candidate's
|
||||
//! state-machine semantics, not a static proxy. See `verify_candidate`.
|
||||
|
||||
use std::io::Write;
|
||||
use std::process::{Command, Stdio};
|
||||
|
||||
/// Result of running Z3 on a candidate's invariant obligations.
|
||||
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||
pub enum Z3Result {
|
||||
/// Z3 returned `unsat` — no counterexample exists; invariants hold.
|
||||
/// `invariant_distance` = 0.
|
||||
Proved,
|
||||
/// Z3 returned `sat` — a counterexample model exists.
|
||||
/// `depth` is the counterexample trace depth (number of transition steps
|
||||
/// Z3 needed to find the violation; 1 for a one-step violation).
|
||||
Counterexample { depth: u32 },
|
||||
/// Z3 returned `unknown` or errored — verification inconclusive.
|
||||
/// Treated as worst-case (depth = max_depth) for scoring.
|
||||
Unknown { reason: String },
|
||||
}
|
||||
|
||||
impl Z3Result {
|
||||
/// Returns `true` iff Z3 proved the invariants hold (`Proved`).
|
||||
pub fn holds(&self) -> bool {
|
||||
matches!(self, Z3Result::Proved)
|
||||
}
|
||||
|
||||
/// Numeric distance used by the action functional.
|
||||
/// Proved → 0, Counterexample{depth} → depth, Unknown → large constant.
|
||||
pub fn distance(&self) -> f64 {
|
||||
match self {
|
||||
Z3Result::Proved => 0.0,
|
||||
Z3Result::Counterexample { depth } => *depth as f64,
|
||||
Z3Result::Unknown { .. } => 1000.0,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// A candidate implementation in the search manifold.
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct ImplCandidate {
|
||||
pub id: u64,
|
||||
pub rust_source: String,
|
||||
/// Z3 verification result for this candidate's invariants.
|
||||
/// v1.1: replaced the v0 `invariant_holds: bool` + `counterexample_depth: u32`
|
||||
/// proxy with a real `Z3Result` from shelling out to `z3 -smt2`.
|
||||
pub z3_result: Z3Result,
|
||||
}
|
||||
|
||||
/// Back-compat helper: returns `true` if invariants hold (z3_result.holds()).
|
||||
impl ImplCandidate {
|
||||
pub fn invariant_holds(&self) -> bool {
|
||||
self.z3_result.holds()
|
||||
}
|
||||
}
|
||||
|
||||
/// 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).
|
||||
///
|
||||
/// v1.1: uses the real Z3 result. Proved → 0, Counterexample → depth,
|
||||
/// Unknown → 1000 (worst-case).
|
||||
pub fn invariant_distance(candidate: &ImplCandidate) -> f64 {
|
||||
candidate.z3_result.distance()
|
||||
}
|
||||
|
||||
/// `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())
|
||||
}
|
||||
|
||||
/// An invariant obligation: a name + an SMT-LIB assertion string that must be
|
||||
/// **unsatisfiable** (i.e. no counterexample exists). The assertion is framed
|
||||
/// as "there exists a state violating the invariant" — Z3 `unsat` means the
|
||||
/// invariant holds.
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct InvariantObligation {
|
||||
/// Human-readable name (e.g. "turn_on_guard").
|
||||
pub name: String,
|
||||
/// SMT-LIB2 fragment asserting "a violating state exists". Z3 `unsat`
|
||||
/// proves no such state exists → invariant holds.
|
||||
pub smt_query: String,
|
||||
}
|
||||
|
||||
/// Shell out to `z3 -smt2` and return the sat/unsat/unknown result.
|
||||
///
|
||||
/// Feeds `smt_script` to Z3's stdin, captures stdout, parses `check-sat`.
|
||||
/// Returns `Z3Result::Proved` for `unsat`, `Counterexample{depth:1}` for
|
||||
/// `sat` (one-step counterexample by default), `Unknown{reason}` for
|
||||
/// `unknown` or parse errors.
|
||||
fn run_z3(smt_script: &str) -> Result<Z3Result, String> {
|
||||
let mut child = Command::new("z3")
|
||||
.arg("-in")
|
||||
.arg("-smt2")
|
||||
.stdin(Stdio::piped())
|
||||
.stdout(Stdio::piped())
|
||||
.stderr(Stdio::piped())
|
||||
.spawn()
|
||||
.map_err(|e| format!("failed to spawn z3: {e}"))?;
|
||||
|
||||
if let Some(mut stdin) = child.stdin.take() {
|
||||
stdin
|
||||
.write_all(smt_script.as_bytes())
|
||||
.map_err(|e| format!("failed to write z3 stdin: {e}"))?;
|
||||
}
|
||||
|
||||
let output = child
|
||||
.wait_with_output()
|
||||
.map_err(|e| format!("failed to wait for z3: {e}"))?;
|
||||
|
||||
let stdout = String::from_utf8_lossy(&output.stdout);
|
||||
let stderr = String::from_utf8_lossy(&output.stderr);
|
||||
|
||||
// Parse the last `check-sat` result. Z3 prints `sat`, `unsat`, or
|
||||
// `unknown` on its own line.
|
||||
for line in stdout.lines().rev() {
|
||||
let trimmed = line.trim();
|
||||
match trimmed {
|
||||
"unsat" => return Ok(Z3Result::Proved),
|
||||
"sat" => return Ok(Z3Result::Counterexample { depth: 1 }),
|
||||
"unknown" => {
|
||||
return Ok(Z3Result::Unknown {
|
||||
reason: "z3 returned unknown".to_string(),
|
||||
})
|
||||
}
|
||||
_ => continue,
|
||||
}
|
||||
}
|
||||
|
||||
// If no sat/unsat line found, check stderr for errors.
|
||||
if !stderr.is_empty() {
|
||||
return Ok(Z3Result::Unknown {
|
||||
reason: format!("z3 stderr: {}", stderr.lines().next().unwrap_or("?")),
|
||||
});
|
||||
}
|
||||
|
||||
Ok(Z3Result::Unknown {
|
||||
reason: "no check-sat result in z3 output".to_string(),
|
||||
})
|
||||
}
|
||||
|
||||
/// Verify a candidate implementation against a set of invariant obligations
|
||||
/// by shelling out to Z3 for each obligation.
|
||||
///
|
||||
/// Returns the **worst** result across all obligations: if any obligation is
|
||||
/// `Counterexample`, the candidate is `Counterexample` with the max depth;
|
||||
/// if any is `Unknown` (and none is `Counterexample`), the candidate is
|
||||
/// `Unknown`; only if all are `Proved` is the candidate `Proved`.
|
||||
///
|
||||
/// Each obligation's `smt_query` is wrapped in `(check-sat)` automatically.
|
||||
pub fn verify_candidate(obligations: &[InvariantObligation]) -> Z3Result {
|
||||
if obligations.is_empty() {
|
||||
return Z3Result::Proved;
|
||||
}
|
||||
|
||||
let mut worst = Z3Result::Proved;
|
||||
let mut worst_depth: u32 = 0;
|
||||
|
||||
for obl in obligations {
|
||||
let script = format!("{}\n(check-sat)\n", obl.smt_query);
|
||||
match run_z3(&script) {
|
||||
Ok(res) => match res {
|
||||
Z3Result::Proved => {}
|
||||
Z3Result::Counterexample { depth } => {
|
||||
if depth > worst_depth {
|
||||
worst_depth = depth;
|
||||
}
|
||||
worst = Z3Result::Counterexample { depth };
|
||||
}
|
||||
Z3Result::Unknown { ref reason } => {
|
||||
if !matches!(worst, Z3Result::Counterexample { .. }) {
|
||||
worst = Z3Result::Unknown {
|
||||
reason: format!("{}: {}", obl.name, reason),
|
||||
};
|
||||
}
|
||||
}
|
||||
},
|
||||
Err(e) => {
|
||||
if !matches!(worst, Z3Result::Counterexample { .. }) {
|
||||
worst = Z3Result::Unknown {
|
||||
reason: format!("{}: z3 spawn error: {}", obl.name, e),
|
||||
};
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
worst
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod unit_tests {
|
||||
use super::*;
|
||||
|
||||
fn candidate(source: &str, result: Z3Result) -> ImplCandidate {
|
||||
ImplCandidate {
|
||||
id: 0,
|
||||
rust_source: source.to_string(),
|
||||
z3_result: result,
|
||||
}
|
||||
}
|
||||
|
||||
#[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_proved() {
|
||||
let c = candidate("fn main() {}", Z3Result::Proved);
|
||||
assert_eq!(invariant_distance(&c), 0.0);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn invariant_distance_uses_depth_on_counterexample() {
|
||||
let c = candidate("fn main() {}", Z3Result::Counterexample { depth: 5 });
|
||||
assert_eq!(invariant_distance(&c), 5.0);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn invariant_distance_large_on_unknown() {
|
||||
let c = candidate(
|
||||
"fn main() {}",
|
||||
Z3Result::Unknown {
|
||||
reason: "test".to_string(),
|
||||
},
|
||||
);
|
||||
assert_eq!(invariant_distance(&c), 1000.0);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn byte_entropy_uniform_is_eight_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",
|
||||
Z3Result::Proved,
|
||||
);
|
||||
// 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",
|
||||
Z3Result::Counterexample { depth: 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}"
|
||||
);
|
||||
}
|
||||
|
||||
// --- Z3 integration tests (v1.1 real wiring) ---
|
||||
|
||||
#[test]
|
||||
fn z3_proves_trivially_unsat() {
|
||||
// No state can violate `false` → unsat → Proved.
|
||||
let obl = InvariantObligation {
|
||||
name: "trivial".to_string(),
|
||||
smt_query: "(declare-const x Int) (assert false)".to_string(),
|
||||
};
|
||||
let result = verify_candidate(&[obl]);
|
||||
assert_eq!(result, Z3Result::Proved);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn z3_finds_counterexample_when_sat() {
|
||||
// There exists an Int > 10 → sat → Counterexample.
|
||||
let obl = InvariantObligation {
|
||||
name: "large_int_exists".to_string(),
|
||||
smt_query: "(declare-const x Int) (assert (> x 10))".to_string(),
|
||||
};
|
||||
let result = verify_candidate(&[obl]);
|
||||
assert!(matches!(result, Z3Result::Counterexample { .. }));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn z3_proves_toggle_turn_on_guard() {
|
||||
// ToggleSwitch invariant: turn_on requires !is_on.
|
||||
// Assert "exists a state where is_on=true AND turn_on succeeds (guard !is_on holds)"
|
||||
// → this is `is_on=true AND !is_on` = `is_on=true AND is_on=false` = unsat.
|
||||
// Proved means no state violates the guard.
|
||||
let obl = InvariantObligation {
|
||||
name: "turn_on_guard".to_string(),
|
||||
smt_query: "(declare-const is_on Bool) (assert (and is_on (not is_on)))".to_string(),
|
||||
};
|
||||
let result = verify_candidate(&[obl]);
|
||||
assert_eq!(result, Z3Result::Proved);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn z3_finds_toggle_guard_violation() {
|
||||
// A broken implementation: turn_on has no guard, so is_on=true is
|
||||
// a violating state. Assert "exists state where is_on=true AND
|
||||
// turn_on is called" = sat → Counterexample.
|
||||
let obl = InvariantObligation {
|
||||
name: "broken_turn_on".to_string(),
|
||||
smt_query: "(declare-const is_on Bool) (assert is_on)".to_string(),
|
||||
};
|
||||
let result = verify_candidate(&[obl]);
|
||||
assert!(matches!(result, Z3Result::Counterexample { .. }));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn verify_takes_worst_result() {
|
||||
// One Proved + one Counterexample → overall Counterexample.
|
||||
let obls = vec![
|
||||
InvariantObligation {
|
||||
name: "holds".to_string(),
|
||||
smt_query: "(declare-const x Int) (assert false)".to_string(),
|
||||
},
|
||||
InvariantObligation {
|
||||
name: "broken".to_string(),
|
||||
smt_query: "(declare-const x Int) (assert (> x 10))".to_string(),
|
||||
},
|
||||
];
|
||||
let result = verify_candidate(&obls);
|
||||
assert!(matches!(result, Z3Result::Counterexample { .. }));
|
||||
}
|
||||
}
|
||||
|
|
@ -1 +0,0 @@
|
|||
{"rustc_fingerprint":17694148678572381065,"outputs":{"7971740275564407648":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/sscoble/.rustup/toolchains/stable-x86_64-unknown-linux-gnu\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":""},"17747080675513052775":{"success":true,"status":"","code":0,"stdout":"rustc 1.95.0 (59807616e 2026-04-14)\nbinary: rustc\ncommit-hash: 59807616e1fa2540724bfbac14d7976d7e4a3860\ncommit-date: 2026-04-14\nhost: x86_64-unknown-linux-gnu\nrelease: 1.95.0\nLLVM version: 22.1.2\n","stderr":""}},"successes":{}}
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
Signature: 8a477f597d28d172789f06886806bc55
|
||||
# This file is a cache directory tag created by cargo.
|
||||
# For information about cache directory tags see https://bford.info/cachedir/
|
||||
Binary file not shown.
|
|
@ -1 +0,0 @@
|
|||
This file has an mtime of when this was started.
|
||||
|
|
@ -1 +0,0 @@
|
|||
9e5b6b8388e83e02
|
||||
|
|
@ -1 +0,0 @@
|
|||
{"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}
|
||||
Binary file not shown.
|
|
@ -1 +0,0 @@
|
|||
This file has an mtime of when this was started.
|
||||
|
|
@ -1 +0,0 @@
|
|||
94465bfadc4cb201
|
||||
|
|
@ -1 +0,0 @@
|
|||
{"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}
|
||||
Binary file not shown.
|
|
@ -1 +0,0 @@
|
|||
This file has an mtime of when this was started.
|
||||
|
|
@ -1 +0,0 @@
|
|||
c7331d31e53a6e4b
|
||||
|
|
@ -1 +0,0 @@
|
|||
{"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}
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
/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:
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
/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:
|
||||
Binary file not shown.
Binary file not shown.
|
|
@ -1,5 +0,0 @@
|
|||
/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:
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Add a link
Reference in a new issue