CubicPathwidth.Alg.DiffMain

Source file CubicPathwidth/Alg/DiffMain.lean of the Lean project (how it is built).

This file is not part of the libraries that lake build builds.

import Lean.Data.Json
import CubicPathwidth.Alg.Port

/-!
# Differential test runner: Lean port vs `sweep.py`

Reads the JSON written by `ancillary/experiments/sweep-algorithms/lean_diff.py` and compares every
recorded case with the Lean port. Run from `lean/` (after `lake build CubicPathwidth.Alg.Port`):

```
lake env lean --run CubicPathwidth/Alg/DiffMain.lean \
  ../ancillary/experiments/sweep-algorithms/lean_diff/cases.json [fn|all] [maxCasesPerFn]
```

Comparison rules (bags are compared as SETS: each bag is sorted and deduplicated on both
sides; the list of bags is compared in order):
* `induced`, `components`, `reduce_record`, `connector_order`: exact lists (orders matter);
* `plain_layout`, `algo_T2a`: bags;
* `switched_layout`, `pd_tw2`, `undo`: if Python raised, the Lean flag must be `true`;
  otherwise the flag must be `false` and the bags equal;
* `algo_T1`, `algo_mixed`: flag `false` and bags equal;
* `algo_T4`: fallback `false`, bags equal, `Dn` equal, and `final` equal (kinds and node
  lists in order).
Moreover every Lean output of a decomposition is checked with `checkPD` (a mirror of
`check_pd`), also when Python raised and the Lean fallback produced it.
Exit code 0 iff every selected case passes.
-/

open Lean CubicPathwidth.Alg

namespace CubicPathwidth.Alg.Diff

/-! ## JSON decoding -/

def natList (j : Json) : Except String (List Nat) := do
  (← j.getArr?).toList.mapM (·.getNat?)

def natListList (j : Json) : Except String (List (List Nat)) := do
  (← j.getArr?).toList.mapM natList

def graphOf (j : Json) : Except String Graph := do
  let nodes ← natList (← j.getObjVal? "nodes")
  let adj ← natListList (← j.getObjVal? "adj")
  return Graph.ofAdjLists nodes adj

/-- Labels `[[v, num, den], …]` as a function (missing vertices get `0`). -/
def labelsOf (j : Json) : Except String Labels := do
  let rows ← (← j.getArr?).toList.mapM fun r => do
    let v ← (← r.getArrVal? 0).getNat?
    let num ← (← r.getArrVal? 1).getInt?
    let den ← (← r.getArrVal? 2).getNat?
    return (v, mkRat num den)
  let tab : Std.HashMap Nat Rat := rows.foldl (fun t p => t.insert p.1 p.2) ∅
  return fun v => tab.getD v 0

def opOf (j : Json) : Except String Op := do
  let tag ← (← j.getArrVal? 0).getStr?
  if tag == "red" then
    return .red (← (← j.getArrVal? 1).getNat?) (← natList (← j.getArrVal? 2))
  else if tag == "del" then
    return .del (← (← j.getArrVal? 1).getNat?)
  else throw s!"unknown op {tag}"

def opsOf (j : Json) : Except String (List Op) := do
  (← j.getArr?).toList.mapM opOf

def kindOf (s : String) : Except String FinalKind :=
  if s == "sweep" then pure .sweep else if s == "thin" then pure .thin
  else throw s!"unknown kind {s}"

/-! ## Canonical forms -/

def dedupSorted : List Nat → List Nat
  | a :: b :: t => if a == b then dedupSorted (b :: t) else a :: dedupSorted (b :: t)
  | l => l

def canonBag (B : Bag) : List Nat := dedupSorted (B.mergeSort (· ≤ ·))

def canonBags (bags : List Bag) : List (List Nat) := bags.map canonBag

def showBags (bags : List (List Nat)) : String :=
  let s := toString bags
  if s.length > 300 then (s.take 300).toString ++ "…" else s

def cmpBags (lean py : List Bag) : Option String :=
  let a := canonBags lean
  let b := canonBags py
  if a == b then none
  else some s!"bags differ: lean {a.length} bags {showBags a} vs python {b.length} bags {showBags b}"

