Skip to main content

Module verified_compiler

logicaffeine_compile::codegen_sva

Module verified_compiler 

Source
Expand description

Verified SVA Compiler via Futamura Projections

P1: Specialize SVA synthesis for a fixed spec → compiled generator P2: Specialize the specializer for SVA synthesis → SVA compiler

The key property: compiled output == interpreted output. Compiler correctness is inherited from the projection framework.

Structs§

CompiledGenerator
A compiled SVA generator — P1 output.
SvaCompiler
An SVA compiler — P2 output.

Functions§

compile_sva_compiler
P2: Specialize the specializer for SVA synthesis → SVA compiler.
compile_sva_generator
P1: Specialize SVA synthesis for a fixed spec → compiled generator.
verify_compiler_correctness
Verify compiler correctness: compiled output == interpreted output.