
  * Copyright Amazon.com , Inc. or its affiliates . All Rights Reserved . 
  * SPDX - License - Identifier : Apache-2.0 OR ISC 
 
 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 * SPDX-License-Identifier: Apache-2.0 OR ISC
 *)

(* ========================================================================= *)
(* Tripling modulo p_sm2, the field characteristic for the CC SM2 curve.     *)
(* ========================================================================= *)

(**** print_literal_from_elf "x86/sm2/bignum_triple_sm2.o";;
 ****)

let bignum_triple_sm2_mc = define_assert_from_elf "bignum_triple_sm2_mc" "x86/sm2/bignum_triple_sm2.o"
[
  0x31; 0xc0;              (* XOR (% eax) (% eax) *)
  MOV ( % rdx ) (   ( % % ( rsi,0 ) ) )
  MOV ( % r8 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
                           (* ADCX (% rdx) (% rdx) *)
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xc2;
  ADOX ( % r8 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,8 ) ) )
  MOV ( % r9 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
                           (* ADCX (% rdx) (% rdx) *)
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xca;
  ADOX ( % r9 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,16 ) ) )
  MOV ( % r10 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
                           (* ADCX (% rdx) (% rdx) *)
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xd2;
  ADOX ( % r10 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,24 ) ) )
  MOV ( % r11 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
                           (* ADCX (% rdx) (% rdx) *)
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xda;
  ADOX ( % r11 ) ( % rdx )
  0xba; 0x01; 0x00; 0x00; 0x00;
  MOV ( % edx ) ( Imm32 ( word 1 ) )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd0;
  ADCX ( % rdx ) ( % rax )
  0xf3; 0x48; 0x0f; 0x38; 0xf6; 0xd0;
  ADOX ( % rdx ) ( % rax )
  MOV ( % rax ) ( % rdx )
  SHL ( % rax ) ( Imm8 ( word 32 ) )
  MOV ( % rcx ) ( % rax )
  0x48; 0x29; 0xd0;        (* SUB (% rax) (% rdx) *)
  0x49; 0x01; 0xd0;        (* ADD (% r8) (% rdx) *)
  0x49; 0x11; 0xc1;        (* ADC (% r9) (% rax) *)
  0x49; 0x83; 0xd2; 0x00;  (* ADC (% r10) (Imm8 (word 0)) *)
  0x49; 0x11; 0xcb;        (* ADC (% r11) (% rcx) *)
  SBB ( % rdx ) ( % rdx )
  0x48; 0xf7; 0xd2;        (* NOT (% rdx) *)
  0x48; 0xb8; 0x00; 0x00; 0x00; 0x00; 0xff; 0xff; 0xff; 0xff;
  MOV ( % rax ) ( Imm64 ( word 18446744069414584320 ) )
  0x48; 0x21; 0xd0;        (* AND (% rax) (% rdx) *)
  0x48; 0xb9; 0xff; 0xff; 0xff; 0xff; 0xfe; 0xff; 0xff; 0xff;
  MOV ( % rcx ) ( Imm64 ( word 18446744069414584319 ) )
  0x48; 0x21; 0xd1;        (* AND (% rcx) (% rdx) *)
  0x49; 0x01; 0xd0;        (* ADD (% r8) (% rdx) *)
  MOV (   ( % % ( rdi,0 ) ) ) ( % r8 )
  0x49; 0x11; 0xc1;        (* ADC (% r9) (% rax) *)
  MOV (   ( % % ( rdi,8 ) ) ) ( % r9 )
  0x49; 0x11; 0xd2;        (* ADC (% r10) (% rdx) *)
  MOV (   ( % % ( rdi,16 ) ) ) ( % r10 )
  0x49; 0x11; 0xcb;        (* ADC (% r11) (% rcx) *)
  MOV (   ( % % (  ) ) ) ( % r11 )
  RET
];;

let BIGNUM_TRIPLE_SM2_EXEC = X86_MK_CORE_EXEC_RULE bignum_triple_sm2_mc;;

(* ------------------------------------------------------------------------- *)
(* Proof.                                                                    *)
(* ------------------------------------------------------------------------- *)

let p_sm2 = new_definition `p_sm2 = 0xFFFFFFFEFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000FFFFFFFFFFFFFFFF`;;

let sm2genshortredlemma = prove
 (`!n. n < 3 * 2 EXP 256
       ==> let q = (n DIV 2 EXP 256) + 1 in
           q <= 3 /\
           q * p_sm2 <= n + p_sm2 /\
           n < q * p_sm2 + p_sm2`,
  CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[p_sm2] THEN ARITH_TAC);;

