Whether a resource quin q may be consumed to satisfy a demand: a reusable (!-marked)
resource always can; a linear resource only if not already consumed.
Danos-Regnier check: is the proof structure a proof net? n_nodes formula occurrences,
the always-present fixed_edges (axiom / cut / ⊗ links), and the par_switches (each a
pair of candidate edges for one ⅋, one chosen per switching). Returns true iff EVERY
switching graph is a tree. Bounded by MAX_PN_NODES / MAX_PN_PARS.
Is applying rule to a formula with the given reusability licensed? Exchange always; Weakening
and Contraction only on a reusable (!-marked) formula — applying either to a linear
resource is an illegal proof step (resources must be used exactly once).
A ⊗ B consumption: a tensor demand needs both operands available together. Consumes
each linear operand (leaves reusable ones); returns false without mutating if either is
already exhausted.
ZK-gated consumption: a linear resource may be exhausted only if a zero-knowledge proof of
entitlement verifies (the witness stays private). Composes the verification boolean — produced
by zk_proofs / legal_compose::zk_eligibility — with the linear consume-once discipline.
Consumes (and returns true) iff the proof holds AND the resource is available. The webizen-VM
opcode dispatch that invokes this gate is a separate, out-of-(this-crate-scope) wiring step.