Inclusion proofs and behavioral predicates

This figure documents the historical i386 source baseline. Current native x86-64/AArch64 qualification is recorded separately; this is not an ELF64 or native SMP implementation diagram.

Full-size SVG
Inclusion proofs and behavioral predicates Recompute a versioned event-summary hash, verify its Merkle path and verify the root signature against the selected node key. This establishes inclusion in that signed epoch. The prove predicates independently scan available events and report PROVED, VIOLATED or INSUFFICIENT_DATA. Neither mechanism establishes complete history, program correctness or externally certified identity; missing evidence limits the claim. event->leaf event->predicate leaf->path path->sign sign->inclusion predicate->result event Archived event summary leaf Recompute versioned event hash path Merkle inclusion path → epoch root sign Verify Ed25519 root signature against selected node public key inclusion Claim: this summary belongs to this signed segment epoch predicate Separate prove predicates scan available event evidence result Predicate outcomes PROVED · within checked evidence VIOLATED · counterexample found INSUFFICIENT_DATA · cannot conclude note Inclusion ≠ completeness ≠ program correctness ≠ externally certified identity. Missing / retained-away evidence limits every claim.
Inclusion proofs and behavioral predicates Recompute a versioned event-summary hash, verify its Merkle path and verify the root signature against the selected node key. This establishes inclusion in that signed epoch. The prove predicates independently scan available events and report PROVED, VIOLATED or INSUFFICIENT_DATA. Neither mechanism establishes complete history, program correctness or externally certified identity; missing evidence limits the claim. Inclusion is not completeness, program correctness, or certified identity. Missing / retained-away evidence limits claims. event->leaf event:e->predicate:e leaf->path path->sign sign->claim predicate->result event Archived event summary leaf Versioned event hash path Merkle inclusion path → epoch root sign Verify Ed25519 root signature against selected node key claim Claim: summary belongs to this signed epoch predicate Separate prove predicates: scan available events result PROVED: checked evidence VIOLATED: counterexample INSUFFICIENT_DATA: cannot conclude

Being included in a signed epoch is not the same claim as satisfying a behavioral predicate.

Text equivalent and source references
  • Recompute a versioned event-summary hash, verify its Merkle path and verify the root signature against the selected node key. This establishes inclusion in that signed epoch.
  • The prove predicates independently scan available events and report PROVED, VIOLATED or INSUFFICIENT_DATA. Neither mechanism establishes complete history, program correctness or externally certified identity; missing evidence limits the claim.

Claim / evidence dependency. Source paths refer to the atlas baseline; the kernel checkout is private.

  • kernel/graph/cjournal.c · epoch proof and signature verification
  • include/prove.h · proof_result_t
  • kernel/graph/prove.c · predicate evaluators

Download SVG · Editable DOT