Struct ChoreographyCertificate 

pub struct ChoreographyCertificate {
    pub schedule_digest: u64,
    pub proof: GraphProof,
    pub balances: Vec<BufferBalance>,
    pub sem_counts: Vec<(SemId, u64, u64)>,
    pub compute: Vec<(StageId, ComputeStageCert)>,
    pub numerics: NumericsClaim,
}

Fields

schedule_digest: u64

proof: GraphProof

balances: Vec<BufferBalance>

sem_counts: Vec<(SemId, u64, u64)>

(semaphore, increments or flag sets, wait target).

compute: Vec<(StageId, ComputeStageCert)>

numerics: NumericsClaim

Implementations

impl ChoreographyCertificate

pub fn places(&self) -> usize

Total places across the proof, whichever form it takes.

pub fn transitions(&self) -> usize

Total transitions across the proof, whichever form it takes.

impl ChoreographyCertificate

pub fn recheck(&self, p: &SpatialProgram) -> bool

Independent re-check: the digest binds the certificate to p; the graph is rebuilt from p’s schedule and compared; the witness is verified against the token-free arcs; balances and semaphore counts are recomputed; every SAT certificate is re-run through the PR/RUP checker.

pub fn with_witness_tampered(&self) -> Self

A tampered copy: the liveness witness permuted so it is no longer a topological order — must fail recheck. This is the probe that proves the witness is load-bearing rather than decorative, so it has to bite in BOTH proof forms.

Whole form: swap one real producer/consumer pair, the most surgical break there is. Per-section form: reverse the first section long enough to have an arc — the graph is not carried there, so a pair cannot be picked out, and reversing violates EVERY token-free arc at once instead of one.

Trait Implementations

impl Clone for ChoreographyCertificate

fn clone(&self) -> ChoreographyCertificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ChoreographyCertificate

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

Formats the value using the given formatter.

impl PartialEq for ChoreographyCertificate

fn eq(&self, other: &ChoreographyCertificate) -> 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 StructuralPartialEq for ChoreographyCertificate