[transfix]

Why

cvc::state's json(), ptree(), json(j) and restore() became iterative in #668 and #674, but they are still synchronous cvc::state calls. That leaves two gaps:

• Scripts can't use them. A state_exec script has no way to serialize or load a subtree.
• The scheduler can't split them. The work runs whole on whatever thread calls it.

state_exec already runs its deep-data work a slice per step: #658 added data.step_nodes, and #665 the sliced stdlib. This adds JSON builtins that work the same way. They share their code with cvc::state, so the two can't drift.

What

• cvc/state/state_json.h holds one implementation, three classes. Each can stop after any number of nodes or values and go on later:

  • state_subtree_cursor is the pre-order walk. It snapshots each node's value and children under that node's own lock, and holds the children it has yet to visit by owning pointer.

  • state_json_writer writes the document. Its text is byte for byte what write_json(ptree()) wrote: boost's escapes (create_escapes) and its pretty layout. ptree(), json() and save() now use the cursor and writer.

  • state_json_reader loads a document as read_json() + ptree(pt) did. json(j) and restore() now use it. It keeps read_json's handling of:

    • grammar and byte-order marks;
    • UTF-8 checks, escapes and surrogates;
    • number text, true/false/null;
    • array keys, error messages and line numbers.

    It checks the whole document before it sets anything, so a malformed document sets nothing. Its container stack lives on the heap rather than one call per level, so nesting costs no native stack.

• (state-json path) and (state-from-json path doc) (intrinsics) run that writer and reader as data jobs:
  • Slices: each step does data.step_nodes units, where a unit is a node or value, plus one per 256 bytes (kDataNodeBytes). A slice ends when its units are spent, so a long value counts for its bytes.
  • Budget: the work counts against max_steps and max_time, and other processes run between slices.
  • Allocation limit: state-json's text is held to limits.max_alloc_bytes as it grows, and each slice's growth is reported to heap accounting once.
  • Links: state-json reads through a transparent link and returns nil for a missing node, like state-get. state-from-json writes through a writable transparent link, like state-set, and returns nil.
  • Removed nodes: a node another process removes between slices is still written, as it was when its parent was read.
• state-json joins the Ariadne predicates' allowlist of side-effect-free state readers.
• Docs: STATE_EXEC_GRAMMAR.md (deep data on the executor) and STATE_EXEC_DEVELOPER_GUIDE.md (state-tree operations, sliced work).

Measurements (MSVC 14.38 Release, Windows)

• Nested-document load on a small stack: the old read_json() + ptree(pt) path overflowed past 349 levels on 64 KiB, 1,897 on 256 KiB and 7,994 on 1 MiB. The new reader loads 100,000 levels on 64 KiB (StateDeepTree.ADeeplyNestedDocumentLoads).
• Slicing at 64 units a step:
  • (state-json "wide") (20,000 children) and (state-json "deep") (a 1,000-level chain, about 1 MB of text) take 74 or more data steps, and their data_nodes cover every node plus the text's bytes.
  • (state-from-json "copy" (state-json "wide")) takes over 200.

Tests

• state_deep_tree_test (+4):
  • JsonIsWhatWriteJsonWrites: keys and values with every byte except ., compared with boost's writer over ptree(); a slice at a time gives the same text.
  • JsonLoadsWhatReadJsonLoads: 13 documents, compared with read_json + ptree(pt). They cover nested legacy documents, arrays, numbers, literals, escapes and surrogates, a BOM, an empty document, a top-level scalar, duplicate keys and UTF-8. Loading a value at a time gives the same tree.
  • AMalformedDocumentFailsAsReadJsonDoesAndSetsNothing: 21 malformed documents, with the same messages and lines as read_json, and nothing set.
  • ADeeplyNestedDocumentLoads: 100,000 levels of objects and of arrays, on a 64 KiB stack.
• state_exec_data_steps_test (+7, on async_scheduler):
  • the output equals json() for a deep and a wide subtree, with the data steps and nodes counted;
  • state-from-json copies a subtree and restores one into its own node;
  • other processes run between slices;
  • max_steps kills the job;
  • a malformed document whose check spans steps sets nothing (state-from-json: line 1: expected value);
  • the allocation limit stops state-json;
  • nodes removed mid-walk are still written.
• Locally: all 4137 ctest cases pass. pycvc: 21 of 22 scripts pass; test_pycvc_lod.py still crashes at exit after its checks, as before.
• clang-format 18 is clean.