rexact-check 0.2.0

//! Certificate and witness verification.
//!
//! A certificate claims that terms `a` and `b` denote the same language. It
//! carries the alphabet universe, a partition of it into symbol classes, the
//! two start terms and a set of derivative pairs. It is valid when:
//!
//! 1. the classes partition the universe and every symbol set mentioned by
//!    any term is a union of classes (so one representative per class
//!    stands for the whole class);
//! 2. the start pair is identical or listed;
//! 3. in every listed pair both terms agree on accepting the empty string;
//! 4. for every listed pair and every class, the pair of derivatives is
//!    identical or listed.
//!
//! Identical pairs are trivially equivalent (a bisimulation up to equality),
//! so they need not be listed. Conditions 2-4 make the listed set a
//! bisimulation, hence `a` and `b` accept the same strings.

use crate::json::{self, J};
use crate::term::{
    self, leaf_sets, norm_ranges, parse_spec, ranges_intersect, Ctx, Ranges, World, T,
};
use crate::{malformed, on_big_stack, rejected, CheckError};
use std::collections::HashSet;

/// Summary of a verified certificate.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CertInfo {
    /// Number of listed (non-identical) pairs.
    pub pairs: usize,
    /// Number of symbol classes.
    pub classes: usize,
    /// Alphabet mode named by the certificate.
    pub alphabet: String,
}

fn ranges_of(j: &J) -> Result<Ranges, CheckError> {
    let arr = j
        .as_arr()
        .ok_or_else(|| malformed("ranges must be an array"))?;
    let mut out = Vec::with_capacity(arr.len());
    for r in arr {
        let p = r
            .as_arr()
            .ok_or_else(|| malformed("range must be [lo, hi]"))?;
        match (
            p.first().and_then(J::as_num),
            p.get(1).and_then(J::as_num),
            p.len(),
        ) {
            (Some(lo), Some(hi), 2) if lo <= hi && hi <= 0x10FFFF => {
                out.push((lo as u32, hi as u32))
            }
            _ => return Err(malformed("range must be [lo, hi] with lo <= hi <= 10FFFF")),
        }
    }
    Ok(out)
}

fn field<'a>(j: &'a J, name: &str) -> Result<&'a J, CheckError> {
    j.get(name)
        .ok_or_else(|| malformed(format!("missing field '{name}'")))
}

/// Verify a certificate document. Returns a summary or the first problem.
pub fn check_certificate(json_text: &str) -> Result<CertInfo, CheckError> {
    let text = json_text.to_string();
    on_big_stack(move || check_certificate_inner(&text))
}

fn parse_ctx(j: &J, world: &World) -> Result<Option<Ctx>, CheckError> {
    if matches!(j, J::Null) {
        return Ok(None);
    }
    let start = match field(j, "s")? {
        J::Bool(b) => *b,
        _ => return Err(malformed("context 's' must be a boolean")),
    };
    let bits = field(j, "b")?
        .as_num()
        .ok_or_else(|| malformed("context 'b' must be a number"))?;
    let mut tracks = Vec::new();
    for t in field(j, "t")?
        .as_arr()
        .ok_or_else(|| malformed("context 't' must be an array"))?
    {
        tracks
            .push(parse_spec(t.as_str().ok_or_else(|| {
                malformed("tracker state must be a string")
            })?)?);
    }
    if tracks.len() != world.trackers.len()
        || (bits >> world.aux.len().min(63)) != 0 && world.aux.len() < 64
    {
        return Err(malformed(
            "context does not match the declared auxiliary sets and trackers",
        ));
    }
    Ok(Some(Ctx {
        start,
        bits,
        tracks,
    }))
}

fn ctx_key(c: &Option<Ctx>) -> String {
    c.as_ref().map_or("-".to_string(), Ctx::key)
}

