Update proofs to work with most recent EC version and setup CI.

.github/workflows/ci.yml

@@ -0,0 +1,56 @@
+name: XMSS
+
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - master
+      - ci
+
+env:
+  OPAMROOT: /home/charlie/.opam
+  OPAMYES: true
+  OPAMJOBS: 2
+  ECRJOBS: 1
+
+jobs:
+  ec:
+    name: Check XMSS EasyCrypt Project
+    runs-on: ubuntu-20.04
+    container:
+      image: ghcr.io/easycrypt/ec-build-box
+    strategy:
+      fail-fast: false
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - uses: actions/checkout@v4
+      name: Checkout EasyCrypt
+      with:
+        repository: EasyCrypt/easycrypt
+        ref: refs/heads/main
+        path: easycrypt
+    - name: Update OPAM & EasyCrypt dependencies
+      run: |
+        opam update
+        opam pin add -n easycrypt easycrypt
+        opam install --deps-only easycrypt
+    - name: Compile & Install EasyCrypt
+      run: opam install easycrypt
+    - name: Detect SMT provers
+      run: |
+        opam config exec -- easycrypt why3config -why3 ~/.why3.conf
+    - name: Compile Project (acai)
+      run: opam config exec -- easycrypt runtest -report report_acai.log -raw-args -gcstats config/tests.config xmss-acai
+    - name: Compile Project (fsai)
+      run: opam config exec -- easycrypt runtest -report report_fsai.log -raw-args -gcstats config/tests.config xmss-fsai
+    - uses: actions/upload-artifact@v4
+      name: Upload reports
+      if: always()
+      with:
+        name: reports
+        path: |
+          report_acai.log
+          report_fsai.log
+        if-no-files-found: ignore

README.md

