Enum GraphProof 

pub enum GraphProof {
    Whole {
        graph: MarkedGraph,
        liveness: LivenessWitness,
        cases: Vec<TripCase>,
        case_witnesses: Vec<LivenessWitness>,
    },
    PerSection {
        sections: Vec<SectionProof>,
        witnesses: Vec<LivenessWitness>,
        places: usize,
        transitions: usize,
    },
}

HOW THE LIVENESS PROOF IS CARRIED.

★ WHY THERE ARE TWO FORMS. The unrolled event graph of a four-layer Qwen3.8 forward is 196,211,828 places and 102,936,753 transitions — 35 GB, two thirds of peak, and the reason the sixty-four-layer model did not fit on a 125 GB box. The graph is not irreducibly that big: it is a DISJOINT UNION of one subgraph per section joined only by the program-counter chain, because on the composed forward NO buffer, semaphore or multicast group is touched by two sections. Proving one section at a time and keeping only the witnesses turns a 35 GB artifact into per-section orders, and peak from the sum of the sections into the largest of them.

★ WHY THE CUT IS SOUND, AND WHERE IT REFUSES. Commoner’s condition asks that every directed cycle carry a token. Cutting the program-counter arcs between sections only REMOVES arcs, so it can invent no cycle; it could only HIDE one that runs backwards from a later section to an earlier one — and a backwards arc is exactly a place produced in one section and consumed in another. section_ranges checks for that and hands back None when it finds one, so a program that does not decompose is proved whole, at the old cost, rather than proved wrongly.

Variants

Whole

One graph for the whole choreography. The form every single-section program takes, and the fallback whenever a place crosses a section boundary. The graph itself is carried, so recheck compares it structurally.

Fields

graph: MarkedGraph

liveness: LivenessWitness

cases: Vec<TripCase>

The graph at every count of the program’s trips’ windows, ordered by case_witnesses.

case_witnesses: Vec<LivenessWitness>

PerSection

One proof per section, plus the totals. The graphs are rebuilt by recheck from the schedule and matched against the carried digests.

★ THE WITNESSES ARE A TABLE, BECAUSE A DECODER REPEATS ITSELF. Sections with the same dataflow build the same graph up to resource names, and so the same topological order. Measured on the composed Qwen3.8 forward: 117 sections carry 11 DISTINCT witnesses at 4 layers, and 232 sections carry the SAME 11 at 8 — the table is constant in depth, while one witness per section grows with it (3,923 entries at 4 layers, 7,759 at 8; the real-width certificate was 810 MB at 2 layers). Sharing is safe by construction: recheck still rebuilds EVERY section’s own graph and verifies the witness it references against that graph, so a shared witness that does not fit a section is a refusal, never an acceptance.

Fields

sections: Vec<SectionProof>

witnesses: Vec<LivenessWitness>

places: usize

transitions: usize

Implementations

impl GraphProof

pub fn places(&self) -> usize

pub fn transitions(&self) -> usize

pub fn whole_graph(&self) -> Option<&MarkedGraph>

The whole graph, when one is carried. None is not “no proof”: it is the per-section form, whose graphs are rebuilt on demand by ChoreographyCertificate::recheck.

pub fn whole_graph_mut(&mut self) -> Option<&mut MarkedGraph>

The whole graph, mutably — the seam a mutation probe needs to corrupt a carried graph.

pub fn witnesses(&self) -> Vec<&LivenessWitness>

Every witness this proof carries, in section order (one entry for the whole form).

pub fn witness_of_section(&self) -> Option<Vec<usize>>

For the per-section form, the witness-table index each section uses, in section order.

Trait Implementations

impl Clone for GraphProof

fn clone(&self) -> GraphProof

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GraphProof

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GraphProof

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for GraphProof

fn eq(&self, other: &GraphProof) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for GraphProof

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for GraphProof

impl StructuralPartialEq for GraphProof