anchor.diff:  #if verify
             Pi.expect (ServerLogBeforeClientCertificateDHE_Auth(si,log));          
   #endif
  -          let ps = serverState ci (ClientCertificateDHE(si,p,g,y,x,log)) in
  +          let ps = serverState ci (ClientCertificateDHE(si,p,g,gx,x,log)) in
           (* Compute the next state of the server *)
               correct (
                 {state with hs_outgoing = output;
  
positive.code: #if verify
            Pi.expect (ServerLogBeforeClientCertificateDHE_NoAuth(si,log));          
  #endif
            let ps = serverState ci (ClientKeyExchangeDHE(si,p,g,y,x,log)) in
              correct (
                {state with hs_outgoing = output;
                            pstate = ps},
  
negative.code: 
          (* ServerKeyExchange *)
          (*KB DH-PMS-KEM (server 1) *)
          let (p,g,gx,x) = DH.serverGen() in
          //~ pms-KEM: ((p,g),gx),(((p,g),gx),x) = keygen_DHE() 
  
          let dheB = dheParamBytes p g gx in
          let toSign = si.init_crand @| si.init_srand @| dheB in
          let sign = Sig.sign alg sk toSign in
  
  