speckl/compiler/src/index.ts

#!/usr/bin/env node

import yargs from 'yargs';
import { hideBin } from 'yargs/helpers';
import { parseSpeckFile } from './parser.js';
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, Z3Options, parseInvariantsFromSource, parseNextFromSource } from './generators/z3.js';
import { generateRust } from './generators/rust.js';
import fs from 'fs';
import path from 'path';

interface CompileOptions {
  outputDir: string;
  bomFormat: 'cdx' | 'spdx' | 'both';
  target: 'typescript' | 'z3' | 'rust' | 'protobuf' | 'all';
  verifyDepth: number;
}

async function main() {
  // Guard: check that dist is not stale before compiling
  const checkScript = path.join(path.dirname(new URL(import.meta.url).pathname), '..', 'check-dist.sh');
  if (fs.existsSync(checkScript)) {
    try {
      const { execSync } = await import('child_process');
      execSync(`bash "${checkScript}"`, { stdio: 'inherit' });
    } catch {
      console.error('\n❌ Cannot compile with stale dist. Rebuild first.');
      process.exit(1);
    }
  }

  const argv = await yargs(hideBin(process.argv))
    .command('$0 <file>', 'Compile a SpeckDL specification', (yargsCmd) => {
      return yargsCmd
        .positional('file', {
          describe: 'SpeckDL file to compile',
          type: 'string',
          demandOption: true,
        })
        .option('output-dir', {
          alias: 'o',
          describe: 'Output directory for compiled artifacts',
          type: 'string',
          default: './out',
        })
        .option('target', {
          alias: 't',
          describe: 'Compilation target',
          type: 'string',
          choices: ['typescript', 'z3', 'rust', 'protobuf', 'all'],
          default: 'typescript' as const,
        })
        .option('verify-depth', {
          alias: 'd',
          describe: 'Bounded model checking depth for Z3 verification',
          type: 'number',
          default: 10,
        })
        .option('bom-format', {
          alias: 'b',
          describe: 'BOM output format',
          type: 'string',
          choices: ['cdx', 'spdx', 'both'],
          default: 'both' as const,
        });
    })
    .help()
    .argv;

  const file = argv.file as string;
  const options = {
    outputDir: argv.outputDir as string,
    bomFormat: argv.bomFormat as 'cdx' | 'spdx' | 'both',
    target: argv.target as 'typescript' | 'z3' | 'rust' | 'protobuf' | 'all',
    verifyDepth: argv.verifyDepth as number,
  };

  console.log(`Compiling ${file}...`);
  
  // Parse the Speck file
  const ast = parseSpeckFile(file);

  const speckCount = ast.specks.length;
  const memberCount = ast.specks.reduce((sum, s) => sum + s.members.length, 0);
  console.log(`AST parsed successfully: ${speckCount} speck(s), ${memberCount} member(s)`);
  
  // Ensure output directory exists
  if (!fs.existsSync(options.outputDir)) {
    fs.mkdirSync(options.outputDir, { recursive: true });
  }
  
  // Read raw source for invariant/next parsing that the AST parser doesn't handle yet
  const rawSource = fs.readFileSync(file, 'utf-8');

  // Generate Rust state machine if target is rust or all
  if (options.target === 'rust' || options.target === 'all') {
    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)...');
    generateProvenanceGraph(ast, options.outputDir);
  }

  // Generate Z3 SMT-LIB2 if target is z3 or all
  if (options.target === 'z3' || options.target === 'all') {
    console.log('\nGenerating Z3 SMT-LIB2...');
    // Parse invariants from raw source for Z3 backend
    for (const speck of ast.specks) {
      const invariants = parseInvariantsFromSource(rawSource, speck.name);
      const nextNode = parseNextFromSource(rawSource, speck.name);
      // Attach parsed data to the AST for the generator
      (speck as any)._invariants = invariants;
      (speck as any)._next = nextNode;
    }
    const z3Options: Z3Options = { verifyDepth: options.verifyDepth };
    generateZ3(ast, options.outputDir, z3Options);
  }

  // Generate TypeScript state machine if not z3-only or rust-only
  if (options.target !== 'z3' && options.target !== 'rust') {
    console.log('\nGenerating TypeScript state machine...');
    generateTypeScriptStateMachine(ast, options.outputDir);

    // Generate BOM based on format selection
    if (options.bomFormat === 'cdx' || options.bomFormat === 'both') {
      console.log('\nGenerating CycloneDX BOM...');
      generateCycloneDX(ast, options.outputDir);
    }

    if (options.bomFormat === 'spdx' || options.bomFormat === 'both') {
      console.log('\nGenerating SPDX BOM...');
      generateSPDX(ast, options.outputDir);
    }
  }
  
  console.log(`\nCompilation complete. Output: ${options.outputDir}/`);
}

main().catch((err) => {
  console.error('Compilation failed:', err);
  process.exit(1);
});