Expand description
Property-Based Testing for Compiler Correctness
This module defines formal properties that the compiler must satisfy and uses proptest to automatically generate test cases to verify these properties.
§Properties
- Type Preservation: Compilation preserves type safety
- Semantic Preservation: Compiled code has same behavior as source
- Memory Safety: Generated code respects memory bounds
- Control Flow Correctness: Branch targets are valid
- Optimization Soundness: Optimizations don’t change semantics
Structs§
- Compiler
Properties - Compiler properties to verify