nibli_protocol/
lib.rs

1//! Shared wire-format types for the nibli proof trace protocol.
2//!
3//! Both nibli-engine (native, serializes) and nibli-ui (browser WASM, deserializes)
4//! depend on this crate. The proof types (`ProofRule`/`ProofStep`/`ProofTrace`/
5//! `LogicalTerm`) ARE the canonical `nibli-types` types, re-exported here; this
6//! crate owns only their JSON helpers and the KB-status wire types.
7//!
8//! Human-readable RENDERING of these types (proof text, the `RenderedNode` tree,
9//! and fact humanization) lives in `nibli-render`, not here — this crate is the
10//! wire-format authority only.
11
12use serde::{Deserialize, Serialize};
13
14// The canonical proof types in `nibli-types` ARE the serde wire types; re-export
15// them so every consumer keeps using `nibli_protocol::{ProofRule, ProofStep,
16// ProofTrace, LogicalTerm}` unchanged. The JSON (de)serialization helpers live
17// below as free functions (`proof_trace_to_json` / `proof_trace_from_json`).
18pub use nibli_types::logic::{LogicalTerm, ProofRule, ProofStep, ProofTrace};
19
20/// The native TCP compute-backend JSON-Lines client, shared by nibli-host (the WASM
21/// host) and nibli-engine (the native embedder). Gated behind the
22/// `compute-client` feature so `std::net` never enters the browser build.
23#[cfg(feature = "compute-client")]
24pub mod compute_client;
25
26// ── KB status wire types ──
27
28#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
29pub struct LineResult {
30    pub line_number: u32,
31    pub text: String,
32    pub success: bool,
33    pub fact_id: Option<u64>,
34    pub error: Option<String>,
35    /// Non-blocking nibli KR lint notes for this line (NIBLI_KR §12
36    /// L1–L9), rendered as `[Note: …]` rows. `default` keeps old wire JSON
37    /// (no field) deserializing.
38    #[serde(default)]
39    pub notes: Vec<String>,
40}
41
42#[derive(Clone, Debug, PartialEq, Serialize, Deserialize)]
43pub struct KbStatus {
44    pub asserted: u32,
45    pub errors: u32,
46    pub skipped: u32,
47    pub line_results: Vec<LineResult>,
48}
49
50// ── Proof trace JSON helpers ──
51//
52// `ProofTrace` is re-exported from `nibli-types` (it IS the serde wire type), so
53// these JSON helpers live here as free functions — `nibli-types` stays free of
54// serde_json (and so does the WASM guest, which never serializes proofs to JSON).
55
56/// Serialize a proof trace to its wire JSON string.
57pub fn proof_trace_to_json(trace: &ProofTrace) -> String {
58    serde_json::to_string(trace).unwrap_or_default()
59}
60
61/// Deserialize a proof trace from its wire JSON string.
62pub fn proof_trace_from_json(s: &str) -> Option<ProofTrace> {
63    serde_json::from_str(s).ok()
64}
65
66// Term display (`LogicalTerm::display` / `trace_display`) now lives as inherent
67// methods on the canonical `nibli_types::logic::LogicalTerm` enum (re-exported
68// here), so it is shared by find-witness formatting and proof rendering alike.
69
70#[cfg(test)]
71mod tests {
72    use super::*;
73
74    fn one_step(rule: ProofRule) -> ProofTrace {
75        ProofTrace {
76            steps: vec![ProofStep {
77                rule,
78                holds: true,
79                children: vec![],
80            }],
81            root: 0,
82            naf_dependent: false,
83            cwa_false: false,
84        }
85    }
86
87    #[test]
88    fn proof_trace_json_roundtrip() {
89        let trace = one_step(ProofRule::Asserted {
90            fact: "gerku(adam)".to_string(),
91        });
92        let json = proof_trace_to_json(&trace);
93        let back = proof_trace_from_json(&json).unwrap();
94        assert_eq!(trace, back);
95    }
96
97    #[test]
98    fn wire_json_shape_is_byte_stable() {
99        // The rule-level wire JSON the UI parses must be byte-stable across the
100        // consolidation: an Asserted rule serializes with the `asserted` tag and
101        // the named `fact` field. (Rule tags + string fields are unchanged by the
102        // canonical-as-wire unification — only nested term encoding changed.)
103        let trace = one_step(ProofRule::Asserted {
104            fact: "gerku(adam)".to_string(),
105        });
106        let json = proof_trace_to_json(&trace);
107        assert!(json.contains(r#""type":"asserted""#), "json: {json}");
108        assert!(json.contains(r#""fact":"gerku(adam)""#), "json: {json}");
109    }
110
111    #[test]
112    fn predicate_check_serializes_named_fields() {
113        let trace = one_step(ProofRule::PredicateCheck {
114            method: "store".to_string(),
115            detail: "gerku(adam)".to_string(),
116        });
117        let json = proof_trace_to_json(&trace);
118        assert!(json.contains(r#""type":"predicate_check""#), "json: {json}");
119        assert!(json.contains(r#""method":"store""#), "json: {json}");
120        assert!(json.contains(r#""detail":"gerku(adam)""#), "json: {json}");
121    }
122
123    #[test]
124    fn exists_witness_term_encoding_is_pinned() {
125        // Choice B: the embedded term is the canonical `LogicalTerm` enum
126        // (snake_case serde), so the proof JSON nests it as `{"constant":"adam"}`.
127        // This is the new term-encoding contract.
128        let trace = one_step(ProofRule::ExistsWitness {
129            var: "x".to_string(),
130            term: LogicalTerm::Constant("adam".to_string()),
131        });
132        let json = proof_trace_to_json(&trace);
133        assert!(json.contains(r#""type":"exists_witness""#), "json: {json}");
134        assert!(json.contains(r#""var":"x""#), "json: {json}");
135        assert!(
136            json.contains(r#""term":{"constant":"adam"}"#),
137            "json: {json}"
138        );
139    }
140}
nibli_protocol/lib.rs

nibli_protocol/
lib.rs