fn check_certificate_inner(text: &str) -> Result<CertInfo, CheckError> {
    let doc = json::parse(text)?;
    if field(&doc, "format")?.as_str() != Some("rexact-cert")
        || field(&doc, "version")?.as_num() != Some(1)
    {
        return Err(malformed("not a rexact-cert version 1 document"));
    }
    let alphabet = field(&doc, "alphabet")?
        .as_str()
        .ok_or_else(|| malformed("alphabet must be a string"))?
        .to_string();
    let universe = norm_ranges(ranges_of(field(&doc, "universe")?)?);
    let mut classes: Vec<Ranges> = Vec::new();
    for c in field(&doc, "classes")?
        .as_arr()
        .ok_or_else(|| malformed("classes must be an array"))?
    {
        let r = ranges_of(c)?;
        if norm_ranges(r.clone()) != r || r.is_empty() {
            return Err(malformed("class ranges must be normalised and non-empty"));
        }
        classes.push(r);
    }
    let mut aux: Vec<Ranges> = Vec::new();
    for a in field(&doc, "aux")?
        .as_arr()
        .ok_or_else(|| malformed("aux must be an array"))?
    {
        aux.push(norm_ranges(ranges_of(a)?));
    }
    let mut trackers = Vec::new();
    for t in field(&doc, "trackers")?
        .as_arr()
        .ok_or_else(|| malformed("trackers must be an array"))?
    {
        trackers.push(parse_spec(
            t.as_str()
                .ok_or_else(|| malformed("tracker must be a string"))?,
        )?);
    }
    let world = World {
        universe: universe.clone(),
        aux,
        trackers,
    };

    // (1a) classes are disjoint and cover the universe exactly.
    let mut covered: Ranges = Vec::new();
    for (i, c) in classes.iter().enumerate() {
        for d in &classes[i + 1..] {
            if !ranges_intersect(c, d).is_empty() {
                return Err(rejected("symbol classes overlap"));
            }
        }
        covered.extend(c.iter().copied());
    }
    if norm_ranges(covered) != universe {
        return Err(rejected("symbol classes do not cover the universe exactly"));
    }

    let a = parse_spec(
        field(&doc, "a")?
            .as_str()
            .ok_or_else(|| malformed("'a' must be a string"))?,
    )?;
    let b = parse_spec(
        field(&doc, "b")?
            .as_str()
            .ok_or_else(|| malformed("'b' must be a string"))?,
    )?;
    let start_ctx = parse_ctx(field(&doc, "start_ctx")?, &world)?;
    let mut pairs: Vec<(T, T, Option<Ctx>)> = Vec::new();
    for p in field(&doc, "pairs")?
        .as_arr()
        .ok_or_else(|| malformed("pairs must be an array"))?
    {
        let e = p
            .as_arr()
            .ok_or_else(|| malformed("pair must be [a, b, ctx]"))?;
        match (
            e.first().and_then(J::as_str),
            e.get(1).and_then(J::as_str),
            e.get(2),
            e.len(),
        ) {
            (Some(x), Some(y), Some(c), 3) => {
                pairs.push((parse_spec(x)?, parse_spec(y)?, parse_ctx(c, &world)?))
            }
            _ => return Err(malformed("pair must be [a, b, ctx]")),
        }
    }

    // (1b) every symbol set anywhere is a union of classes within the universe,
    // and every assertion set / lookbehind body is declared.
    let mut sets: Vec<Ranges> = world.aux.clone();
    leaf_sets(&a, &mut sets);
    leaf_sets(&b, &mut sets);
    let mut all_terms: Vec<&T> = vec![&a, &b];
    for (x, y, c) in &pairs {
        leaf_sets(x, &mut sets);
        leaf_sets(y, &mut sets);
        all_terms.push(x);
        all_terms.push(y);
        if let Some(c) = c {
            c.tracks.iter().for_each(|t| leaf_sets(t, &mut sets));
        }
    }
    for t in &world.trackers {
        leaf_sets(t, &mut sets);
    }
    if !all_terms.iter().all(|t| world.declares(t)) {
        return Err(rejected(
            "a term uses an assertion set or lookbehind that the certificate does not declare",
        ));
    }
    for s in &sets {
        if ranges_intersect(s, &universe) != *s {
            return Err(rejected("a term mentions symbols outside the universe"));
        }
        for c in &classes {
            let inter = ranges_intersect(s, c);
            if !inter.is_empty() && inter != *c {
                return Err(rejected(
                    "a symbol set splits a class; the partition is too coarse",
                ));
            }
        }
    }

    // The context only matters when a term is context-dependent; otherwise it is "-".
    let norm = |x: &T, y: &T, c: &Option<Ctx>| {
        if x.dep || y.dep {
            ctx_key(c)
        } else {
            "-".to_string()
        }
    };
    let listed: HashSet<(String, String, String)> = pairs
        .iter()
        .map(|(x, y, c)| (x.key.clone(), y.key.clone(), norm(x, y, c)))
        .collect();
    let ok = |x: &T, y: &T, c: &Option<Ctx>| {
        x.key == y.key || listed.contains(&(x.key.clone(), y.key.clone(), norm(x, y, c)))
    };

    // (2) the start pair.
    if !ok(&a, &b, &start_ctx) {
        return Err(rejected(format!(
            "start pair ({}, {}) is not covered",
            a.key, b.key
        )));
    }
    // (3) acceptance and (4) closure under every class.
    let blank = Ctx {
        start: false,
        bits: 0,
        tracks: Vec::new(),
    };
    for (x, y, c) in &pairs {
        let here = c.as_ref().unwrap_or(&blank);
        if world.accepting(x, here) != world.accepting(y, here) {
            return Err(rejected(format!(
                "pair ({}, {}) disagrees on the empty string",
                x.key, y.key
            )));
        }
        for class in &classes {
            let rep = class[0].0; // smallest member of the class
            let (dx, dy) = (world.derive(x, rep, here), world.derive(y, rep, here));
            let next = if dx.dep || dy.dep {
                Some(world.advance(here, rep))
            } else {
                None
            };
            if !ok(&dx, &dy, &next) {
                return Err(rejected(format!(
                    "pair ({}, {}) has derivative pair ({}, {}) on class starting U+{:04X}, which is not listed",
                    x.key, y.key, dx.key, dy.key, rep
                )));
            }
        }
    }
    Ok(CertInfo {
        pairs: pairs.len(),
        classes: classes.len(),
        alphabet,
    })
}