@@ -1,13 +1,13 @@
-# Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+
-This repository accompanies the paper "Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+", authored by Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub. The original (proceeding's) version of the paper can be found [here](https://link.springer.com/chapter/10.1007/978-3-031-38554-4_14); the most recent version of the paper can be found [here](https://eprint.iacr.org/2023/408).\
+# Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺
+This repository accompanies the paper "Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺", authored by Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, and Pierre-Yves Strub. The original (proceeding's) version of the paper can be found [here](https://link.springer.com/chapter/10.1007/978-3-031-38554-4_14); the most recent version of the paper can be found [here](https://eprint.iacr.org/2023/408).\
 \
-This repository comprises EasyCrypt scripts primarily aimed at the formal verification of the security of XMSS as a standalone construction — specified in [RFC 8391](https://www.rfc-editor.org/rfc/rfc8391). Due to the modular approach taken in the formal verification, the scripts contain an independent formal verification of the fix of the security proof of SPHINCS+ presented in [Recovering the Tight Security Proof of SPHINCS+](https://link.springer.com/chapter/10.1007/978-3-031-22972-5_1), validating the remediation of the flaw in the original proof and paving the way for a complete formal verification of SPHINCS+. Furthermore, again due to the modular approach, the scripts contain an independent formal verification of a security property of XMSS as a component of SPHINCS+.\
+This repository comprises EasyCrypt scripts primarily aimed at the formal verification of the security of XMSS as a standalone construction — specified in [RFC 8391](https://www.rfc-editor.org/rfc/rfc8391). Due to the modular approach taken in the formal verification, the scripts contain an independent formal verification of the fix of the security proof of SPHINCS⁺ presented in [Recovering the Tight Security Proof of SPHINCS⁺](https://link.springer.com/chapter/10.1007/978-3-031-22972-5_1), validating the remediation of the flaw in the original proof and paving the way for a complete formal verification of SPHINCS⁺. Furthermore, again due to the modular approach, the scripts contain an independent formal verification of a security property of XMSS as a component of SPHINCS⁺.\
 \
 Currently, the latest version of EasyCrypt that has been confirmed to verify the scripts in this repository corresponds to the following commit of the `main` branch of the [EasyCrypt repository](https://github.com/EasyCrypt/easycrypt): `commit eaba09c215c28b292259bd61aaf575bf7d21dbfe`.
 
 ## Repository Structure and Contents
 This repository is structured as follows.
-* `proofs/`: All scripts relevant to the formal verification of the security of XMSS (both as standalone and as a component of SPHINCS+) and the fix of the security proof of SPHINCS+.
+* `proofs/`: All scripts relevant to the formal verification of the security of XMSS (both as standalone and as a component of SPHINCS⁺) and the fix of the security proof of SPHINCS⁺.
   * `acai/` (*abstract context address indices*): Scripts comprising a version of the proofs that completely abstracts away (the indices corresponding to) the part of the addresses that is not directly used/manipulated in the executed operations (i.e., the part that may be used to, for example, differentiate the context in an encompassing structure).  
     * `DigitalSignatures.eca`: (Library) Generically defines signature schemes (both stateless and key-updating) and their security notions.
     * `DigitalSignaturesROM.eca`: (Library) Similar to `DigitalSignatures.eca`, except that it defines everything with respect to a random oracle (this is for proofs in the random oracle model).
@@ -21,4 +21,4 @@ This repository is structured as follows.
     * `WOTS_TW.ec`: Provides the context, specification, and proofs concerning WOTS-TW (with an abstract encoding).
     * `WOTS_TW_Checksum.ec`: Defines the concrete encoding used in WOTS-TW and demonstrates that the proofs from `WOTS_TW.ec` still hold true when using this encoding.
     * `XMSS_TW.ec`: Provides the context, specification, and proofs concerning XMSS-TW.
-  * `fsai/` (*fully specified address indices*): Scripts comprising a version of the proofs that entirely specifies the (indices contained in the) addresses. More precisely, it considers the (relevant) indices used for the addresses in SPHINCS+. The files in this directory are identically named to those in the `acai/` directory (except that this directory does not contain the `HashAddresses.ec` file); indeed, each of these files is analogous (in purpose) to its similarly-named counterpart in the `acai\` directory.
+  * `fsai/` (*fully specified address indices*): Scripts comprising a version of the proofs that entirely specifies the (indices contained in the) addresses. More precisely, it considers the (relevant) indices used for the addresses in SPHINCS⁺. The files in this directory are identically named to those in the `acai/` directory (except that this directory does not contain the `HashAddresses.ec` file); indeed, each of these files is analogous (in purpose) to its similarly-named counterpart in the `acai\` directory.

config/tests.config

@@ -0,0 +1,5 @@
+[test-xmss-acai]
+okdirs  = !proofs/acai
+
+[test-xmss-fsai]
+okdirs  = !proofs/fsai

easycrypt.project

@@ -0,0 +1,5 @@
+[general]
+timeout = 10
+provers = [email protected]
+provers = [email protected]
+provers = [email protected]

proofs/acai/FL_XMSS_TW.ec

@@ -4742,7 +4742,7 @@ have nthxval:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i (R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.inpll{2})) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   rewrite xval equnz2ts_flinpl nth_flatten 1,2:/#.
   case (i = 1) => [eq1_i | neq1_i].
@@ -4763,7 +4763,7 @@ have -> //=:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.adrsll{2}) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   do 4! congr. 
   apply (eq_from_nth witness); first by rewrite 2!size_map ?size_take /#. 

proofs/acai/HashThenSign.eca

@@ -1323,8 +1323,8 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
-  rewrite addrC; apply ler_add.
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
+  rewrite addrC ler_add. 
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
                       Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(true) @ &m : res] |).
@@ -1356,7 +1356,7 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
   rewrite addrC; apply ler_add.
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
@@ -2035,8 +2035,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_CRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 
@@ -2066,8 +2065,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_METCRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 

proofs/acai/WOTS_TW.ec

@@ -898,7 +898,7 @@ clone import FC.SMDTPREC as FC_PRE with
   Interpretation of arguments is, respectively, as follows:
   - Tweakable hash function to chain
   - Public seed
-  - Address (should be of chaining type (chtype))
+  - Address
   - Current position/index in chain
   - Number of times to chain the tweakable hash function
   - Input to apply the tweakable hash function on
@@ -5368,7 +5368,7 @@ have indtelesum:
     BRA.bigi predT (fun (x : int) => Pr[DistRCHil.main(x) @ &m : res] - Pr[DistRCHil.main(x + 1) @ &m : res]) 0 i.
 + elim => [/= | i ge0_i ih]; first by rewrite range_geq.
   rewrite -addr0 (: 0%r = (- Pr[DistRCHil.main(i) @ &m : res] + Pr[DistRCHil.main(i) @ &m : res])) 1:/#.
-  by rewrite addrA ih BRA.big_int_recr //= addrA.
+  by rewrite BRA.big_int_recr /#.
 rewrite (indtelesum (w - 2)); first by smt(val_w).
 have ->:
   BRA.bigi predT (fun (i : int) => Pr[DistRCHil.main(i) @ &m : res] - Pr[DistRCHil.main(i + 1) @ &m : res]) 0 (w - 2)

proofs/fsai/FL_XMSS_TW.ec

@@ -4109,7 +4109,7 @@ have nthxval:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.inpll{2}) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   rewrite xval equnz2ts_flinpl nth_flatten 1,2:/#.
   case (i = 1) => [eq1_i | neq1_i].
@@ -4130,7 +4130,7 @@ have -> //=:
     split=> [| _].
     * rewrite {2}(: i = i - 1 + 1) // (take_nth witness) 1:/# flatten_rcons size_cat.
       by rewrite ltz_add2l /#.
-    rewrite -{2}(cat_take_drop i) flatten_cat size_cat.
+    rewrite -{2}(cat_take_drop i R_SMDTTCRCTRH_EUFRMAFLXMSSTWESNOPRF.adrsll{2}) flatten_cat size_cat.
     by rewrite lez_addl size_ge0.
   do 4! congr. 
   apply (eq_from_nth witness); first by rewrite 2!size_map ?size_take /#. 

proofs/fsai/HashThenSign.eca

@@ -1355,7 +1355,7 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
   rewrite addrC; apply ler_add.
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
@@ -1388,7 +1388,7 @@ theory WithSampling.
   apply (ler_trans (`|  Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]
                       - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] |
                     + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])).