def opsStr (ops : List Op) : String :=
  toString (ops.map fun | .red v nb => s!"red {v} {nb}" | .del w => s!"del {w}")

/-- Computable mirror of Python `check_pd` (sweep.py lines 19-30): every node in some bag,
the bags of each node contiguous, every edge in some bag. -/
def checkPD (G : Graph) (bags : List Bag) : Bool := Id.run do
  let mut first : Std.HashMap Nat Nat := ∅
  let mut last : Std.HashMap Nat Nat := ∅
  let mut cnt : Std.HashMap Nat Nat := ∅
  for (B, i) in bags.zipIdx do
    for v in canonBag B do
      if !first.contains v then first := first.insert v i
      last := last.insert v i
      cnt := cnt.insert v (cnt.getD v 0 + 1)
  for v in G.nodes do
    if !first.contains v then return false
    if cnt.getD v 0 != last.getD v 0 - first.getD v 0 + 1 then return false
  for v in G.nodes do
    for u in G.nbrs v do
      if max (first.getD u 0) (first.getD v 0) > min (last.getD u 0) (last.getD v 0) then
        return false
  return true

/-! ## One case -/

/-- If Python raised, the Lean flag must be set (and the Lean output must still be a valid
decomposition, which `k ()` does not check: see `withValid`); otherwise the flag must be
clear and `k ()` decides. -/
def checkFlag (flag : Bool) (raised : Bool) (k : Unit → Option String) : Option String :=
  if raised then (if flag then none else some "python raised but the lean flag is false")
  else if flag then some "lean fallback fired but python did not raise"
  else k ()

/-- Also require that the Lean output is a valid decomposition of `G` (`checkPD`). -/
def withValid (G : Graph) (bags : List Bag) (r : Option String) : Option String :=
  match r with
  | some m => some m
  | none => if checkPD G bags then none else some "lean output is not a valid decomposition"

def raisedOf (j : Json) : Bool :=
  match j.getObjValAs? Bool "raised" with
  | .ok b => b
  | .error _ => false