let BIGNUM_TRIPLE_SM2_CORRECT = time prove
 (`!z x n pc.
        nonoverlapping (word pc,0xb4) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_triple_sm2_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = word (pc + 0xb3) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`z:int64`; `x:int64`; `n:num`; `pc:num`] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  BIGNUM_TERMRANGE_TAC `4` `n:num` THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "n_" `read (memory :> bytes (x,8 * 4)) s0` THEN

* * Input load and initial multiplication by 3 * *

  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC (1--20) (1--20) THEN
  SUBGOAL_THEN
   `bignum_of_wordlist [sum_s5; sum_s9; sum_s13; sum_s17; sum_s20] =
    2 EXP 256 + 3 * n`
  ASSUME_TAC THENL
   [EXPAND_TAC "n" THEN
    REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
    ACCUMULATOR_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN
    DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_ARITH_TAC;
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN DISCARD_FLAGS_TAC] THEN

  (*** Properties of quotient estimate q = h + 1 ***)

  ABBREV_TAC `h = (3 * n) DIV 2 EXP 256` THEN
  SUBGOAL_THEN `h < 3` ASSUME_TAC THENL
   [UNDISCH_TAC `n < 2 EXP (64 * 4)` THEN EXPAND_TAC "h" THEN ARITH_TAC;
    ALL_TAC] THEN
  SUBGOAL_THEN `sum_s20:int64 = word(h + 1)` SUBST_ALL_TAC THENL
   [EXPAND_TAC "h" THEN REWRITE_TAC[ARITH_RULE
     `(3 * n) DIV 2 EXP 256 + 1 = (2 EXP 256 + 3 * n) DIV 2 EXP 256`] THEN
    FIRST_X_ASSUM(fun th ->
      GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV) [SYM th]) THEN
    CONV_TAC(ONCE_DEPTH_CONV BIGNUM_OF_WORDLIST_DIV_CONV) THEN
    REWRITE_TAC[WORD_VAL];
    ALL_TAC] THEN
  MP_TAC(SPEC `3 * n` sm2genshortredlemma) THEN ASM_REWRITE_TAC[] THEN
  ANTS_TAC THENL
   [UNDISCH_TAC `n < 2 EXP (64 * 4)` THEN ARITH_TAC;
    CONV_TAC(LAND_CONV let_CONV) THEN STRIP_TAC] THEN

* * Computation of 3 * n - ( h + 1 ) * p_sm2 * *

  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC (25--28) (21--30) THEN
  MP_TAC(SPECL
   [`word_neg(word(bitval(~carry_s28))):int64`;
    `&(bignum_of_wordlist[sum_s25; sum_s26; sum_s27; sum_s28]):real`;
    `256`; `3 * n`; `(h + 1) * p_sm2`]
   MASK_AND_VALUE_FROM_CARRY_LT) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [REWRITE_TAC[GSYM WORD_NOT_MASK; REAL_VAL_WORD_NOT; DIMINDEX_64] THEN
    CONJ_TAC THENL
     [MAP_EVERY UNDISCH_TAC
       [`(h + 1) * p_sm2 <= 3 * n + p_sm2`;
        `3 * n < (h + 1) * p_sm2 + p_sm2`] THEN
      REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_sm2] THEN REAL_ARITH_TAC;
      ALL_TAC] THEN
    CONJ_TAC THENL
     [REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
      BOUNDER_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `&(3 * n):real =
      &(bignum_of_wordlist [sum_s5; sum_s9; sum_s13; sum_s17; word (h + 1)]) -
      &2 pow 256`
    SUBST1_TAC THENL
     [ASM_REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN REAL_ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[p_sm2; bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
    ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
    UNDISCH_TAC `h < 3` THEN
    SPEC_TAC(`h:num`,`h:num`) THEN CONV_TAC EXPAND_CASES_CONV THEN
    CONV_TAC(DEPTH_CONV(NUM_RED_CONV ORELSEC WORD_RED_CONV ORELSEC
                        GEN_REWRITE_CONV I [BITVAL_CLAUSES])) THEN
    REWRITE_TAC[REAL_VAL_WORD_MASK; DIMINDEX_64] THEN REPEAT CONJ_TAC THEN
    DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN
    DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC;
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN DISCARD_FLAGS_TAC THEN
    REWRITE_TAC[WORD_ARITH `word_neg x = word_neg y <=> val x = val y`] THEN
    REWRITE_TAC[VAL_WORD_BITVAL; EQ_BITVAL] THEN
    REWRITE_TAC[TAUT `(~p <=> q) <=> (p <=> ~q)`] THEN
    DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN
    RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP]) THEN
    REWRITE_TAC[MESON[REAL_MUL_RZERO; REAL_MUL_RID; REAL_ADD_RID; bitval]
     `(if p then x + a else x):real = x + a * &(bitval p)`] THEN
    DISCH_TAC] THEN

  (*** Final corrective masked addition ***)

  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC [35;37;39;41] (31--42) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[WORD_NOT_MASK; NOT_LE]) THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_UNIQ_BALANCED_REAL THEN
  MAP_EVERY EXISTS_TAC [`h + 1`; `256`] THEN
  ASM_REWRITE_TAC[] THEN
  ABBREV_TAC `topcar <=> 3 * n < (h + 1) * p_sm2` THEN
  FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
   `x:real = &(3 * n) - y + z ==> &(3 * n) = x + y - z`)) THEN
  REWRITE_TAC[p_sm2] THEN CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
  CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_sm2; bignum_of_wordlist] THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN
  POP_ASSUM_LIST(K ALL_TAC) THEN
  BOOL_CASES_TAC `topcar:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC WORD_REDUCE_CONV THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC);;

