Skip to content

Commit 8535372

Browse files
varshith-Gitvarshith-Git
committed
embedded: Implement Phase 3 - Deterministic WAL Replay
1 parent b02e416 commit 8535372

3 files changed

Lines changed: 162 additions & 18 deletions

File tree

‎embedded/src/main.rs‎

Lines changed: 64 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ mod flash;
2020
mod snapshot;
2121
mod proof;
2222
mod transport;
23+
mod wal;
2324

2425
use cortex_m_rt::entry;
2526
use embedded_alloc::Heap;
@@ -54,6 +55,15 @@ const D: usize = 16;
5455
const MAX_NODES: usize = 1000;
5556
const MAX_EDGES: usize = 2048;
5657

58+
#[derive(PartialEq)]
59+
enum BootMode {
60+
SelfTest,
61+
WalReplay,
62+
}
63+
64+
// Set Firmware Mode here
65+
const MODE: BootMode = BootMode::WalReplay;
66+
5767
// --- 2. Entry Point ---
5868
#[entry]
5969
fn main() -> ! {
@@ -66,24 +76,60 @@ fn main() -> ! {
6676
// B. Initialize Kernel
6777
let mut state = KernelState::<MAX_RECORDS, D, MAX_NODES, MAX_EDGES>::new();
6878

69-
// C. Deterministic Test Vector
70-
// Q16.16 values:
71-
// 1.0 -> 65536
72-
// 0.5 -> 32768
73-
// -1.0 -> -65536
74-
let mut vector = FxpVector::<D>::new_zeros();
75-
vector.data[0] = FxpScalar(65536); // 1.0
76-
vector.data[1] = FxpScalar(0); // 0.0
77-
vector.data[2] = FxpScalar(-65536); // -1.0
78-
vector.data[3] = FxpScalar(32768); // 0.5
79-
80-
// D. Apply Command (Insert)
81-
let id = RecordId(0);
82-
let cmd = Command::InsertRecord { id, vector };
83-
84-
match state.apply(&cmd) {
85-
Ok(_) => {}
86-
Err(_) => cortex_m::asm::bkpt(),
79+
if MODE == BootMode::SelfTest {
80+
// C. Deterministic Test Vector (Manual)
81+
// Q16.16 values: 1.0 -> 65536, 0.5 -> 32768, -1.0 -> -65536
82+
let mut vector = FxpVector::<D>::new_zeros();
83+
vector.data[0] = FxpScalar(65536); // 1.0
84+
vector.data[1] = FxpScalar(0); // 0.0
85+
vector.data[2] = FxpScalar(-65536); // -1.0
86+
vector.data[3] = FxpScalar(32768); // 0.5
87+
88+
let id = RecordId(0);
89+
let cmd = Command::InsertRecord { id, vector };
90+
91+
match state.apply(&cmd) {
92+
Ok(_) => {}
93+
Err(_) => cortex_m::asm::bkpt(),
94+
}
95+
} else {
96+
// Mode B: WAL Replay
97+
// In production: Read from UART buffer.
98+
// In simulation: Use a hardcoded buffer representing the same command.
99+
// Validates `wal.rs` logic.
100+
101+
// Construct WAL Packet:
102+
// Opcode (0x00) | ID (0) | Dim (16) | [1.0, 0.0, -1.0, 0.5 ...]
103+
// 1 + 4 + 2 + (16 * 4) = 7 + 64 = 71 bytes.
104+
let mut wal_data: [u8; 71] = [0; 71];
105+
let mut idx = 0;
106+
107+
// Opcode
108+
wal_data[idx] = 0x00; idx += 1;
109+
// ID (0)
110+
wal_data[idx..idx+4].copy_from_slice(&0u32.to_le_bytes()); idx += 4;
111+
// Dim (16)
112+
wal_data[idx..idx+2].copy_from_slice(&(D as u16).to_le_bytes()); idx += 2;
113+
114+
// Data
115+
// 0: 65536
116+
wal_data[idx..idx+4].copy_from_slice(&65536i32.to_le_bytes()); idx += 4;
117+
// 1: 0
118+
wal_data[idx..idx+4].copy_from_slice(&0i32.to_le_bytes()); idx += 4;
119+
// 2: -65536
120+
wal_data[idx..idx+4].copy_from_slice(&(-65536i32).to_le_bytes()); idx += 4;
121+
// 3: 32768
122+
wal_data[idx..idx+4].copy_from_slice(&32768i32.to_le_bytes()); idx += 4;
123+
124+
// Remaining 12 are 0 (already 0 init)
125+
126+
match wal::apply_wal_log(&mut state, &wal_data) {
127+
Ok(_) => {},
128+
Err(_) => {
129+
transport::export_error(b"WAL_FAIL");
130+
cortex_m::asm::bkpt();
131+
},
132+
}
87133
}
88134

89135
// -----------------------------------------------------------------------

‎embedded/src/transport.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
const SYNC_WORD: [u8; 4] = [0x55, 0xAA, 0x55, 0xAA];
33
const TYPE_PROOF: u8 = 0x01;
44
const TYPE_SNAPSHOT: u8 = 0x02;
5+
pub const TYPE_WAL: u8 = 0x03;
6+
pub const TYPE_ERR: u8 = 0xEE;
57

68
/// Simulated UART write
79
/// In production, this writes to TX register.
@@ -41,3 +43,7 @@ pub fn export_snapshot(data: &[u8]) {
4143
send_chunk(TYPE_SNAPSHOT, chunk);
4244
}
4345
}
46+
47+
pub fn export_error(err_code: &[u8]) {
48+
send_chunk(TYPE_ERR, err_code);
49+
}

‎embedded/src/wal.rs‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
// This module defines Valori Embedded deterministic WAL replay mode.
2+
//
3+
// Given:
4+
// Initial state S0
5+
// Command log L
6+
//
7+
// Applying:
8+
// Device_A = Apply(S0, L)
9+
// Device_B = Apply(S0, L)
10+
//
11+
// Guarantee:
12+
// hash(Device_A) == hash(Device_B)
13+
//
14+
// This establishes cross-architecture state convergence.
15+
// The MCU does not create memory — it proves it.
16+
17+
use valori_kernel::state::kernel::KernelState;
18+
use valori_kernel::state::command::Command;
19+
use valori_kernel::types::id::RecordId;
20+
use valori_kernel::types::vector::FxpVector;
21+
use valori_kernel::types::scalar::FxpScalar;
22+
23+
const WAL_OP_INSERT: u8 = 0x00;
24+
25+
fn read_u8(buf: &[u8], offset: &mut usize) -> Result<u8, ()> {
26+
if *offset + 1 > buf.len() { return Err(()); }
27+
let val = buf[*offset];
28+
*offset += 1;
29+
Ok(val)
30+
}
31+
32+
fn read_u16(buf: &[u8], offset: &mut usize) -> Result<u16, ()> {
33+
if *offset + 2 > buf.len() { return Err(()); }
34+
let bytes: [u8; 2] = buf[*offset..*offset+2].try_into().map_err(|_| ())?;
35+
*offset += 2;
36+
Ok(u16::from_le_bytes(bytes))
37+
}
38+
39+
fn read_u32(buf: &[u8], offset: &mut usize) -> Result<u32, ()> {
40+
if *offset + 4 > buf.len() { return Err(()); }
41+
let bytes: [u8; 4] = buf[*offset..*offset+4].try_into().map_err(|_| ())?;
42+
*offset += 4;
43+
Ok(u32::from_le_bytes(bytes))
44+
}
45+
46+
fn read_i32(buf: &[u8], offset: &mut usize) -> Result<i32, ()> {
47+
if *offset + 4 > buf.len() { return Err(()); }
48+
let bytes: [u8; 4] = buf[*offset..*offset+4].try_into().map_err(|_| ())?;
49+
*offset += 4;
50+
Ok(i32::from_le_bytes(bytes))
51+
}
52+
53+
pub fn apply_wal_log<const M: usize, const D: usize, const N: usize, const E: usize>(
54+
state: &mut KernelState<M, D, N, E>,
55+
wal_bytes: &[u8]
56+
) -> Result<(), ()> {
57+
let mut offset = 0;
58+
59+
// Process until buffer exhausted
60+
while offset < wal_bytes.len() {
61+
let opcode = read_u8(wal_bytes, &mut offset)?;
62+
63+
match opcode {
64+
WAL_OP_INSERT => {
65+
// Format: RecordID(u32) | Dim(u16) | Values...
66+
let rid = read_u32(wal_bytes, &mut offset)?;
67+
let dim = read_u16(wal_bytes, &mut offset)?;
68+
69+
if dim as usize != D {
70+
return Err(()); // Dimension mismatch
71+
}
72+
73+
let mut vector = FxpVector::<D>::new_zeros();
74+
for i in 0..D {
75+
let val = read_i32(wal_bytes, &mut offset)?;
76+
vector.data[i] = FxpScalar(val);
77+
}
78+
79+
// Apply to Kernel
80+
let id = RecordId(rid);
81+
let cmd = Command::InsertRecord { id, vector };
82+
83+
state.apply(&cmd).map_err(|_| ())?;
84+
}
85+
_ => {
86+
return Err(()); // Invalid Opcode
87+
}
88+
}
89+
}
90+
91+
Ok(())
92+
}

0 commit comments

Comments
 (0)