/-- Returns `none` if the case passes, or a description of the mismatch. -/
def runCase (fn : String) (j : Json) : Except String (Option String) := do
  match fn with
  | "induced" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let keep ← natList (← j.getObjVal? "keep")
    let ks : Std.HashSet Nat := keep.foldl (fun s v => s.insert v) ∅
    let H := G.induced ks.contains
    let P ← graphOf (← j.getObjVal? "out_graph")
    return if (H.nodes, H.adjLists) == (P.nodes, P.adjLists) then none
      else some s!"lean {repr H} vs python {repr P}"
  | "components" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let out ← natListList (← j.getObjVal? "out")
    return if G.components == out then none else some s!"lean {G.components} vs python {out}"
  | "plain_layout" | "algo_T2a" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let Y ← labelsOf (← j.getObjVal? "labels")
    let out ← natListList (← j.getObjVal? "out")
    let res := if fn == "plain_layout" then plainLayout G Y else algoT2a G Y
    return withValid G res (cmpBags res out)
  | "connector_order" =>
    let Qs ← natList (← j.getObjVal? "Qs")
    let items ← natListList (← j.getObjVal? "items")
    let out ← natList (← j.getObjVal? "out")
    let (q, flag) := connectorOrderF Qs items
    return checkFlag flag false fun _ =>
      if q == out then none else some s!"lean {q} vs python {out}"
  | "switched_layout" | "algo_T1" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let Y ← labelsOf (← j.getObjVal? "labels")
    let out ← natListList (← j.getObjVal? "out")
    let (res, flag) := if fn == "algo_T1" then algoT1F G Y else switchedLayoutF G Y
    return withValid G res (checkFlag flag (raisedOf j) fun _ => cmpBags res out)
  | "reduce_record" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let P ← graphOf (← j.getObjVal? "out_graph")
    let ops ← opsOf (← j.getObjVal? "ops")
    let (H, ops', flag) := reduceRecordF G
    return checkFlag flag false fun _ =>
      if (H.nodes, H.adjLists) != (P.nodes, P.adjLists) then
        some s!"graph: lean {repr H} vs python {repr P}"
      else if ops' != ops then some s!"ops: lean {opsStr ops'} vs python {opsStr ops}"
      else none
  | "pd_tw2" =>
    let H ← graphOf (← j.getObjVal? "graph")
    let out ← natListList (← j.getObjVal? "out")
    let (res, flag) := pdTw2F H
    return withValid H res (checkFlag flag (raisedOf j) fun _ => cmpBags res out)
  | "undo" =>
    let F ← graphOf (← j.getObjVal? "F")
    let R ← graphOf (← j.getObjVal? "R")
    let ops ← opsOf (← j.getObjVal? "ops")
    let bagsR ← natListList (← j.getObjVal? "bagsR")
    let out ← natListList (← j.getObjVal? "out")
    let (res, flag) := undoF F ops R bagsR
    return withValid F res (checkFlag flag (raisedOf j) fun _ => cmpBags res out)
  | "algo_mixed" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let Y ← labelsOf (← j.getObjVal? "labels")
    let out ← natListList (← j.getObjVal? "out")
    let (res, flag) := algoMixedF G (fun _ => Y)
    return withValid G res (checkFlag flag false fun _ => cmpBags res out)
  | "algo_T4" =>
    let G ← graphOf (← j.getObjVal? "graph")
    let Y ← labelsOf (← j.getObjVal? "labels")
    let out ← natListList (← j.getObjVal? "out")
    let dn ← (← j.getObjVal? "Dn").getNat?
    let final ← (← (← j.getObjVal? "final").getArr?).toList.mapM fun e => do
      let k ← kindOf (← (← e.getArrVal? 0).getStr?)
      let ns ← natList (← e.getArrVal? 1)
      return (k, ns)
    let r := algoT4Full G (fun _ => Y)
    let lf := r.final.map fun e => (e.kind, e.graph.nodes)
    return withValid G r.bags <| checkFlag r.fallback false fun _ =>
      match cmpBags r.bags out with
      | some m => some m
      | none =>
        if r.numDeleted != dn then some s!"Dn: lean {r.numDeleted} vs python {dn}"
        else if lf != final then some s!"final: lean {repr lf} vs python {repr final}"
        else none
  | _ => throw s!"unknown fn {fn}"

end CubicPathwidth.Alg.Diff

open CubicPathwidth.Alg.Diff in

def main (args : List String) : IO UInt32 := do
  let path := args.headD "../experiments/sweep-algorithms/lean_diff/cases.json"
  let only := args.getD 1 "all"
  let maxPer := (args.getD 2 "1000000000").toNat!
  let txt ← IO.FS.readFile path
  let j ← IO.ofExcept (Json.parse txt)
  let cases ← IO.ofExcept ((← IO.ofExcept (j.getObjVal? "cases")).getArr?)
  let mut stats : Std.HashMap String (Nat × Nat) := ∅
  let mut shown : Std.HashMap String Nat := ∅
  let mut order : Array String := #[]
  for c in cases do
    let fn ← IO.ofExcept ((← IO.ofExcept (c.getObjVal? "fn")).getStr?)
    if only != "all" && only != fn then continue
    let (pass, total) := stats.getD fn (0, 0)
    if total ≥ maxPer then continue
    if !stats.contains fn then order := order.push fn
    match runCase fn c with
    | .error e =>
      stats := stats.insert fn (pass, total + 1)
      IO.println s!"[{fn} #{total}] decode error: {e}"
    | .ok none => stats := stats.insert fn (pass + 1, total + 1)
    | .ok (some msg) =>
      stats := stats.insert fn (pass, total + 1)
      let k := shown.getD fn 0
      if k < 3 then
        IO.println s!"[{fn} #{total}] MISMATCH: {msg}"
      shown := shown.insert fn (k + 1)
  let mut allOk := true
  for fn in order do
    let (pass, total) := stats.getD fn (0, 0)
    if pass != total then allOk := false
    IO.println s!"{fn}: {pass}/{total} pass"
  return if allOk then 0 else 1