let BIGNUM_TRIPLE_SM2_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        nonoverlapping (word pc,0xb4) (z,8 * 4) /\
        nonoverlapping (stackpointer,8) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_triple_sm2_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RSP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_triple_sm2_mc
      BIGNUM_TRIPLE_SM2_CORRECT);;

(* ------------------------------------------------------------------------- *)
(* Correctness of Windows ABI version.                                       *)
(* ------------------------------------------------------------------------- *)

let windows_bignum_triple_sm2_mc = define_from_elf
   "windows_bignum_triple_sm2_mc" "x86/sm2/bignum_triple_sm2.obj";;

let WINDOWS_BIGNUM_TRIPLE_SM2_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0xbe); (x,8 * 4)] /\
        nonoverlapping (word pc,0xbe) (z,8 * 4) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_triple_sm2_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  WINDOWS_C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RSP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC
    windows_bignum_triple_sm2_mc bignum_triple_sm2_mc
    BIGNUM_TRIPLE_SM2_CORRECT);;

 ========================================================================= 
 Tripling modulo p_sm2, the field characteristic for the CC SM2 curve.     
 ========================================================================= 
*** print_literal_from_elf "x86/sm2/bignum_triple_sm2.o";;
 ***
 XOR (% eax) (% eax) 
 ADCX (% rdx) (% rdx) 
 ADCX (% rdx) (% rdx) 
 ADCX (% rdx) (% rdx) 
 ADCX (% rdx) (% rdx) 
 SUB (% rax) (% rdx) 
 ADD (% r8) (% rdx) 
 ADC (% r9) (% rax) 
 ADC (% r10) (Imm8 (word 0)) 
 ADC (% r11) (% rcx) 
 NOT (% rdx) 
 AND (% rax) (% rdx) 
 AND (% rcx) (% rdx) 
 ADD (% r8) (% rdx) 
 ADC (% r9) (% rax) 
 ADC (% r10) (% rdx) 
 ADC (% r11) (% rcx) 
 ------------------------------------------------------------------------- 
 Proof.                                                                    
 ------------------------------------------------------------------------- 
** Properties of quotient estimate q = h + 1 **
** Final corrective masked addition **
 ------------------------------------------------------------------------- 
 Correctness of Windows ABI version.                                       
 ------------------------------------------------------------------------- 

  * Copyright Amazon.com , Inc. or its affiliates . All Rights Reserved . 
  * SPDX - License - Identifier : Apache-2.0 OR ISC 
 
 * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 * SPDX-License-Identifier: Apache-2.0 OR ISC
 *)