/// Collect assertion sets and lookbehind bodies from specs, to build a world for witnesses.
fn world_for(specs: &[&T]) -> World {
    fn walk(t: &T, aux: &mut Vec<Ranges>, trk: &mut Vec<T>) {
        match &t.k {
            term::K::Assert(_, w, l) => {
                for r in [w, l].into_iter().flatten() {
                    if !aux.contains(r) {
                        aux.push(r.clone());
                    }
                }
            }
            term::K::Behind(_, b) => {
                if !trk.iter().any(|x| x.key == b.key) {
                    trk.push(b.clone());
                }
            }
            term::K::Ahead(_, x) | term::K::Star(x) | term::K::Not(x) => walk(x, aux, trk),
            term::K::Cat(a, b) => {
                walk(a, aux, trk);
                walk(b, aux, trk);
            }
            term::K::Alt(v) | term::K::And(v) => v.iter().for_each(|x| walk(x, aux, trk)),
            _ => {}
        }
    }
    let (mut aux, mut trk) = (Vec::new(), Vec::new());
    for t in specs {
        walk(t, &mut aux, &mut trk);
    }
    World {
        universe: vec![(0, 0x10FFFF)],
        aux,
        trackers: trk,
    }
}

/// Run a term over `input` from the start of the text; true if it accepts.
fn run_term(t: T, world: &World, input: &[u32]) -> bool {
    let sigma = world.sigma_star();
    let mut ctx = Ctx {
        start: true,
        bits: 0,
        tracks: world
            .trackers
            .iter()
            .map(|b| term::cat(sigma.clone(), b.clone()))
            .collect(),
    };
    let mut t = t;
    for &c in input {
        t = world.derive(&t, c, &ctx);
        ctx = world.advance(&ctx, c);
    }
    world.accepting(&t, &ctx)
}

/// Does `spec` accept `input`? Simple derivative simulation.
pub fn check_witness(spec: &str, input: &[u32]) -> Result<bool, CheckError> {
    let (spec, input) = (spec.to_string(), input.to_vec());
    on_big_stack(move || {
        let t = parse_spec(&spec)?;
        let world = world_for(&[&t]);
        Ok(run_term(t, &world, &input))
    })
}