-  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0] 2:&(ler_norm_add).
+  + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add).
   rewrite addrC; apply ler_add.
   + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA.
   apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] -
@@ -2067,8 +2067,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_CRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 
@@ -2098,8 +2097,7 @@ theory WithPRF.
   rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA.
   apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - 
                        Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | +
-                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)).
-  + by apply ler_norm_add.
+                    `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add).
   rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //.
   rewrite ger0_norm 1:Pr[mu_ge0] //.
   move: (ALKUDSS_EUFCMARO_METCRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A 

proofs/fsai/WOTS_TW.ec

@@ -5616,7 +5616,7 @@ have indtelesum:
     BRA.bigi predT (fun (x : int) => Pr[DistRCHil.main(x) @ &m : res] - Pr[DistRCHil.main(x + 1) @ &m : res]) 0 i.
 + elim => [/= | i ge0_i ih]; first by rewrite range_geq.
   rewrite -addr0 (: 0%r = (- Pr[DistRCHil.main(i) @ &m : res] + Pr[DistRCHil.main(i) @ &m : res])) 1:/#.
-  by rewrite addrA ih BRA.big_int_recr //= addrA.
+  by rewrite addrA BRA.big_int_recr /#.
 rewrite (indtelesum (w - 2)); first by smt(val_w).
 have ->:
   BRA.bigi predT (fun (i : int) => Pr[DistRCHil.main(i) @ &m : res] - Pr[DistRCHil.main(i + 1) @ &m : res]) 0 (w - 2)