let bignum_triple_sm2_mc = define_assert_from_elf "bignum_triple_sm2_mc" "x86/sm2/bignum_triple_sm2.o"
[
  MOV ( % rdx ) (   ( % % ( rsi,0 ) ) )
  MOV ( % r8 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xc2;
  ADOX ( % r8 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,8 ) ) )
  MOV ( % r9 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xca;
  ADOX ( % r9 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,16 ) ) )
  MOV ( % r10 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xd2;
  ADOX ( % r10 ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,24 ) ) )
  MOV ( % r11 ) ( % rdx )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd2;
  0xf3; 0x4c; 0x0f; 0x38; 0xf6; 0xda;
  ADOX ( % r11 ) ( % rdx )
  0xba; 0x01; 0x00; 0x00; 0x00;
  MOV ( % edx ) ( Imm32 ( word 1 ) )
  0x66; 0x48; 0x0f; 0x38; 0xf6; 0xd0;
  ADCX ( % rdx ) ( % rax )
  0xf3; 0x48; 0x0f; 0x38; 0xf6; 0xd0;
  ADOX ( % rdx ) ( % rax )
  MOV ( % rax ) ( % rdx )
  SHL ( % rax ) ( Imm8 ( word 32 ) )
  MOV ( % rcx ) ( % rax )
  SBB ( % rdx ) ( % rdx )
  0x48; 0xb8; 0x00; 0x00; 0x00; 0x00; 0xff; 0xff; 0xff; 0xff;
  MOV ( % rax ) ( Imm64 ( word 18446744069414584320 ) )
  0x48; 0xb9; 0xff; 0xff; 0xff; 0xff; 0xfe; 0xff; 0xff; 0xff;
  MOV ( % rcx ) ( Imm64 ( word 18446744069414584319 ) )
  MOV (   ( % % ( rdi,0 ) ) ) ( % r8 )
  MOV (   ( % % ( rdi,8 ) ) ) ( % r9 )
  MOV (   ( % % ( rdi,16 ) ) ) ( % r10 )
  MOV (   ( % % (  ) ) ) ( % r11 )
  RET
];;

let BIGNUM_TRIPLE_SM2_EXEC = X86_MK_CORE_EXEC_RULE bignum_triple_sm2_mc;;


let p_sm2 = new_definition `p_sm2 = 0xFFFFFFFEFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000FFFFFFFFFFFFFFFF`;;

let sm2genshortredlemma = prove
 (`!n. n < 3 * 2 EXP 256
       ==> let q = (n DIV 2 EXP 256) + 1 in
           q <= 3 /\
           q * p_sm2 <= n + p_sm2 /\
           n < q * p_sm2 + p_sm2`,
  CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[p_sm2] THEN ARITH_TAC);;

