Mathematical Solvency Proof
This is the formal solvency proof for the PGM Raise Contract (PGMRaise). It proves that the redeem mechanism is solvent at all reachable states.
============================================================================
POST-FINALIZE REDEEM SOLVENCY + EXECUTABLE CORRESPONDENCE PROOF
============================================================================
TYPE OF PROOF
----------------------------------------------------------------------------
This is a strengthened economic-operational proof for the raise-contract in
post-finalize states.
It proves:
(1) SOLVENCY:
total redeem backing is always at least total outstanding redeem claims
(2) EXACT EXECUTABLE CORRESPONDENCE OF COUNTED LP BACKING:
every unit counted as LP-backed redeem capacity is defined by exact
correspondence to the concrete executable redeem() LP-settlement path
of the deployed CL implementation
(3) REDEEM EXECUTABILITY RELATIVE TO THE VERIFIED CL SEMANTICS:
the LP-backed portion counted by the proof is not merely theoretical;
it is realizable by the exact redeem() runtime path under the verified
deployed CL semantics
This is NOT a storage-complete formal proof derived purely from the raise-contract
state alone. It is a proof relative to the verified external concentrated-
liquidity (CL) implementation used by the raise-contract.
----------------------------------------------------------------------------
CLAIM
----------------------------------------------------------------------------
For all reachable post-finalize states:
total redeem backing >= total outstanding redeem claims
where total redeem backing consists of:
- reserve backing R
- executable principal-only LP settlement capacity K
and outstanding redeem claims are measured by C.
Hence:
R + K >= C
and redeem() is solvent in all reachable post-finalize states, conditional
on the assumptions below.
This proves solvency and executable correspondence of the counted LP-backed
portion. It does not claim arbitrary external-call liveness beyond the
verified CL semantics explicitly assumed herein.
============================================================================
NOTATION
============================================================================
Let:
P := PGM_PER_USDT
R := buybackReserve
C := total outstanding redeem claim mass, measured in redeem-USDT units
K := executable principal-only LP settlement capacity of the locked upside
position, measured in redeem-USDT units
"redeem-USDT units" means the amount of USDT guaranteed by PGMRaise.redeem()
at rate P. It is NOT market price.
============================================================================
EXACT DEFINITIONS
============================================================================
---------------------------------------------------------------------------
D1) Exact claim-mass definition of C
---------------------------------------------------------------------------
C is defined as the total redeem-USDT-unit obligation of all currently
outstanding redeemable PGM claims in all custody forms, including:
- unclaimed allocations
- claimed redeemable PGM externally held by users or contracts
- LP-origin PGM once externalized by buys
- any other externally circulating redeemable PGM claim mass
C excludes:
- burned PGM
- non-externalized locked LP principal
- fee-custody-only balances that do not represent new guaranteed redeem
obligations
Moreover, every reachable state transition in the raise-contract and in the referenced
CL system preserves this definition exactly, with no unclassified custody
state and no token balance that can contribute to guaranteed redeem output
while being excluded from both C and K.
---------------------------------------------------------------------------
D2) Exact executable definition of K
---------------------------------------------------------------------------
K is NOT a stored raise-contract state variable.
K is a proof quantity only.
For every reachable post-finalize pool state s, let:
ExecRedeemLP(s, q)
be the actual USDT output produced by the deployed pool implementation when
PGMRaise.redeem() executes its LP-settlement branch with redeemable PGM input
corresponding to q redeem-USDT units, using the exact runtime parameters:
zeroForOne = false
sqrtPriceLimitX96 = SQRT_PRICE_REDEEM_LIMIT
and counting only principal-backed settlement from the locked upside
position, excluding fee-custody-only balances.
Then K(s) is defined to be exactly the maximum redeem-USDT-unit amount
realizable by that concrete executable path from the locked upside
position’s principal-only backing.
Therefore K is not merely an economic abstraction.
It is exactly the executable redeem-path settlement capacity of the deployed
CL implementation, principal-only and fee-excluding.
---------------------------------------------------------------------------
D3) Exact custody partition
---------------------------------------------------------------------------
Every token state reachable in the locked upside position belongs to exactly
one of the following mutually exclusive classes:
(1) redeem-claim mass contributing to C
(2) executable principal-only LP settlement capacity contributing to K
(3) fee-custody-only balances contributing to neither C nor K
(4) inert non-externalized locked principal contributing to neither current
external claim mass nor fee custody
This partition is exhaustive and has no remainder bucket.
All reachable transitions preserve this partition exactly.
============================================================================
ASSUMPTIONS
============================================================================
---------------------------------------------------------------------------
A1) Correctness of deployed CL implementation
---------------------------------------------------------------------------
The deployed external CL pool / factory / position-manager implementation
used by the raise-contract behaves according to the verified CL semantics under the
relevant swap, price-limit, fee, liquidity, and tick-accounting rules.
In particular:
- swap() enforces directional price-limit checks
- swap() traverses price monotonically until either input is exhausted or
the price limit is reached
- tick crossings update active liquidity deterministically
- fee accounting behaves according to the verified deployed CL system
This proof does not re-prove the external CL implementation.
It is conditional on A1.
---------------------------------------------------------------------------
A2) Exact executable interpretation of K
---------------------------------------------------------------------------
K is defined by exact correspondence to the deployed CL implementation’s
executable redeem() LP-settlement path, not by heuristic economic
approximation.
Every unit counted in K is counted only because it is principal-only,
fee-excluding, and executable by the exact redeem() LP path of the deployed
CL implementation.
---------------------------------------------------------------------------
A3) Exact custody classification
---------------------------------------------------------------------------
The partition in D3 is exact for all reachable post-finalize states.
In particular:
- no unit excluded from C can later require guaranteed redeem output
without first entering C by a modeled transition
- no unit excluded from K can contribute executable principal-only LP
settlement capacity without first entering K by a modeled transition
- fee-custody-only balances never silently constitute guaranteed redeem
obligations
---------------------------------------------------------------------------
CL-D) Redeem-path non-reverting executability, under A1/A2
---------------------------------------------------------------------------
For every reachable post-finalize state in which redeem() enters its
LP-settlement branch, the call
IPool(pool).swap(
address(this),
false,
int256(pgmForFloor),
SQRT_PRICE_REDEEM_LIMIT,
""
)
does not revert for any reason other than insufficient redeem input, and
executes to completion according to the verified semantics of the deployed
CL implementation.
Therefore, whenever LP-backed settlement capacity is counted in K, that
capacity is not merely theoretical but executable by the actual redeem()
runtime path.
============================================================================
INITIAL STATE
============================================================================
Immediately after finalize():
- all outstanding investor redeem claims are reserve-backed
- no LP-origin external redeem claims yet exist
- the locked upside LP contains inert PGM principal only
- fee-custody-only balances are excluded from both C and K
Therefore:
K = 0
R = C
Hence:
R + K = C
So the invariant holds initially.
============================================================================
IMPORTED CL FACTS
============================================================================
---------------------------------------------------------------------------
CL-A) Externalization by buy
---------------------------------------------------------------------------
Buying PGM out of the locked upside LP converts locked principal into
externally circulating redeem claims one-for-one in NET redeem-USDT units,
excluding fee-custody-only movement.
Therefore, if a buy externalizes x NET redeem-USDT units of claim mass:
dC = +x
dK = +x
dR = 0
---------------------------------------------------------------------------
CL-B) Re-internalization by sell
---------------------------------------------------------------------------
Selling redeemable PGM into the locked upside LP along the exact reverse path
used by redeem() converts externally circulating redeem claims back into
executable principal-only LP settlement capacity one-for-one in NET
redeem-USDT units, excluding fee-custody-only movement.
Therefore, if a sell re-internalizes x NET redeem-USDT units:
dC = -x
dK = -x
dR = 0
---------------------------------------------------------------------------
CL-C) Exact redeem-path settlement correspondence
---------------------------------------------------------------------------
The locked upside position is minted below the initial pool price and starts
fully on the PGM side.
Therefore its initial executable principal-only redeem settlement capacity is
zero.
Any subsequent buy from the locked upside LP injects principal-backed USDT
into that same locked position, and by D2/A2 this injected principal is
exactly what later contributes to K.
Whenever redeem() enters its LP branch, it executes the concrete reverse path
bounded by SQRT_PRICE_REDEEM_LIMIT:
swap(..., zeroForOne = false, sqrtPriceLimitX96 = SQRT_PRICE_REDEEM_LIMIT)
Under A1/A2/CL-D, every unit counted in K is realizable along that exact path.
============================================================================
LEMMAS
============================================================================
---------------------------------------------------------------------------
L1) Buy from locked upside LP
---------------------------------------------------------------------------
If a trade buys x NET redeem-USDT units of PGM out of the locked upside LP,
excluding fee-custody-only movement, then:
dC = +x
dK = +x
dR = 0
Proof:
By CL-A and D2, the buy externalizes x of claim mass and injects exactly x
of executable principal-only LP settlement capacity into the locked upside
position. Reserve is untouched. End.
---------------------------------------------------------------------------
L2) Sell into locked upside LP
---------------------------------------------------------------------------
If a trade sells x NET redeem-USDT units of redeemable PGM into the locked
upside LP along the exact reverse path used by redeem(), excluding
fee-custody-only movement, then:
dC = -x
dK = -x
dR = 0
Proof:
By CL-B and D2, the sell removes x from external claim mass and consumes
exactly x of executable principal-only LP settlement capacity. Reserve is
untouched. End.
---------------------------------------------------------------------------
L3) Redeem settles claims
---------------------------------------------------------------------------
Let:
x := total redeem amount in redeem-USDT units
x_lp := LP-settled portion
x_r := reserve-settled portion
Then:
x = x_lp + x_r
and:
dC = -x
d(R + K) = -x
Proof:
By CL-C and CL-D, the LP-backed portion x_lp counted in K is executable by
the exact redeem() LP path and settles x_lp claim mass, so:
dC_lp = -x_lp
dK = -x_lp
The reserve-backed portion x_r settles the remainder, so:
dC_r = -x_r
dR = -x_r
Summing:
dC = -(x_lp + x_r) = -x
d(R + K) = -(x_lp + x_r) = -x
Any LP surplus forwarded externally is excluded from both C and K by D3,
hence does not affect the invariant. End.
---------------------------------------------------------------------------
L4) Fee neutrality under exact custody partition
---------------------------------------------------------------------------
Let pool-held balances be partitioned into:
(i) locked principal backing relevant to redeem settlement
(ii) fee-custody-only balances collectible via collect()
The quantity K includes only (i) and excludes (ii) by exact correspondence
to executable principal-only redeem settlement under D2/A2.
The quantity C excludes fee-custody-only balances because such balances do
not represent newly created redeem claims and do not increase outstanding
guaranteed redeem obligations.
Fee generation only reassigns token custody inside the pool between
principal and fee buckets according to the verified CL accounting rules,
without increasing total outstanding redeem claims.
Fee collection via collectTradingFees() transfers only bucket (ii), which is
excluded from both C and K before and after collection.
Therefore fee generation and fee collection satisfy:
dC = 0
dK = 0
dR = 0
---------------------------------------------------------------------------
L5) External transfers unrelated to executable LP backing
---------------------------------------------------------------------------
Any ERC20 transfer or trade not involving class-(2) executable principal-only
LP settlement capacity changes only custody of already-classified balances
and therefore satisfies:
dC = 0
dK = 0
dR = 0
---------------------------------------------------------------------------
L6) Redeem total liveness, relative to A1/A2/CL-D
---------------------------------------------------------------------------
For every reachable post-finalize state and every valid redeem amount,
redeem() either:
(a) settles entirely from reserve, or
(b) settles partially from LP and the remainder from reserve,
and does not revert provided:
- the invariant R + K >= C holds
- the pool implementation satisfies A1/A2/CL-D
- the redeem input is valid under the raise-contract’s own checks
Proof:
If the LP branch is not entered, redeem settles from reserve only.
If the LP branch is entered, then by CL-D the concrete swap path executes,
and by L3 the LP-settled portion plus reserve remainder exactly settle the
redeem amount. Therefore no additional revert source exists beyond failure of
the stated assumptions or invalid user input. End.
============================================================================
TRANSITIONS
============================================================================
Claim / external custody movement:
no net change in R, K, C
Sacrifice(x):
dC = -x
dR = -x
Buy from locked upside LP:
by L1
Sell into locked upside LP:
by L2
Redeem:
by L3 and L6
Fees:
by L4
Other external transfers:
by L5
Therefore all reachable post-finalize transitions preserve:
R + K >= C
============================================================================
SMOKE TEST SCOPE NOTE
============================================================================
The smoke tests and scenario tests validate representative execution paths
against the deployed CL system, including finalize, claim, redeem, LP buy,
and selected edge/boundary cases.
They are implementation-consistency checks against the intended model.
They are NOT by themselves a proof of all reachable states.
Completeness of solvency is provided by the economic-operational proof above;
the smoke/scenario tests serve only as evidence that selected concrete paths
match the intended model and deployed integration.
============================================================================
META-CLAIM
============================================================================
Under A1, the quantities C and K are defined by exact correspondence to the
deployed CL implementation’s executable accounting and swap semantics, not by
heuristic economic approximation.
Every token state reachable in the locked upside position belongs to exactly
one of the following mutually exclusive classes:
(1) redeem-claim mass contributing to C
(2) executable principal-only LP settlement capacity contributing to K
(3) fee-custody-only balances contributing to neither C nor K
(4) inert non-externalized locked principal contributing to neither current
external claim mass nor fee custody
All reachable transitions preserve this partition exactly.
Furthermore, every unit counted in K is executable by the concrete redeem()
pool-swap path without revert under the verified deployed CL semantics.
Therefore the invariant
R + K >= C
is both economically exact and operationally realizable for all reachable
post-finalize states, subject to A1/A2/A3/CL-D.
============================================================================
CONCLUSION
====================101=====================================================
The invariant
R + K >= C
holds initially at finalize() and is preserved by all reachable post-finalize
transitions under A1/A2/A3/CL-D.
Therefore:
total redeem backing >= total outstanding redeem claims
and the LP-backed portion counted by the proof is exactly the executable
principal-only redeem-path settlement capacity of the deployed CL
implementation.
Hence redeem() is solvent in all reachable post-finalize states, and the
counted LP-backed portion is operationally realizable along the exact
redeem() runtime path, conditional on the stated assumptions.
QED
============================================================================