SpecTec-Core

A spec programming framework. SpecTec was originally developed for WebAssembly (Wasm-SpecTec), then adapted/generalized for P4 (P4-SpecTec). SpecTec Core is a stripped down version of P4-SpecTec's algorithmic flavor, meant to serve as a base for adaptation to other languages or domains.

Installation

• Install opam version 2.0.5 or higher.

  apt-get install opam
  opam init

• Create OCaml switch for version 5.1.0 Install dune version 3.16.1, bignum version v0.17.0, menhir version 20240715, core version v0.17.1, core_unix version v0.17.0, and bisect_ppx version 2.8.3 via opam.

  opam switch create spectec-core 5.1.0
  eval $(opam env)
  opam install dune bignum menhir core core_unix bisect_ppx

Building the Project

make exe

This creates an executable spectec-core in the project root.

Structure

SpecTec-Core currently consists of three main components.

• SpecTec EL is the surface language in which the spec is authored.
• SpecTec IL (internal language). EL -> IL conversion is called "elaboration". Elaboration makes the spec more algorithmic and unambiguous.
• SpecTec SL (structured language). IL -> SL conversion is called "structuring". Structuring groups related execution paths into explicit branching with over-approximation. This minimizes backtracking, making the SL interpreter much faster than the IL interpreter.
• Interpreter backends for IL/SL.
  • Needs to be coupled with a parser that converts an input file into a SpecTec IL value.

Repository layout:

spectec/lib/lang/        ASTs for el / il / sl / xl
spectec/lib/pass/        parse, elaborate (EL→IL), structure (IL→SL)
spectec/lib/interp/      IL and SL interpreters, builtins, target interface
spectec/lib/cli/         reusable CLI machinery (Target_cli, Task_cli, Subcommand)
spectec/lib/spectec.ml   public facade (pipeline + eval + Error/Task/Target)
spectec/targets/<t>/     per-target code, including each target's CLI module
spectec/bin/             top-level entrypoint that registers each target's CLI
spectec/test/            diff-based test drivers
spectec/testdata/        test inputs

Commands

# print out the IL representation of a SpecTec spec
./spectec-core elab spec/*.spectec
# print the SL representation of a SpecTec spec
./spectec-core struct spec/*.spectec

## P4-specific commands

# parse a P4 program to an IL value (-r to do a roundtrip test)
./spectec-core p4 parse spec/*.spectec -i spectec/testdata/interp/p4-tests/includes -p target/file.p4 [-r]

# run a P4 program based on SpecTec IL/SL
./spectec-core p4 typecheck -i spectec/testdata/interp/p4-tests/includes -p target/file.p4
./spectec-core p4 typecheck -i spectec/testdata/interp/p4-tests/includes -p target/file.p4 --sl

Testing

make test

• Checks parsing, elaboration and structuring using the spectec/examples/p4-concrete spec corpus.
• Checks IL/SL interpreter coupled with the P4 parser using spectec/testdata/interp/p4-tests files.

Adding a New Target

Targets live in spectec/targets/<name>/, separate from spectec/lib/. The reusable CLI infrastructure (Target_cli, Task_cli, Subcommand constructors) lives in spectec/lib/cli/. To add a target:

1. Implement Spectec.Target.S and one or more Spectec.Task.S in spectec/targets/<name>/.
2. Add target-specific built-ins under spectec/targets/<name>/builtins/.
3. For each task, implement a Cli.Task_cli.S module that parses command-line flags into the task's input.
4. Compose those task-CLIs into a Cli : Cli.Target_cli.S module using Cli.Subcommand constructors (make_task, make_parse, make_batch, make_checkpoint).
5. Register the target in spectec/bin/main.ml by adding (Your_target.Cli.name, Your_target.Cli.command) to the top-level command group.

The P4 target (spectec/targets/p4/p4.ml) is the working example.

Contributing

Contributions are welcome — open an issue or pull request. See CONTRIBUTING.md for code conventions, commit and PR format, and rebase guidance.

License

SpecTec-Core is released under the Apache 2.0 license.

Credits

Most of the current codebase is derived from P4-SpecTec, which in turn is largely based on Wasm-SpecTec.