Function check_lrat 

pub fn check_lrat(num_vars: usize, original: &[Vec<Lit>], lrat: &str) -> bool

Independently verify an LRAT proof against original — the small, naive checker whose simplicity is the trust. Replays each addition’s hint chain (every hinted clause must be unit at its turn, the last must conflict) and accepts iff a line derives the empty clause. Rejects a corrupted hint, a dangling id, or a chain that fails to conflict.