/// Acceptance of `input` by each of two specs: `(by_a, by_b)`.
pub fn check_counterexample(a: &str, b: &str, input: &[u32]) -> Result<(bool, bool), CheckError> {
    Ok((check_witness(a, input)?, check_witness(b, input)?))
}

#[cfg(test)]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic)]
mod tests {
    use super::*;

    fn cert(a: &str, b: &str, classes: &str, pairs: &str) -> String {
        format!(
            r#"{{"format":"rexact-cert","version":1,"alphabet":"test","universe":[[0,127]],"classes":{classes},"aux":[],"trackers":[],"start_ctx":null,"a":"{a}","b":"{b}","pairs":{pairs}}}"#
        )
    }

    // a* and (a|e)* over {a} vs rest: classes [97] and the rest.
    const CLS: &str = "[[[0,96],[98,127]],[[97,97]]]";

    #[test]
    fn identical_terms_need_no_pairs() {
        let c = cert("(* [61])", "(* [61])", CLS, "[]");
        assert_eq!(check_certificate(&c).unwrap().pairs, 0);
    }

    #[test]
    fn a_valid_nontrivial_certificate_is_accepted() {
        // a* vs (a|e)*: normalisation makes these identical, so use a*  vs  e|aa*
        let c = cert(
            "(* [61])",
            "(| e (. [61] (* [61])))",
            CLS,
            r#"[["(* [61])","(| e (. [61] (* [61])))",null]]"#,
        );
        let info = check_certificate(&c).unwrap();
        assert_eq!((info.pairs, info.classes), (1, 2));
    }

    #[test]
    fn missing_pair_is_rejected_with_e001() {
        let c = cert("(* [61])", "(| e (. [61] (* [61])))", CLS, "[]");
        assert_eq!(check_certificate(&c).unwrap_err().code, "RX-E001");
    }

    #[test]
    fn disagreeing_acceptance_is_rejected() {
        // a+ vs a*: start pair listed but they disagree on the empty string.
        let c = cert(
            "(. [61] (* [61]))",
            "(* [61])",
            CLS,
            r#"[["(. [61] (* [61]))","(* [61])",null]]"#,
        );
        let e = check_certificate(&c).unwrap_err();
        assert_eq!(e.code, "RX-E001");
        assert!(e.message.contains("empty string"));
    }

    #[test]
    fn coarse_partition_is_rejected() {
        let c = cert("[61]", "[61]", "[[[0,127]]]", "[]");
        assert!(check_certificate(&c)
            .unwrap_err()
            .message
            .contains("splits a class"));
    }

    #[test]
    fn partition_must_cover_the_universe() {
        let c = cert("e", "e", "[[[0,96]]]", "[]");
        assert!(check_certificate(&c).unwrap_err().message.contains("cover"));
    }

    #[test]
    fn malformed_documents_are_e004() {
        assert_eq!(check_certificate("{").unwrap_err().code, "RX-E004");
        assert_eq!(
            check_certificate(r#"{"format":"x"}"#).unwrap_err().code,
            "RX-E004"
        );
        let c = cert("(. [61]", "e", CLS, "[]");
        assert_eq!(check_certificate(&c).unwrap_err().code, "RX-E004");
    }

    #[test]
    fn witness_simulation() {
        // (a|b)*c
        let spec = "(. (* [61-62]) [63])";
        assert!(check_witness(spec, &[97, 98, 99]).unwrap());
        assert!(!check_witness(spec, &[97, 98]).unwrap());
        assert!(!check_witness(spec, &[100]).unwrap());
        assert_eq!(
            check_counterexample("[61]", "[62]", &[97]).unwrap(),
            (true, false)
        );
    }

    #[test]
    fn complement_and_intersection() {
        // !a accepts "" and "b" but not "a".
        assert!(check_witness("(! [61])", &[]).unwrap());
        assert!(check_witness("(! [61])", &[98]).unwrap());
        assert!(!check_witness("(! [61])", &[97]).unwrap());
        assert!(check_witness("(& (* [61-62]) (! (. [61] (* [61-62]))))", &[98, 97]).unwrap());
        assert!(!check_witness("(& (* [61-62]) (! (. [61] (* [61-62]))))", &[97, 98]).unwrap());
    }
}