synthesize_acceptance
Derive a machine-checked AcceptanceSpec from a synthesized FrameworkPlan and load it as the session's acceptance judge, generating no-fault, clock, NVIC, and GPIO checks.
Instructions
Auto-derive a machine-checked AcceptanceSpec from the synthesized FrameworkPlan (Pillar D Tier 3) and load it as the session's acceptance judge — welding design synthesis to the acceptance loop. Always emits a no_fault check (init must not HardFault); adds a memory_u32 bits_set check per clock the plan enables (RCC enable bit), a memory_u32 bits_set check per interrupt the plan enables (arch-standard NVIC ISER bit, from the resolved IRQ number), and a masked memory_u32 eq check per configured pin (GPIO MODER = AF/analog; F1's CRL/CRH is skipped). Register/IRQ/port placements come from the session's loaded SVD or explicit register_map/irq_map/gpio_map; anything unresolvable is surfaced, never guessed. Each derived check also carries source provenance (the init function + line that should satisfy it), so a later failure points straight at the fix site. Run design_framework first; load an SVD (start_debug_session/set svd) for clock/NVIC/GPIO checks.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| load | No | Load the derived spec as the session acceptance judge (default true). | |
| name | No | Optional spec name. | |
| irq_map | No | Optional explicit IRQ numbers {line_or_family: {irq_name: number}} (name with or without _IRQn); overrides the SVD. | |
| session | No | Target session id (default 'default'). | |
| gpio_map | No | Optional explicit GPIO port bases {line_or_family: {port_letter: MODER_address}}; overrides the SVD. | |
| stopped_at | No | Optional symbol to also assert the PC reached after init (e.g. 'main'). | |
| include_gpio | No | Emit GPIO MODER checks for configured pins (default true). | |
| include_nvic | No | Emit NVIC ISER checks for enabled interrupts (default true). | |
| register_map | No | Optional explicit RCC placements {line_or_family: {clock: {address, bit}}}; overrides the SVD. | |
| include_no_fault | No | Emit the no_fault check (default true). |