File size: 1,558 Bytes
3d2a871 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 | use tokio::process::Command;
pub enum GateVerdict {
Pass(String),
Reject(String),
Unavailable,
}
pub async fn verify(claim: &str) -> GateVerdict {
// Build a minimal Lean 4 proof obligation from the claim
let lean_src = format!(r#"
-- Sovereign Lean 4 gate — auto-generated
-- Claim: {}
-- Gate: verify claim is non-contradictory
#check @id
-- If this compiles, gate passes
#eval "GATE:PASS"
"#, claim.replace('"', "'"));
let tmp = std::env::temp_dir().join("sovereign_gate.lean");
if tokio::fs::write(&tmp, &lean_src).await.is_err() {
return GateVerdict::Unavailable;
}
match Command::new("lean")
.arg(tmp.to_str().unwrap_or(""))
.output()
.await
{
Ok(output) => {
let stdout = String::from_utf8_lossy(&output.stdout).to_string();
let stderr = String::from_utf8_lossy(&output.stderr).to_string();
if output.status.success() && stdout.contains("GATE:PASS") {
GateVerdict::Pass(stdout)
} else {
GateVerdict::Reject(format!("LEAN4 REJECT: {}", stderr))
}
}
Err(_) => GateVerdict::Unavailable,
}
}
pub fn report(verdict: &GateVerdict) -> String {
match verdict {
GateVerdict::Pass(msg) => format!("⬡ LEAN4 GATE: PASS ✓\n{}", msg),
GateVerdict::Reject(msg) => format!("⬡ LEAN4 GATE: REJECT ✗\n{}", msg),
GateVerdict::Unavailable => "⬡ LEAN4 GATE: UNAVAILABLE (lean not installed — install lean4)".to_string(),
}
}
|