Module algebra 

Pure bounded-retention and floor-transition algebra.

Structs

FloorComputation

Reproducible outputs of the participant physical-floor rule.

MandatoryCapacity

Results of the mandatory-class debt and absolute-fit formulas.

RecoveryTransfer

Exact post-transfer values for a recovery transaction of charge r.

RecoveryTransferError

Invalid or unrepresentable recovery-charge transfer.

ResourceVector

One entry/byte resource vector before arithmetic widening.

WideResourceVector

One entry/byte resource vector after widening to the protocol arithmetic domain.

Enums

AdmissibleFloor

What a binding-fate floor measured earlier is allowed to install NOW.

BaselineError

Invalid inputs to the retained-baseline formula.

ResourceDimension

Resource dimension, in the contract’s entry-before-byte precedence.

Functions

admissible_installed_floor

Decides what an earlier-measured binding-fate floor may install against the frontier as it stands now.

floor_transition

Computes the participant physical-floor rule.

mandatory_capacity

Computes the mandatory-class debt and its two required checks.

marker_clamped_floor

Lowers a computed floor so it cannot cross the lowest retained marker.

no_edge_legal

Checks the only legal no-edge state: zero debt plus full-K fit.

recovery_transfer

Transfers an exact recovery record charge from K_remaining into B.

retained_baseline

Computes B = S + ((I - C) × marker_max) componentwise.

zero_debt_admission

Checks the zero-debt ordinary-admission invariant B + Q + K <= cap.

zero_debt_capacity_failure

Returns the first failed component of B + Q + K <= cap.