Part of the V&V coverage initiative.
Problem
synth has Rocq proofs for i32 instruction selection and proptest robustness tests but no cargo-fuzz directory. ARM-codegen edges (encoding corner cases, instruction-mix edge cases, odd register allocations) are where silent mis-compilations live and where fuzzing pays the most.
Recognized under DO-178C §6.4.2.2 (random testing) and fits the DO-333 §FM.6.7(f) "translation preserves semantics" story — fuzz the translation validator on adversarial inputs.
Acceptance
Notes
- synth has
tests/proptest_robustness.rs — extend that pattern to fuzz
- Differential against a reference disassembler (e.g. capstone) closes the loop
Part of the V&V coverage initiative.
Problem
synth has Rocq proofs for i32 instruction selection and proptest robustness tests but no cargo-fuzz directory. ARM-codegen edges (encoding corner cases, instruction-mix edge cases, odd register allocations) are where silent mis-compilations live and where fuzzing pays the most.
Recognized under DO-178C §6.4.2.2 (random testing) and fits the DO-333 §FM.6.7(f) "translation preserves semantics" story — fuzz the translation validator on adversarial inputs.
Acceptance
fuzz/directory scaffolded with cargo-fuzz initfuzz_backend_codegen— random WASM inputs produce well-formed ARM output (or clean error)fuzz_regalloc— register allocator never produces invalid schedulesfuzz_encoding— emitted ARM bytes round-trip through a disassembler (differential)rivet.yaml: fuzz targets link to DO-333 §FM.6.7(f) translation-validation evidenceNotes
tests/proptest_robustness.rs— extend that pattern to fuzz