# H.264 Baseline Profile Video Codec
## H.264 Baseline Profile Video Codec

A **complete H.264 Baseline Profile encoder and decoder** pipeline — pure Lean reference functions with formal proofs, and **fully synthesizable hardware codec** producing playable MP4 files directly from hardware. 16×16 frame → H.264 encode → MP4 mux, all in Signal DSL.

### Pipeline Architecture

```
ENCODER:  Pixels → Intra Pred → DCT → Quant → CAVLC → NAL → H.264 Bitstream → MP4 Container
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
          Fully synthesizable Signal DSL — h264MP4Encoder module (Phase 40)

DECODER:  Bitstream → NAL Parse → CAVLC Decode → Dequant → IDCT → Intra Recon → Pixels
          Synthesizable decoder pipeline (Phase 32)
```

### Hardware MP4 Encoder (Phase 40)

A single hardware module that takes a 16×16 frame and produces a **complete playable MP4 file** — no software post-processing needed.

```
h264MP4Encoder (Signal.loop, 12 registers, ~6100 cycles)
├── h264FrameEncoder (nested sub-module — SPS + PPS + IDR slice)
├── IDR buffer memory (1024×8-bit)
├── MP4 ROM memory (1024×8-bit, host-loaded ftyp+moov template)
└── FSM: buffer encoder output → emit ROM (with runtime patching) → emit mdat
```

| Component | File | Description |
|-----------|------|-------------|
| **MP4 Encoder** | `MP4Encoder.lean` | 12-register FSM, 7 phases, ROM patching at 16 offsets |
| **Frame Encoder** | `FrameEncoder.lean` | 21-register FSM, 20 phases, 3 nested sub-modules |
| **MP4 Muxer** | `MP4Mux.lean` | Software MP4 box builder + ROM template generator |
| **Synth** | `MP4EncoderSynth.lean` | `#writeDesign` → SV + CppSim + JIT |

```bash
lake build h264-mp4-encoder-test && lake exe h264-mp4-encoder-test
# Output: 709 bytes, byte-identical to software muxer
# ffprobe: valid 16×16 H.264 Baseline MP4, 1 frame
```

### Synthesizable Decoder Pipeline (Phase 32)

```
Quantized Levels (16×16-bit) → [Dequant FSM] → [IDCT FSM] → [Reconstruct FSM] → Pixels [0,255]
                                 16 cycles       64 cycles      16 cycles
```

| Module | File | Cycles | Description |
|--------|------|--------|-------------|
| **Dequant** | `DequantSynth.lean` | 16 | level × V[posClass] × 2^(qp/6), fixed QP=20 |
| **Inverse DCT** | `IDCTSynth.lean` | 64 | Butterfly row+col transforms, +32>>6 rounding |
| **Reconstruct** | `ReconstructSynth.lean` | 16 | predicted + residual, clamp [0,255] |
| **Pipeline** | `DecoderSynth.lean` | ~96 | Monolithic FSM: IDLE→DEQUANT→IDCT→RECON→DONE |

Each module generates SystemVerilog + CppSim header + JIT wrapper via `#writeDesign`.

### Modules (14 phases)

| Module | Pure Lean | Proofs | Tests | Synth |
|--------|:---------:|:------:|:-----:|:-----:|
| DRAM Interface | `DRAMInterface.lean` | 3 theorems | `DRAMTest.lean` | Sim model |
| 4×4 Integer DCT/IDCT | `DCT.lean` | bounded error, linearity | `DCTTest.lean` | **IDCTSynth** |
| Quantization | `Quant.lean` | zero/sign preservation | `QuantTest.lean` | **DequantSynth** |
| CAVLC Decode | `CAVLCDecode.lean` | 4 roundtrip proofs | `CAVLCDecodeTest.lean` | — |
| NAL Pack/Parse | `NAL.lean` | roundtrip proof | `NALTest.lean` | — |
| Intra Prediction (9 modes) | `IntraPred.lean` | residual roundtrip | `IntraPredTest.lean` | — |
| Encoder Top | `Encoder.lean` | — | `H264PipelineTest.lean` | — |
| Decoder Top | `Decoder.lean` | — | `H264PipelineTest.lean` | — |
| Frame-Level E2E | — | — | `H264FrameTest.lean` | — |
| Quant/Dequant Roundtrip | `QuantRoundtripSynth.lean` | — | `H264JITTest.lean` | **Full** |
| Reconstruction | `ReconstructSynth.lean` | — | `H264DecoderSynthTest.lean` | **Full** |
| Decoder Pipeline | `DecoderSynth.lean` | — | `H264DecoderSynthTest.lean` | **Full** |
| CAVLC Encoder | `CAVLCSynth.lean` | — | `H264BitstreamTest.lean` | **Full** |
| Frame Encoder | `FrameEncoder.lean` | — | `H264FrameEncoderTest.lean` | **Full** |
| MP4 Encoder | `MP4Encoder.lean` | — | `H264MP4EncoderTest.lean` | **Full** |
| MP4 Muxer | `MP4Mux.lean` | — | `H264PlayableTest.lean` | Software |

### JIT End-to-End Test

The quant→dequant roundtrip module synthesizes to SystemVerilog, compiles via JIT, and passes all 4 tests:

```bash
lake exe h264-jit-test
# === H.264 JIT End-to-End Test ===
# JIT: Compiling IP/Video/H264/gen/quant_roundtrip_jit.cpp...
# JIT: Loaded shared library
#   Test 1: Zero block...        PASS
#   Test 2: DCT coefficients...  PASS (all 16 match)
#   Test 3: Single large coeff... PASS
#   Test 4: Negative coeffs...   PASS
# *** ALL H.264 JIT TESTS PASSED ***
```

### Hardware MP4 Encoder Test

```bash
lake exe h264-mp4-encoder-test
# === H.264 MP4 Encoder JIT Test ===
#   ROM loaded (629 bytes)
#   Frame encoder completed in 5437 cycles
#   Output: 709 bytes — byte-identical to software muxer
#   ftyp: OK, moov: OK, mdat: OK, IDR NAL (0x65): OK
#   ROM vs reference: MATCH, IDR NAL (68 bytes): MATCH
# TEST PASSED
```

### Formal Proofs (all without `sorry`)

- **DRAM**: read-after-write, write-write, read-default
- **DCT**: `|IDCT(DCT(x))[i] - x[i]| ≤ 1`, linearity
- **Quant**: `quant(0) = 0`, sign preservation
- **CAVLC**: `decode(encode(coeffs)) = coeffs` (zero block, mixed coefficients, DC-only, trailing ones)
- **NAL**: `parse(pack(payload)) = payload`
- **Intra**: `predicted + (original - predicted) = original`

---