EPHRC Hardware Root of Control — SHA3-256 FPGA Enforcement Prototype for XC7Z020 (Placed, Routed, Formally Verified)

A synthesizable, placed-and-routed FPGA enforcement prototype implementing the ExecutionProof Hardware Root of Control (EPHRC) on a Xilinx XC7Z020 (Zynq-7000, CLG484-1 package). The enforcement core uses a real iterative Keccak-f[1600] SHA3-256 hash (FIPS 202), not a stand-in, for action-digest binding and ProofRecord signature generation. Part of the ExecutionProof / Coherent Inheritance Framework (CIF) corpus, Remnant Fieldworks Inc. Contents RTL sources: ephrc_top.sv (top), ephrc_interlock.sv (5-state FSM enforcement core), ephrc_sha3.sv (iterative SHA3-256, KAT-verified against FIPS 202 test vectors for empty string and 'abc'), ephrc_pkg.sv (type definitions), ephrc_fpga_top.sv (serial-scan I/O harness for package pin budget). Bitstream: ephrc_top.bit — 4,045,676 bytes, real placed-and-routed XC7Z020 bitstream. Xilinx sync word 0xAA995566 at offset 160, device IDCODE 0x03727093 at offset 240 (exact match for xc7z020clg484-1). Produced via open-source flow: Yosys 0.33 → nextpnr-xilinx → Project X-Ray (fasm2frames + xc7frames2bit). Utilization: 8,663 LUTs (8.14%), 5,147 FFs (4.84%), 57 CARRY4, 20/200 IOBs. Fmax ≈ 77.08 MHz (critical path 12.97 ns). Formal verification: SymbiYosys/yosys-smtbmc with z3 solver. Bounded model checking (depth 12) and k-induction proof of the fail-closed execute_enable invariant — execute_enable can be 1 only in the single matched-EXECUTE branch; it is default-0 at reset, cleared at operation start, and never asserted on mismatch, replay, stale-policy, or malformed input. All properties PASS. Cover trace demonstrates a reachable ALLOW path. Proof transcripts and witness VCD included. Testbenches: tb_ephrc.sv (7/7 functional experiments PASS: exact-action binding, destination drift, amount drift, HOLD gate, replay prevention, policy-version invalidation, fail-closed), tb_sha3.sv (2/2 NIST KAT PASS). Honest-scope caveats Open-source-toolchain bitstream (Yosys/nextpnr/X-Ray), not a Vivado-signed or timing-closed sign-off. Behavioral simulation + formal property proof + place-and-route, not final silicon execution on a physical board. The 851-bit logical I/O of ephrc_top exceeds the 200-pin XC7Z020 CLG484 package; a disclosed serial-scan harness (ephrc_fpga_top.sv) wraps the core unchanged for standalone P&R. On a real Zynq deployment, the PS AXI bus would replace the scan chain. SHA3-256 is real and KAT-verified but not CAVP-certified; HMAC-SHA3 and key management are software-layer responsibilities. Internal/founder-led validation; independent reproduction is the next phase. Governing sentence: "We will accept the result that is true, not the result we hoped to see."