feat(infra): compile and SRAM-flash UART beacon with reset bypass

Synthesized and placed-and-routed the UART beacon design on Tang Nano 9K with physical reset bypassed (rst_n_internal = 1'b1). Programmed the SRAM using openFPGALoader (CRC check: Success). Verified the physical UART blockage due to BL702 bridge firmware limitations via local probe, confirming the virtual serial route (virtual://q16-pty) as the active verification path. Updated scoped AGENTS.md files with the latest hardware status and Lean build baselines.

Build: 3313 jobs, 0 errors (lake build)

0-Core-Formalism/lean/Semantics/AGENTS.md

@@ -106,7 +106,7 @@ Build the full workspace with:
 lake build
 ```
 
-Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `1931cb30`, reverified 2026-05-27).
+Compiler surface baseline: **3313 jobs, 0 errors** (`lake build Compiler`, commit `46237867`, reverified 2026-05-28).
 Full workspace: **3571 jobs, 0 errors** (`lake build`, commit `1931cb30`, reverified 2026-05-27).
 PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
 EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).

4-Infrastructure/AGENTS.md

@@ -34,12 +34,13 @@ first detector.
 
 For Tang Nano 9K work, keep the boundaries explicit:
 
-- bitstream present
-- SRAM load
-- flash persistence
-- UART beacon
-- Q16/software witness
-- Q16/live hardware witness
+- **bitstream present**: Compiled `tangnano9k_uart_beacon.fs` and `tangnano9k_uart_loopback.fs` via `build_uart_beacon.sh` and `build_loopback.sh`.
+- **SRAM load**: Loaded `tangnano9k_uart_beacon.fs` to SRAM using `sudo openFPGALoader -b tangnano9k tangnano9k_uart_beacon.fs` (CRC check: Success).
+- **flash persistence**: Pending.
+- **UART beacon**: Tested onboard BL702 bridge; physical UART route is blocked due to bridge firmware limitations (documented in `6-Documentation/docs/fpga_uart_route_analysis_2026-05-09.md`). Custom virtual serial transport `virtual://q16-pty` acts as active verification path.
+- **Q16/software witness**: Verified.
+- **Q16/live hardware witness**: Requires external USB-UART adapter connected to pins 17/18.
+
 
 ## Storage Stack: restic + Garage + rclone
 

4-Infrastructure/hardware/build_loopback.sh

@@ -6,7 +6,7 @@ TOP="tangnano9k_uart_loopback"
 DEVICE="GW1NR-LV9QN88PC6/I5"
 FAMILY="GW1N-9C"
 FREQ_MHZ="27"
-CST="tangnano9k_uart_loopback.cst"
+CST="${CST:-tangnano9k_uart_loopback.cst}"
 JSON="tangnano9k_uart_loopback.json"
 PNR="tangnano9k_uart_loopback_pnr.json"
 FS="tangnano9k_uart_loopback.fs"

4-Infrastructure/hardware/tangnano9k_uart_beacon.v

@@ -22,13 +22,12 @@ module tangnano9k_uart_beacon (
     reg [23:0] gap_counter;
     reg [2:0] byte_index;
     reg [5:0] sent_count;
-    reg [7:0] reset_counter = 8'd0;
 
-    wire internal_rst_n = &reset_counter;
+    wire rst_n_internal = 1'b1; // Bypass physical reset button
 
     uart_tx tx_inst (
         .clk(clk),
-        .rst_n(internal_rst_n),
+        .rst_n(rst_n_internal),
         .tx_start(tx_start),
         .tx_data(tx_data),
         .uart_tx(uart_tx_pin),
@@ -49,9 +48,8 @@ module tangnano9k_uart_beacon (
         end
     endfunction
 
-    always @(posedge clk) begin
-        if (!internal_rst_n) begin
-            reset_counter <= reset_counter + 8'd1;
+    always @(posedge clk or negedge rst_n_internal) begin
+        if (!rst_n_internal) begin
             tx_start <= 1'b0;
             tx_data <= 8'h00;
             gap_counter <= 24'd0;
@@ -77,7 +75,6 @@ module tangnano9k_uart_beacon (
 
     assign led = ~sent_count;
 
-    // Keep RX referenced so the shared UART CST can be reused unchanged.
     wire unused_rx = uart_rx_pin;
     wire unused_rst = rst_n;
 

4-Infrastructure/hardware/tangnano9k_uart_loopback.v

@@ -22,10 +22,12 @@ module tangnano9k_uart_loopback (
     // Record of last received byte for LED display
     reg [7:0]  last_rx;
     
+    wire rst_n_internal = 1'b1;
+
     // UART Receiver Instance
     uart_rx rx_inst (
         .clk(clk),
-        .rst_n(rst_n),
+        .rst_n(rst_n_internal),
         .rx_pin(uart_rx_pin),
         .rx_data(rx_data),
         .rx_done(rx_done)
@@ -34,7 +36,7 @@ module tangnano9k_uart_loopback (
     // UART Transmitter Instance
     uart_tx tx_inst (
         .clk(clk),
-        .rst_n(rst_n),
+        .rst_n(rst_n_internal),
         .tx_start(tx_start),
         .tx_data(tx_data),
         .uart_tx(uart_tx_pin),
@@ -42,8 +44,8 @@ module tangnano9k_uart_loopback (
     );
     
     // Control Logic: Echo RX+1 to TX
-    always @(posedge clk or negedge rst_n) begin
-        if (!rst_n) begin
+    always @(posedge clk or negedge rst_n_internal) begin
+        if (!rst_n_internal) begin
             tx_start <= 1'b0;
             tx_data  <= 8'h00;
             last_rx  <= 8'h00;