From 963d893c3777f9cdb84b575a3b41d96bfd9302d7 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 5 Jun 2026 20:35:01 +0200 Subject: [PATCH 01/10] add rocq proof --- .gitignore | 1 + rocq/maxRepaidHealthy.v | 320 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 321 insertions(+) create mode 100644 rocq/maxRepaidHealthy.v diff --git a/.gitignore b/.gitignore index 5280472af..3b7243426 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ cache out .certora_internal +.*.cache diff --git a/rocq/maxRepaidHealthy.v b/rocq/maxRepaidHealthy.v new file mode 100644 index 000000000..e6e7523e0 --- /dev/null +++ b/rocq/maxRepaidHealthy.v @@ -0,0 +1,320 @@ +From Stdlib Require Import ZArith Lia Psatz. + +Open Scope Z_scope. + +Definition WAD : Z := 1000000000000000000. +Definition ORACLE_PRICE_SCALE : Z := 1000000000000000000000000000000000000. + +Definition ceil_div (numerator denominator : Z) : Z := + (numerator + denominator - 1) / denominator. + +(** +If: +- maxRepaid is computed as: + ceil((debt - maxDebt) * WAD^2 / (WAD^2 - lif * lltv)) +- seizedAssets is computed as: + floor(floor(maxRepaid * lif / WAD) * ORACLE_PRICE_SCALE / price) +- maxDebt is computed from the current collateral as: + otherCollatContribution + floor(floor(collat * price / ORACLE_PRICE_SCALE) * lltv / WAD) + +then after liquidating maxRepaid, the borrower is healthy: + newDebt <= newMaxDebt + +This proof is entirely over integer arithmetic. +It does not use real-number approximations. +The assumptions that the collateral seized does not exceed the current collateral does not narrow the generality of the proof: in that case the transaction would revert independently of the RCF mechanism, so that mechanism does not restrict the possibility to go back to health. +*) + +Definition max_repaid_liquidation_leaves_healthy_statement : Prop := + forall debt maxDebt otherCollatContribution collat seizedAssets price lltv lif maxRepaid, + 0 < price -> + 0 <= debt -> 0 <= otherCollatContribution -> + 0 <= collat -> 0 <= seizedAssets -> seizedAssets <= collat -> + 0 <= lltv -> 0 <= lif -> + lif * lltv < WAD * WAD -> + maxDebt = + otherCollatContribution + + (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD -> + seizedAssets = + (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> + maxRepaid = + ceil_div ((debt - maxDebt) * (WAD * WAD)) + (WAD * WAD - lif * lltv) -> + maxDebt <= debt -> + let newDebt := debt - maxRepaid in + let newMaxDebt := + otherCollatContribution + + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD + in + newDebt <= newMaxDebt. + +(* -------------------------------------------------------------------------- *) +(* Generic integer-division lemmas *) +(* -------------------------------------------------------------------------- *) + +Lemma WAD_pos : 0 < WAD. +Proof. unfold WAD; lia. Qed. + +Lemma ORACLE_PRICE_SCALE_pos : 0 < ORACLE_PRICE_SCALE. +Proof. unfold ORACLE_PRICE_SCALE; lia. Qed. + +Lemma div_upper_strict : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + numerator < denominator * (numerator / denominator + 1). +Proof. + intros numerator denominator Hden Hnum. + pose proof (Z.div_mod numerator denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. + nia. +Qed. + +Lemma floor_mul_le : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + (numerator / denominator) * denominator <= numerator. +Proof. + intros numerator denominator Hden Hnum. + pose proof (Z.div_mod numerator denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound numerator denominator Hden) as Hmod. + nia. +Qed. + +Lemma ceil_div_mul_ge : + forall numerator denominator, + 0 < denominator -> 0 <= numerator -> + numerator <= ceil_div numerator denominator * denominator. +Proof. + intros numerator denominator Hden Hnum. + unfold ceil_div. + pose proof (Z.div_mod (numerator + denominator - 1) denominator) as Hdivmod. + specialize (Hdivmod ltac:(lia)). + pose proof (Z.mod_pos_bound (numerator + denominator - 1) denominator Hden) as Hmod. + nia. +Qed. + +Lemma ceil_div_le_of_mul_ge : + forall numerator denominator bound, + 0 < denominator -> 0 <= numerator -> numerator <= bound * denominator -> + ceil_div numerator denominator <= bound. +Proof. + intros numerator denominator bound Hden Hnum Hbound. + unfold ceil_div. + assert ((numerator + denominator - 1) / denominator < bound + 1) as Hlt. + { apply Z.div_lt_upper_bound; nia. } + lia. +Qed. + +Lemma ceil_div_mono : + forall left right denominator, + 0 < denominator -> left <= right -> + ceil_div left denominator <= ceil_div right denominator. +Proof. + intros left right denominator Hden Hle. + unfold ceil_div. + apply Z.div_le_mono; lia. +Qed. + +Lemma floor_drop_div_le_ceil : + forall base drop denominator, + 0 < denominator -> 0 <= base -> 0 <= drop -> + (base + drop) / denominator - base / denominator <= ceil_div drop denominator. +Proof. + intros base drop denominator Hden Hbase Hdrop. + assert (Hbase_lt : base < denominator * (base / denominator + 1)). + { apply div_upper_strict; lia. } + assert (Hdrop_le : drop <= ceil_div drop denominator * denominator). + { apply ceil_div_mul_ge; lia. } + assert ((base + drop) / denominator < base / denominator + ceil_div drop denominator + 1) as Hlt. + { apply Z.div_lt_upper_bound; nia. } + lia. +Qed. + +(* -------------------------------------------------------------------------- *) +(* Midnight-specific rounding lemmas *) +(* -------------------------------------------------------------------------- *) + +Lemma seized_value_drop_le_maxSeizedValue : + forall maxRepaid lif price seizedAssets, + 0 < price -> + 0 <= maxRepaid -> 0 <= lif -> + seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> + ceil_div (seizedAssets * price) ORACLE_PRICE_SCALE <= maxRepaid * lif / WAD. +Proof. + intros maxRepaid lif price seizedAssets Hprice HmaxRepaid Hlif Hseized. + subst seizedAssets. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + assert (HmaxSeizedValue_nonneg : 0 <= maxRepaid * lif / WAD). + { apply Z.div_pos; nia. } + apply ceil_div_le_of_mul_ge. + - exact Hscale. + - apply Z.mul_nonneg_nonneg; [apply Z.div_pos |]; nia. + - pose proof (floor_mul_le (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) price Hprice) as Hfloor. + specialize (Hfloor ltac:(nia)). + nia. +Qed. + +Lemma max_debt_contribution_drop_bound : + forall collat seizedAssets price lltv maxRepaid lif, + 0 < price -> + 0 <= collat -> 0 <= seizedAssets -> seizedAssets <= collat -> + 0 <= lltv -> 0 <= maxRepaid -> 0 <= lif -> + seizedAssets = (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> + let currentCollatValue := collat * price / ORACLE_PRICE_SCALE in + let newCollatValue := (collat - seizedAssets) * price / ORACLE_PRICE_SCALE in + currentCollatValue * lltv / WAD - newCollatValue * lltv / WAD + <= ceil_div (maxRepaid * lif * lltv) (WAD * WAD). +Proof. + intros collat seizedAssets price lltv maxRepaid lif + Hprice Hcollat HseizedNonneg HseizedLe Hlltv HmaxRepaid Hlif HseizedEq + currentCollatValue newCollatValue. + subst currentCollatValue newCollatValue. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + + set (collatValueDrop := + collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). + set (maxSeizedValue := maxRepaid * lif / WAD). + set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). + + assert (HcollatValueDrop_le : collatValueDrop <= maxSeizedValue). + { + unfold collatValueDrop, maxSeizedValue. + replace (collat * price) + with ((collat - seizedAssets) * price + seizedAssets * price) by nia. + eapply Z.le_trans. + - apply floor_drop_div_le_ceil; nia. + - eapply seized_value_drop_le_maxSeizedValue; eauto; nia. + } + + assert (Hold_ge_new_value : + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE <= collat * price / ORACLE_PRICE_SCALE). + { + apply Z.div_le_mono; nia. + } + + assert (HmaxDebtDrop_by_valueDrop : + collat * price / ORACLE_PRICE_SCALE * lltv / WAD + - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD + <= ceil_div (collatValueDrop * lltv) WAD). + { + unfold collatValueDrop. + replace (collat * price / ORACLE_PRICE_SCALE * lltv) + with (((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv + + (collat * price / ORACLE_PRICE_SCALE - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv) by nia. + eapply floor_drop_div_le_ceil. + - exact HWAD. + - apply Z.mul_nonneg_nonneg; try nia. + apply Z.div_pos; nia. + - apply Z.mul_nonneg_nonneg; nia. + } + + assert (Hceil_valueDrop_le_maxSeizedValue : + ceil_div (collatValueDrop * lltv) WAD <= ceil_div (maxSeizedValue * lltv) WAD). + { + apply ceil_div_mono; nia. + } + + assert (HmaxSeizedValue_floor : maxSeizedValue * WAD <= maxRepaid * lif). + { + unfold maxSeizedValue. + apply floor_mul_le; nia. + } + + assert (HmaxDebtDropBound_mul : maxRepaid * lif * lltv <= maxDebtDropBound * (WAD * WAD)). + { + unfold maxDebtDropBound. + apply ceil_div_mul_ge; nia. + } + + assert (HmaxSeizedValue_to_maxDebtDropBound : maxSeizedValue * lltv <= maxDebtDropBound * WAD). + { + nia. + } + + assert (Hceil_maxSeizedValue_le_maxDebtDropBound : + ceil_div (maxSeizedValue * lltv) WAD <= maxDebtDropBound). + { + apply ceil_div_le_of_mul_ge; nia. + } + + lia. +Qed. + +(* -------------------------------------------------------------------------- *) +(* Final theorem *) +(* -------------------------------------------------------------------------- *) + +Theorem max_repaid_liquidation_leaves_healthy : + max_repaid_liquidation_leaves_healthy_statement. +Proof. + unfold max_repaid_liquidation_leaves_healthy_statement. + intros debt maxDebt otherCollatContribution collat seizedAssets price lltv lif maxRepaid + Hprice Hdebt Hother Hcollat HseizedNonneg HseizedLe Hlltv Hlif + Hden HmaxDebtEq HseizedEq HmaxRepaidEq HgapNonneg. + assert (HWAD : 0 < WAD) by apply WAD_pos. + assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. + + assert (HmaxDebt : 0 <= maxDebt). + { + rewrite HmaxDebtEq. + assert (HcollatValue_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE). + { apply Z.div_pos; nia. } + assert (HcollatContribution_nonneg : + 0 <= (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD). + { apply Z.div_pos; nia. } + nia. + } + + set (gap := debt - maxDebt). + set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). + + assert (Hgap_nonneg : 0 <= gap) by (unfold gap; lia). + assert (Hden_pos : 0 < WAD * WAD - lif * lltv) by nia. + + assert (HmaxRepaid : 0 <= maxRepaid). + { + rewrite HmaxRepaidEq. + unfold ceil_div. + apply Z.div_pos; nia. + } + + assert (HmaxRepaid_def_le : + gap * (WAD * WAD) <= maxRepaid * (WAD * WAD - lif * lltv)). + { + rewrite HmaxRepaidEq. + unfold gap. + apply ceil_div_mul_ge; nia. + } + + assert (Hextra_mul : + (maxRepaid - gap) * (WAD * WAD) >= maxRepaid * lif * lltv). + { + nia. + } + + assert (HmaxDebtDropBound_le_extra : maxDebtDropBound <= maxRepaid - gap). + { + unfold maxDebtDropBound. + apply ceil_div_le_of_mul_ge; nia. + } + + assert (HmaxDebtDrop_le_bound : maxDebt - + (otherCollatContribution + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD) + <= maxDebtDropBound). + { + rewrite HmaxDebtEq. + replace (otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD)) + with (collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD) by lia. + unfold maxDebtDropBound. + eapply max_debt_contribution_drop_bound; eauto; nia. + } + + unfold gap in *. + lia. +Qed. From 4a33783de0cef4b6b181b26df27c9daa3cd8f3c9 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 11:01:36 +0200 Subject: [PATCH 02/10] include actual repaid amount --- rocq/maxRepaidHealthy.v | 180 +++++++++++++++++++++++++--------------- 1 file changed, 113 insertions(+), 67 deletions(-) diff --git a/rocq/maxRepaidHealthy.v b/rocq/maxRepaidHealthy.v index e6e7523e0..273b6a77c 100644 --- a/rocq/maxRepaidHealthy.v +++ b/rocq/maxRepaidHealthy.v @@ -12,12 +12,13 @@ Definition ceil_div (numerator denominator : Z) : Z := If: - maxRepaid is computed as: ceil((debt - maxDebt) * WAD^2 / (WAD^2 - lif * lltv)) +- repaid is the amount actually repaid: min(maxRepaid, debt) - seizedAssets is computed as: - floor(floor(maxRepaid * lif / WAD) * ORACLE_PRICE_SCALE / price) + floor(floor(repaid * lif / WAD) * ORACLE_PRICE_SCALE / price) - maxDebt is computed from the current collateral as: otherCollatContribution + floor(floor(collat * price / ORACLE_PRICE_SCALE) * lltv / WAD) -then after liquidating maxRepaid, the borrower is healthy: +then after liquidating repaid, the borrower is healthy: newDebt <= newMaxDebt This proof is entirely over integer arithmetic. @@ -26,27 +27,28 @@ The assumptions that the collateral seized does not exceed the current collatera *) Definition max_repaid_liquidation_leaves_healthy_statement : Prop := - forall debt maxDebt otherCollatContribution collat seizedAssets price lltv lif maxRepaid, + forall debt otherCollatContribution collat price lltv lif, + let maxDebt := + otherCollatContribution + + (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD in + let maxRepaid := + ceil_div ((debt - maxDebt) * (WAD * WAD)) + (WAD * WAD - lif * lltv) in + let repaid := Z.min maxRepaid debt in + let seizedAssets := + (repaid * lif / WAD * ORACLE_PRICE_SCALE) / price in + let newDebt := debt - repaid in + let newMaxDebt := + otherCollatContribution + + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD in 0 < price -> 0 <= debt -> 0 <= otherCollatContribution -> - 0 <= collat -> 0 <= seizedAssets -> seizedAssets <= collat -> + 0 <= collat -> 0 <= lltv -> 0 <= lif -> lif * lltv < WAD * WAD -> - maxDebt = - otherCollatContribution - + (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD -> - seizedAssets = - (maxRepaid * lif / WAD * ORACLE_PRICE_SCALE) / price -> - maxRepaid = - ceil_div ((debt - maxDebt) * (WAD * WAD)) - (WAD * WAD - lif * lltv) -> maxDebt <= debt -> - let newDebt := debt - maxRepaid in - let newMaxDebt := - otherCollatContribution - + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD - in - newDebt <= newMaxDebt. + seizedAssets <= collat -> + 0 <= newDebt /\ newDebt <= newMaxDebt. (* -------------------------------------------------------------------------- *) (* Generic integer-division lemmas *) @@ -252,69 +254,113 @@ Theorem max_repaid_liquidation_leaves_healthy : max_repaid_liquidation_leaves_healthy_statement. Proof. unfold max_repaid_liquidation_leaves_healthy_statement. - intros debt maxDebt otherCollatContribution collat seizedAssets price lltv lif maxRepaid - Hprice Hdebt Hother Hcollat HseizedNonneg HseizedLe Hlltv Hlif - Hden HmaxDebtEq HseizedEq HmaxRepaidEq HgapNonneg. + intros debt otherCollatContribution collat price lltv lif. + set (maxDebt := otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD). + set (maxRepaid := ceil_div ((debt - maxDebt) * (WAD * WAD)) (WAD * WAD - lif * lltv)). + set (repaid := Z.min maxRepaid debt). + set (seizedAssets := repaid * lif / WAD * ORACLE_PRICE_SCALE / price). + set (newDebt := debt - repaid). + set (newMaxDebt := otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). + intros Hprice Hdebt Hother Hcollat Hlltv Hlif Hden HmaxDebtLeDebt HseizedLeCollat. assert (HWAD : 0 < WAD) by apply WAD_pos. assert (Hscale : 0 < ORACLE_PRICE_SCALE) by apply ORACLE_PRICE_SCALE_pos. - - assert (HmaxDebt : 0 <= maxDebt). + assert (Hden_pos : 0 < WAD * WAD - lif * lltv) by nia. + assert (HmaxDebt_nonneg : 0 <= maxDebt). { - rewrite HmaxDebtEq. + subst maxDebt. assert (HcollatValue_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE). { apply Z.div_pos; nia. } - assert (HcollatContribution_nonneg : - 0 <= (collat * price / ORACLE_PRICE_SCALE) * lltv / WAD). + assert (HcollatContribution_nonneg : 0 <= collat * price / ORACLE_PRICE_SCALE * lltv / WAD). { apply Z.div_pos; nia. } nia. } - - set (gap := debt - maxDebt). - set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). - - assert (Hgap_nonneg : 0 <= gap) by (unfold gap; lia). - assert (Hden_pos : 0 < WAD * WAD - lif * lltv) by nia. - - assert (HmaxRepaid : 0 <= maxRepaid). + assert (HmaxRepaid_nonneg : 0 <= maxRepaid). { - rewrite HmaxRepaidEq. + subst maxRepaid. unfold ceil_div. apply Z.div_pos; nia. } - - assert (HmaxRepaid_def_le : - gap * (WAD * WAD) <= maxRepaid * (WAD * WAD - lif * lltv)). + assert (Hrepaid_nonneg : 0 <= repaid). { - rewrite HmaxRepaidEq. - unfold gap. - apply ceil_div_mul_ge; nia. + subst repaid. + apply Z.min_glb; assumption. } - - assert (Hextra_mul : - (maxRepaid - gap) * (WAD * WAD) >= maxRepaid * lif * lltv). + assert (Hrepaid_le_debt : repaid <= debt). { - nia. + subst repaid. + apply Z.le_min_r. } - - assert (HmaxDebtDropBound_le_extra : maxDebtDropBound <= maxRepaid - gap). - { - unfold maxDebtDropBound. - apply ceil_div_le_of_mul_ge; nia. - } - - assert (HmaxDebtDrop_le_bound : maxDebt - - (otherCollatContribution + ((collat - seizedAssets) * price / ORACLE_PRICE_SCALE) * lltv / WAD) - <= maxDebtDropBound). - { - rewrite HmaxDebtEq. - replace (otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD - - (otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD)) - with (collat * price / ORACLE_PRICE_SCALE * lltv / WAD - - (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD) by lia. - unfold maxDebtDropBound. - eapply max_debt_contribution_drop_bound; eauto; nia. - } - - unfold gap in *. - lia. + split. + - subst newDebt; lia. + - destruct (Z.leb_spec0 debt maxRepaid) as [Hdebt_le_maxRepaid | HmaxRepaid_lt_debt]. + + assert (Hrepaid_eq : repaid = debt). + { subst repaid. apply Z.min_r. lia. } + subst newDebt newMaxDebt. + rewrite Hrepaid_eq. + assert (Hseized_nonneg : 0 <= seizedAssets). + { + subst seizedAssets. + rewrite Hrepaid_eq. + apply Z.div_pos. + - apply Z.mul_nonneg_nonneg. + + apply Z.div_pos; nia. + + lia. + - lia. + } + assert (HnewCollatValue_nonneg : 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE). + { apply Z.div_pos; nia. } + assert (HnewContribution_nonneg : + 0 <= (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD). + { apply Z.div_pos; nia. } + nia. + + assert (Hrepaid_eq : repaid = maxRepaid). + { subst repaid. apply Z.min_l. lia. } + set (gap := debt - maxDebt). + set (maxDebtDropBound := ceil_div (maxRepaid * lif * lltv) (WAD * WAD)). + assert (Hgap_nonneg : 0 <= gap) by (unfold gap; lia). + assert (HmaxRepaid_def_le : + gap * (WAD * WAD) <= maxRepaid * (WAD * WAD - lif * lltv)). + { + subst maxRepaid. + unfold gap. + apply ceil_div_mul_ge; nia. + } + assert (Hextra_mul : + (maxRepaid - gap) * (WAD * WAD) >= maxRepaid * lif * lltv). + { nia. } + assert (HmaxDebtDropBound_le_extra : maxDebtDropBound <= maxRepaid - gap). + { + unfold maxDebtDropBound. + apply ceil_div_le_of_mul_ge; nia. + } + assert (Hseized_nonneg : 0 <= seizedAssets). + { + subst seizedAssets. + rewrite Hrepaid_eq. + apply Z.div_pos. + - apply Z.mul_nonneg_nonneg. + + apply Z.div_pos; nia. + + lia. + - lia. + } + assert (HseizedEq : seizedAssets = maxRepaid * lif / WAD * ORACLE_PRICE_SCALE / price). + { + subst seizedAssets. + rewrite Hrepaid_eq. + reflexivity. + } + assert (HmaxDebtDrop_le_bound : maxDebt - newMaxDebt <= maxDebtDropBound). + { + subst maxDebt newMaxDebt. + replace (otherCollatContribution + collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (otherCollatContribution + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD)) + with (collat * price / ORACLE_PRICE_SCALE * lltv / WAD - + (collat - seizedAssets) * price / ORACLE_PRICE_SCALE * lltv / WAD) by lia. + unfold maxDebtDropBound. + eapply max_debt_contribution_drop_bound; eauto; nia. + } + subst newDebt. + rewrite Hrepaid_eq. + unfold gap in *. + lia. Qed. From 6c4eb39ec4c1c6af772f7b05947d3e30d0f318a7 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 13:38:53 +0200 Subject: [PATCH 03/10] add ci --- .github/workflows/rocq.yml | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 .github/workflows/rocq.yml diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml new file mode 100644 index 000000000..eed4b53bf --- /dev/null +++ b/.github/workflows/rocq.yml @@ -0,0 +1,27 @@ +name: rocq + +on: + push: + branches: + - main + pull_request: + workflow_dispatch: + +jobs: + prove: + runs-on: ubuntu-latest + container: rocq/rocq-prover:9.1 + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + + - name: Check proofs and assumptions + run: | + # Assume .v files are independent. + # Do not check admits in the module's dependencies. + for file in rocq/*.v; do + rocq compile "$file" + module="$(basename "$file" .v)" + if rocq check -silent --output-context "rocq/$module.vo" 2>&1 | grep -F " $module."; then + exit 1 + fi + done From 1a3c44d7627ed8310d07d7cc53cd24578cf70f97 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 13:51:29 +0200 Subject: [PATCH 04/10] ci: write in an allowed place --- .github/workflows/rocq.yml | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index eed4b53bf..54f10170b 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -10,18 +10,20 @@ on: jobs: prove: runs-on: ubuntu-latest - container: rocq/rocq-prover:9.1 steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 - - name: Check proofs and assumptions - run: | - # Assume .v files are independent. - # Do not check admits in the module's dependencies. - for file in rocq/*.v; do - rocq compile "$file" - module="$(basename "$file" .v)" - if rocq check -silent --output-context "rocq/$module.vo" 2>&1 | grep -F " $module."; then - exit 1 - fi - done + - uses: rocq-prover/docker-opam-action@126d4ac196f8133729a1cb0d2aa1ee7106efec58 # v1.5.2 + with: + custom_image: rocq/rocq-prover:9.1 + custom_script: | + mkdir -p /tmp/rocq + # Assume .v files are independent. + # Do not check admits in the module's dependencies. + for file in rocq/*.v; do + module="$(basename "$file" .v)" + rocq compile -noglob -o "/tmp/rocq/$module.vo" "$file" + if rocq check -silent --output-context "/tmp/rocq/$module.vo" 2>&1 | grep -F " $module."; then + exit 1 + fi + done From 6ed8cf8dc314418d8a085667713621b41cb80aff Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 14:01:21 +0200 Subject: [PATCH 05/10] fix edge case in ci --- .github/workflows/rocq.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 54f10170b..9fcbb321e 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -17,13 +17,13 @@ jobs: with: custom_image: rocq/rocq-prover:9.1 custom_script: | - mkdir -p /tmp/rocq # Assume .v files are independent. # Do not check admits in the module's dependencies. for file in rocq/*.v; do module="$(basename "$file" .v)" - rocq compile -noglob -o "/tmp/rocq/$module.vo" "$file" - if rocq check -silent --output-context "/tmp/rocq/$module.vo" 2>&1 | grep -F " $module."; then + rocq compile -o "/tmp/$module.vo" "$file" + output="$(rocq check -silent --output-context "/tmp/$module.vo" 2>&1)" + if printf '%s\n' "$output" | grep -F " $module."; then exit 1 fi done From 9075cb96a6d6419a58ad3eec26f69f8782114500 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 14:08:59 +0200 Subject: [PATCH 06/10] try direct docker --- .github/workflows/rocq.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 9fcbb321e..498128f0f 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -13,12 +13,11 @@ jobs: steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 - - uses: rocq-prover/docker-opam-action@126d4ac196f8133729a1cb0d2aa1ee7106efec58 # v1.5.2 - with: - custom_image: rocq/rocq-prover:9.1 - custom_script: | + - name: Check proofs and assumptions + run: | + docker run --rm -v "$PWD:$PWD" -w "$PWD" rocq/rocq-prover@sha256:b85a80a11bb65c7c843f91c7cbcce282f22ee397c9ca42f123d568ab6cef68b0 sh -lc ' # Assume .v files are independent. - # Do not check admits in the module's dependencies. + # Do not check admits in the module'\''s dependencies. for file in rocq/*.v; do module="$(basename "$file" .v)" rocq compile -o "/tmp/$module.vo" "$file" @@ -27,3 +26,4 @@ jobs: exit 1 fi done + ' From 3777fb7b654e9de91ff2bd3ff5521409215839ec Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 14:11:49 +0200 Subject: [PATCH 07/10] break ci on purpose --- rocq/bad.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 rocq/bad.v diff --git a/rocq/bad.v b/rocq/bad.v new file mode 100644 index 000000000..5fa34d8e0 --- /dev/null +++ b/rocq/bad.v @@ -0,0 +1,6 @@ +From Stdlib Require Import ZArith. + +Open Scope Z_scope. + +Theorem bad : 0 <> 0. +Admitted. From b7fad631f4e7f593e586cffae577cb71541e48f7 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 14:14:27 +0200 Subject: [PATCH 08/10] Revert "break ci on purpose" This reverts commit 3777fb7b654e9de91ff2bd3ff5521409215839ec. --- rocq/bad.v | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 rocq/bad.v diff --git a/rocq/bad.v b/rocq/bad.v deleted file mode 100644 index 5fa34d8e0..000000000 --- a/rocq/bad.v +++ /dev/null @@ -1,6 +0,0 @@ -From Stdlib Require Import ZArith. - -Open Scope Z_scope. - -Theorem bad : 0 <> 0. -Admitted. From 151dbb4bb541f7d70c937708fbb57286904b5d5c Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 14:20:45 +0200 Subject: [PATCH 09/10] use bash --- .github/workflows/rocq.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml index 498128f0f..ab4bae578 100644 --- a/.github/workflows/rocq.yml +++ b/.github/workflows/rocq.yml @@ -15,7 +15,7 @@ jobs: - name: Check proofs and assumptions run: | - docker run --rm -v "$PWD:$PWD" -w "$PWD" rocq/rocq-prover@sha256:b85a80a11bb65c7c843f91c7cbcce282f22ee397c9ca42f123d568ab6cef68b0 sh -lc ' + docker run --rm -v "$PWD:$PWD" -w "$PWD" rocq/rocq-prover@sha256:b85a80a11bb65c7c843f91c7cbcce282f22ee397c9ca42f123d568ab6cef68b0 bash -ec ' # Assume .v files are independent. # Do not check admits in the module'\''s dependencies. for file in rocq/*.v; do From e7d40e2c9dfa8edb54e8adffc41ef5ef60d2d55c Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 24 Jun 2026 17:11:25 +0200 Subject: [PATCH 10/10] remove rocq ci --- .github/workflows/rocq.yml | 29 ----------------------------- 1 file changed, 29 deletions(-) delete mode 100644 .github/workflows/rocq.yml diff --git a/.github/workflows/rocq.yml b/.github/workflows/rocq.yml deleted file mode 100644 index ab4bae578..000000000 --- a/.github/workflows/rocq.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: rocq - -on: - push: - branches: - - main - pull_request: - workflow_dispatch: - -jobs: - prove: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 - - - name: Check proofs and assumptions - run: | - docker run --rm -v "$PWD:$PWD" -w "$PWD" rocq/rocq-prover@sha256:b85a80a11bb65c7c843f91c7cbcce282f22ee397c9ca42f123d568ab6cef68b0 bash -ec ' - # Assume .v files are independent. - # Do not check admits in the module'\''s dependencies. - for file in rocq/*.v; do - module="$(basename "$file" .v)" - rocq compile -o "/tmp/$module.vo" "$file" - output="$(rocq check -silent --output-context "/tmp/$module.vo" 2>&1)" - if printf '%s\n' "$output" | grep -F " $module."; then - exit 1 - fi - done - '