let BIGNUM_TRIPLE_SM2_CORRECT = time prove
 (`!z x n pc.
        nonoverlapping (word pc,0xb4) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_triple_sm2_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = word (pc + 0xb3) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`z:int64`; `x:int64`; `n:num`; `pc:num`] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  BIGNUM_TERMRANGE_TAC `4` `n:num` THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "n_" `read (memory :> bytes (x,8 * 4)) s0` THEN

* * Input load and initial multiplication by 3 * *

  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC (1--20) (1--20) THEN
  SUBGOAL_THEN
   `bignum_of_wordlist [sum_s5; sum_s9; sum_s13; sum_s17; sum_s20] =
    2 EXP 256 + 3 * n`
  ASSUME_TAC THENL
   [EXPAND_TAC "n" THEN
    REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
    ACCUMULATOR_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN
    DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_ARITH_TAC;
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN DISCARD_FLAGS_TAC] THEN


  ABBREV_TAC `h = (3 * n) DIV 2 EXP 256` THEN
  SUBGOAL_THEN `h < 3` ASSUME_TAC THENL
   [UNDISCH_TAC `n < 2 EXP (64 * 4)` THEN EXPAND_TAC "h" THEN ARITH_TAC;
    ALL_TAC] THEN
  SUBGOAL_THEN `sum_s20:int64 = word(h + 1)` SUBST_ALL_TAC THENL
   [EXPAND_TAC "h" THEN REWRITE_TAC[ARITH_RULE
     `(3 * n) DIV 2 EXP 256 + 1 = (2 EXP 256 + 3 * n) DIV 2 EXP 256`] THEN
    FIRST_X_ASSUM(fun th ->
      GEN_REWRITE_TAC (RAND_CONV o RAND_CONV o LAND_CONV) [SYM th]) THEN
    CONV_TAC(ONCE_DEPTH_CONV BIGNUM_OF_WORDLIST_DIV_CONV) THEN
    REWRITE_TAC[WORD_VAL];
    ALL_TAC] THEN
  MP_TAC(SPEC `3 * n` sm2genshortredlemma) THEN ASM_REWRITE_TAC[] THEN
  ANTS_TAC THENL
   [UNDISCH_TAC `n < 2 EXP (64 * 4)` THEN ARITH_TAC;
    CONV_TAC(LAND_CONV let_CONV) THEN STRIP_TAC] THEN

* * Computation of 3 * n - ( h + 1 ) * p_sm2 * *

  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC (25--28) (21--30) THEN
  MP_TAC(SPECL
   [`word_neg(word(bitval(~carry_s28))):int64`;
    `&(bignum_of_wordlist[sum_s25; sum_s26; sum_s27; sum_s28]):real`;
    `256`; `3 * n`; `(h + 1) * p_sm2`]
   MASK_AND_VALUE_FROM_CARRY_LT) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [REWRITE_TAC[GSYM WORD_NOT_MASK; REAL_VAL_WORD_NOT; DIMINDEX_64] THEN
    CONJ_TAC THENL
     [MAP_EVERY UNDISCH_TAC
       [`(h + 1) * p_sm2 <= 3 * n + p_sm2`;
        `3 * n < (h + 1) * p_sm2 + p_sm2`] THEN
      REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_sm2] THEN REAL_ARITH_TAC;
      ALL_TAC] THEN
    CONJ_TAC THENL
     [REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
      BOUNDER_TAC[];
      ALL_TAC] THEN
    SUBGOAL_THEN
     `&(3 * n):real =
      &(bignum_of_wordlist [sum_s5; sum_s9; sum_s13; sum_s17; word (h + 1)]) -
      &2 pow 256`
    SUBST1_TAC THENL
     [ASM_REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN REAL_ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[p_sm2; bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
    ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
    UNDISCH_TAC `h < 3` THEN
    SPEC_TAC(`h:num`,`h:num`) THEN CONV_TAC EXPAND_CASES_CONV THEN
    CONV_TAC(DEPTH_CONV(NUM_RED_CONV ORELSEC WORD_RED_CONV ORELSEC
                        GEN_REWRITE_CONV I [BITVAL_CLAUSES])) THEN
    REWRITE_TAC[REAL_VAL_WORD_MASK; DIMINDEX_64] THEN REPEAT CONJ_TAC THEN
    DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN
    DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC;
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN DISCARD_FLAGS_TAC THEN
    REWRITE_TAC[WORD_ARITH `word_neg x = word_neg y <=> val x = val y`] THEN
    REWRITE_TAC[VAL_WORD_BITVAL; EQ_BITVAL] THEN
    REWRITE_TAC[TAUT `(~p <=> q) <=> (p <=> ~q)`] THEN
    DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC MP_TAC) THEN
    RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP]) THEN
    REWRITE_TAC[MESON[REAL_MUL_RZERO; REAL_MUL_RID; REAL_ADD_RID; bitval]
     `(if p then x + a else x):real = x + a * &(bitval p)`] THEN
    DISCH_TAC] THEN


  X86_ACCSTEPS_TAC BIGNUM_TRIPLE_SM2_EXEC [35;37;39;41] (31--42) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[WORD_NOT_MASK; NOT_LE]) THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_UNIQ_BALANCED_REAL THEN
  MAP_EVERY EXISTS_TAC [`h + 1`; `256`] THEN
  ASM_REWRITE_TAC[] THEN
  ABBREV_TAC `topcar <=> 3 * n < (h + 1) * p_sm2` THEN
  FIRST_X_ASSUM(SUBST1_TAC o MATCH_MP (REAL_ARITH
   `x:real = &(3 * n) - y + z ==> &(3 * n) = x + y - z`)) THEN
  REWRITE_TAC[p_sm2] THEN CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN
  CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_sm2; bignum_of_wordlist] THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN
  POP_ASSUM_LIST(K ALL_TAC) THEN
  BOOL_CASES_TAC `topcar:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC WORD_REDUCE_CONV THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC);;

let BIGNUM_TRIPLE_SM2_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        nonoverlapping (word pc,0xb4) (z,8 * 4) /\
        nonoverlapping (stackpointer,8) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_triple_sm2_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RSP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_triple_sm2_mc
      BIGNUM_TRIPLE_SM2_CORRECT);;


let windows_bignum_triple_sm2_mc = define_from_elf
   "windows_bignum_triple_sm2_mc" "x86/sm2/bignum_triple_sm2.obj";;

let WINDOWS_BIGNUM_TRIPLE_SM2_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0xbe); (x,8 * 4)] /\
        nonoverlapping (word pc,0xbe) (z,8 * 4) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_triple_sm2_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  WINDOWS_C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  bignum_from_memory (z,4) s = (3 * n) MOD p_sm2)
          (MAYCHANGE [RIP; RSP; RAX; RCX; RDX; R8; R9; R10; R11] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC
    windows_bignum_triple_sm2_mc bignum_triple_sm2_mc
    BIGNUM_TRIPLE_SM2_CORRECT);;
