Struct WfNetConst 

pub struct WfNetConst<const SOUNDNESS: SoundnessState> { /* private fields */ }

A WF-net with soundness state encoded as a const generic parameter.

The SOUNDNESS parameter tracks whether soundness is unknown, claimed, or witnessed. Crucially, WfNetConst<{SoundnessState::Witnessed}> is only constructible via WfNetConst::witness_soundness, which requires a SoundnessProof — a type that is itself only constructible inside this module or via the wasm4pm graduation bridge.

Direct struct-literal construction fails because _seal is a private field.

use wasm4pm_compat::petri::{WfNetConst, SoundnessProof};
use wasm4pm_compat::law::SoundnessState;

// Build an unknown-soundness net, then claim it:
let unknown = WfNetConst::<{ SoundnessState::Unknown }>::new();
let claimed = unknown.claim_sound();
// To reach Witnessed, you would call claimed.witness_soundness(proof)
// where proof is only producible by the wasm4pm engine or this module.

use wasm4pm_compat::petri::WfNetConst;
use wasm4pm_compat::law::SoundnessState;
// ERROR: _seal is a private field; direct forged construction is impossible.
let forged: WfNetConst<{ SoundnessState::Witnessed }> = WfNetConst {
    _seal: todo!(),
};

Implementations

impl WfNetConst<{ SoundnessState::Unknown }>

pub fn new() -> Self

Construct a WfNetConst in the initial Unknown soundness state.

use wasm4pm_compat::petri::WfNetConst;
use wasm4pm_compat::law::SoundnessState;
let _wf = WfNetConst::<{ SoundnessState::Unknown }>::new();

pub fn claim_sound(self) -> WfNetConst<{ SoundnessState::Claimed }>

Advance to Claimed soundness — a type-level re-tagging only.

use wasm4pm_compat::petri::WfNetConst;
use wasm4pm_compat::law::SoundnessState;
let claimed: WfNetConst<{ SoundnessState::Claimed }> =
    WfNetConst::<{ SoundnessState::Unknown }>::new().claim_sound();

impl WfNetConst<{ SoundnessState::Claimed }>

pub fn witness_soundness( self, _proof: SoundnessProof, ) -> WfNetConst<{ SoundnessState::Witnessed }>

Advance a claimed WF-net to Witnessed — requires a SoundnessProof.

The SoundnessProof is only constructible inside this module or by the wasm4pm graduation bridge. This is the sanctioned, non-forgeable path to SoundnessState::Witnessed.

// Conceptual: the wasm4pm bridge supplies the proof after verifying soundness.
let witnessed = claimed.witness_soundness(proof_from_wasm4pm);

Trait Implementations

impl Default for WfNetConst<{ SoundnessState::Unknown }>

fn default() -> Self

Returns the “default value” for a type.

impl WfNetQuery for WfNetConst<{ SoundnessState::Claimed }>

fn soundness_state(&self) -> SoundnessState

The soundness state of this WF-net as a runtime value.

impl WfNetQuery for WfNetConst<{ SoundnessState::Unknown }>

fn soundness_state(&self) -> SoundnessState

The soundness state of this WF-net as a runtime value.

impl WfNetQuery for WfNetConst<{ SoundnessState::Witnessed }>

fn soundness_state(&self) -> SoundnessState

The soundness state of this WF-net as a runtime value.