
  * 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
 *)

(* ========================================================================= *)
(* Addition modulo p_256k1, the field characteristic for secp256k1.          *)
(* ========================================================================= *)

(**** print_literal_from_elf "x86/secp256k1/bignum_add_p256k1.o";;
 ****)

let bignum_add_p256k1_mc = define_assert_from_elf "bignum_add_p256k1_mc" "x86/secp256k1/bignum_add_p256k1.o"
[
  MOV ( % rcx ) (   ( % % ( rsi,0 ) ) )
  ADD ( % rcx ) (   ( % % ( rdx,0 ) ) )
  MOV ( % r8 ) (   ( % % ( rsi,8 ) ) )
  ADC ( % r8 ) (   ( % % ( rdx,8 ) ) )
  MOV ( % r9 ) (   ( % % ( rsi,16 ) ) )
  ADC ( % r9 ) (   ( % % ( rdx,16 ) ) )
  MOV ( % r10 ) (   ( % % ( rsi,24 ) ) )
  ADC ( % r10 ) (   ( % % ( rdx,24 ) ) )
  SBB ( % rdx ) ( % rdx )
  MOV ( % rax ) ( % r8 )
  0x4c; 0x21; 0xc8;        (* AND (% rax) (% r9) *)
  0x4c; 0x21; 0xd0;        (* AND (% rax) (% r10) *)
  0x48; 0xbe; 0x2e; 0xfc; 0xff; 0xff; 0xfe; 0xff; 0xff; 0xff;
  MOV ( % rsi ) ( Imm64 ( word 18446744069414583342 ) )
  CMP ( % rsi ) ( % rcx )
  0x48; 0x83; 0xd0; 0x00;  (* ADC (% rax) (Imm8 (word 0)) *)
  SBB ( % rdx ) ( Imm8 ( word 0 ) )
  0x48; 0xf7; 0xd6;        (* NOT (% rsi) *)
  0x48; 0x0f; 0x44; 0xf2;  (* CMOVE (% rsi) (% rdx) *)
  0x48; 0x01; 0xf1;        (* ADD (% rcx) (% rsi) *)
  MOV (   ( % % ( rdi,0 ) ) ) ( % rcx )
  0x49; 0x83; 0xd0; 0x00;  (* ADC (% r8) (Imm8 (word 0)) *)
  MOV (   ( % % ( rdi,8 ) ) ) ( % r8 )
  0x49; 0x83; 0xd1; 0x00;  (* ADC (% r9) (Imm8 (word 0)) *)
  MOV (   ( % % ( rdi,16 ) ) ) ( % r9 )
  0x49; 0x83; 0xd2; 0x00;  (* ADC (% r10) (Imm8 (word 0)) *)
  MOV (   ( % % (  ) ) ) ( % r10 )
  RET
];;

let BIGNUM_ADD_P256K1_EXEC = X86_MK_CORE_EXEC_RULE bignum_add_p256k1_mc;;

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

let p_256k1 = new_definition `p_256k1 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F`;;

let BIGNUM_ADD_P256K1_CORRECT = time prove
 (`!z x y m n pc.
        nonoverlapping (word pc,0x65) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_add_p256k1_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = word (pc + 0x64) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSI; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`z:int64`; `x:int64`; `y:int64`; `m:num`; `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
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "m_" `read (memory :> bytes (x,8 * 4)) s0` THEN
  BIGNUM_DIGITIZE_TAC "n_" `read (memory :> bytes (y,8 * 4)) s0` THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC [2;4;6;8] (1--9) THEN
  ABBREV_TAC `l = bignum_of_wordlist [sum_s2; sum_s4; sum_s6; sum_s8]` THEN
  SUBGOAL_THEN `2 EXP 256 * bitval carry_s8 + l = m + n` ASSUME_TAC THENL
   [MAP_EVERY EXPAND_TAC ["l"; "m"; "n"] THEN
    REWRITE_TAC[bignum_of_wordlist; MULT_CLAUSES; ADD_CLAUSES] THEN
    REWRITE_TAC[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;
    RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC (14--15) (10--18) THEN
  RULE_ASSUM_TAC(SIMP_RULE[ADD_CLAUSES; VAL_EQ_0]) THEN
  SUBGOAL_THEN
   `word_sub (word_neg (word (bitval carry_s8))) (word (bitval carry_s15)) =
    (word 0:int64)<=>
    m + n < p_256k1`
  SUBST_ALL_TAC THENL
   [REWRITE_TAC[WORD_RULE
     `word_sub (word_neg x) y = word 0 <=> word_add x y = word 0`] THEN
    REWRITE_TAC[GSYM VAL_EQ_0] THEN
   REWRITE_TAC[VAL_WORD_ADD_CASES; VAL_WORD_BITVAL; DIMINDEX_64] THEN
    SIMP_TAC[ADD_EQ_0; BITVAL_EQ_0; BITVAL_BOUND; ARITH_RULE
     `a <= 1 /\ b <= 1 ==> a + b < 2 EXP 64`] THEN
    FIRST_X_ASSUM(fun th ->
     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [SYM th]) THEN
    ASM_CASES_TAC `carry_s8:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THENL
     [REWRITE_TAC[p_256k1] THEN ARITH_TAC; ALL_TAC] THEN
    REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; GSYM NOT_LE] THEN AP_TERM_TAC THEN
    TRANS_TAC EQ_TRANS `2 EXP 256 <= l + 4294968273` THEN CONJ_TAC THENL
     [ALL_TAC; REWRITE_TAC[p_256k1] THEN ARITH_TAC] THEN
    TRANS_TAC EQ_TRANS
     `2 EXP 128 <=
      bignum_of_wordlist[sum_s2; word_and (word_and sum_s4 sum_s6) sum_s8] +
      4294968273` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC FLAG_FROM_CARRY_LE THEN EXISTS_TAC `128` THEN
      REWRITE_TAC[bignum_of_wordlist; MULT_CLAUSES; ADD_CLAUSES] THEN
      REWRITE_TAC[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 BOUNDER_TAC[];
      ALL_TAC] THEN
    EXPAND_TAC "l" THEN ONCE_REWRITE_TAC[bignum_of_wordlist] THEN
    MATCH_MP_TAC(ARITH_RULE
     `l < 2 EXP 64 /\ (a < 2 EXP 64 - 1 <=> h < 2 EXP 192 - 1) /\
      (~(h < 2 EXP 192 - 1)
       ==> (2 EXP 128 <= (l + 2 EXP 64 * a) + 4294968273 <=>
            2 EXP 256 <= (l + 2 EXP 64 * h) + 4294968273))
      ==> (2 EXP 128 <= (l + 2 EXP 64 * a) + 4294968273 <=>
           2 EXP 256 <= (l + 2 EXP 64 * h) + 4294968273)`) THEN
    SIMP_TAC[VAL_BOUND_64; BIGNUM_OF_WORDLIST_LT_MAX; LENGTH;
             ARITH_MULT; ARITH_ADD; ARITH_SUC; EX; DE_MORGAN_THM;
             WORD_BITWISE_RULE
              `word_and a b = word_not(word 0) <=>
               a = word_not(word 0) /\ b = word_not(word 0)`] THEN
    REWRITE_TAC[DISJ_ACI] THEN DISCH_TAC THEN
    ASM_REWRITE_TAC[bignum_of_wordlist] THEN CONV_TAC WORD_REDUCE_CONV THEN
    ARITH_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP]) THEN
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC [19;21;23;25] (19--26) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN
  ASM_REWRITE_TAC[] THEN DISCARD_STATE_TAC "s23" THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC EQUAL_FROM_CONGRUENT_MOD_MOD THEN
  MAP_EVERY EXISTS_TAC
   [`64 * 4`;
    `if m + n < p_256k1 then &(m + n) else &(m + n) - &p_256k1:real`] THEN
  REPEAT CONJ_TAC THENL
   [CONV_TAC NUM_REDUCE_CONV THEN BOUNDER_TAC[];
    REWRITE_TAC[p_256k1] THEN ARITH_TAC;
    REWRITE_TAC[p_256k1] THEN ARITH_TAC;
    ALL_TAC;
    ASM_SIMP_TAC[MOD_ADD_CASES; GSYM NOT_LE; COND_SWAP] THEN
    COND_CASES_TAC THEN ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_256k1] THEN REAL_ARITH_TAC] THEN
  ABBREV_TAC `q <=> m + n < p_256k1` THEN
  UNDISCH_THEN `2 EXP 256 * bitval carry_s8 + l = m + n`
   (SUBST1_TAC o SYM) THEN
  EXPAND_TAC "l" THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN
  REWRITE_TAC[WORD_AND_MASK; GSYM NOT_LE] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist; p_256k1] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC WORD_REDUCE_CONV THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC);;

let BIGNUM_ADD_P256K1_SUBROUTINE_CORRECT = time prove
 (`!z x y m n pc stackpointer returnaddress.
        nonoverlapping (word pc,0x65) (z,8 * 4) /\
        nonoverlapping (stackpointer,8) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_add_p256k1_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSP; RSI; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_add_p256k1_mc BIGNUM_ADD_P256K1_CORRECT);;


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

let windows_bignum_add_p256k1_mc = define_from_elf
   "windows_bignum_add_p256k1_mc" "x86/secp256k1/bignum_add_p256k1.obj";;

let WINDOWS_BIGNUM_ADD_P256K1_SUBROUTINE_CORRECT = time prove
 (`!z x y m n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0x72); (x,8 * 4); (y,8 * 4)] /\
        nonoverlapping (word pc,0x72) (z,8 * 4) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_add_p256k1_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  WINDOWS_C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSP; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC windows_bignum_add_p256k1_mc
    bignum_add_p256k1_mc BIGNUM_ADD_P256K1_CORRECT);;

 ========================================================================= 
 Addition modulo p_256k1, the field characteristic for secp256k1.          
 ========================================================================= 
*** print_literal_from_elf "x86/secp256k1/bignum_add_p256k1.o";;
 ***
 AND (% rax) (% r9) 
 AND (% rax) (% r10) 
 ADC (% rax) (Imm8 (word 0)) 
 NOT (% rsi) 
 CMOVE (% rsi) (% rdx) 
 ADD (% rcx) (% rsi) 
 ADC (% r8) (Imm8 (word 0)) 
 ADC (% r9) (Imm8 (word 0)) 
 ADC (% r10) (Imm8 (word 0)) 
 ------------------------------------------------------------------------- 
 Proof.                                                                    
 ------------------------------------------------------------------------- 
 ------------------------------------------------------------------------- 
 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_add_p256k1_mc = define_assert_from_elf "bignum_add_p256k1_mc" "x86/secp256k1/bignum_add_p256k1.o"
[
  MOV ( % rcx ) (   ( % % ( rsi,0 ) ) )
  ADD ( % rcx ) (   ( % % ( rdx,0 ) ) )
  MOV ( % r8 ) (   ( % % ( rsi,8 ) ) )
  ADC ( % r8 ) (   ( % % ( rdx,8 ) ) )
  MOV ( % r9 ) (   ( % % ( rsi,16 ) ) )
  ADC ( % r9 ) (   ( % % ( rdx,16 ) ) )
  MOV ( % r10 ) (   ( % % ( rsi,24 ) ) )
  ADC ( % r10 ) (   ( % % ( rdx,24 ) ) )
  SBB ( % rdx ) ( % rdx )
  MOV ( % rax ) ( % r8 )
  0x48; 0xbe; 0x2e; 0xfc; 0xff; 0xff; 0xfe; 0xff; 0xff; 0xff;
  MOV ( % rsi ) ( Imm64 ( word 18446744069414583342 ) )
  CMP ( % rsi ) ( % rcx )
  SBB ( % rdx ) ( Imm8 ( word 0 ) )
  MOV (   ( % % ( rdi,0 ) ) ) ( % rcx )
  MOV (   ( % % ( rdi,8 ) ) ) ( % r8 )
  MOV (   ( % % ( rdi,16 ) ) ) ( % r9 )
  MOV (   ( % % (  ) ) ) ( % r10 )
  RET
];;

let BIGNUM_ADD_P256K1_EXEC = X86_MK_CORE_EXEC_RULE bignum_add_p256k1_mc;;


let p_256k1 = new_definition `p_256k1 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F`;;

let BIGNUM_ADD_P256K1_CORRECT = time prove
 (`!z x y m n pc.
        nonoverlapping (word pc,0x65) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_add_p256k1_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = word (pc + 0x64) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSI; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`z:int64`; `x:int64`; `y:int64`; `m:num`; `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
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "m_" `read (memory :> bytes (x,8 * 4)) s0` THEN
  BIGNUM_DIGITIZE_TAC "n_" `read (memory :> bytes (y,8 * 4)) s0` THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC [2;4;6;8] (1--9) THEN
  ABBREV_TAC `l = bignum_of_wordlist [sum_s2; sum_s4; sum_s6; sum_s8]` THEN
  SUBGOAL_THEN `2 EXP 256 * bitval carry_s8 + l = m + n` ASSUME_TAC THENL
   [MAP_EVERY EXPAND_TAC ["l"; "m"; "n"] THEN
    REWRITE_TAC[bignum_of_wordlist; MULT_CLAUSES; ADD_CLAUSES] THEN
    REWRITE_TAC[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;
    RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC (14--15) (10--18) THEN
  RULE_ASSUM_TAC(SIMP_RULE[ADD_CLAUSES; VAL_EQ_0]) THEN
  SUBGOAL_THEN
   `word_sub (word_neg (word (bitval carry_s8))) (word (bitval carry_s15)) =
    (word 0:int64)<=>
    m + n < p_256k1`
  SUBST_ALL_TAC THENL
   [REWRITE_TAC[WORD_RULE
     `word_sub (word_neg x) y = word 0 <=> word_add x y = word 0`] THEN
    REWRITE_TAC[GSYM VAL_EQ_0] THEN
   REWRITE_TAC[VAL_WORD_ADD_CASES; VAL_WORD_BITVAL; DIMINDEX_64] THEN
    SIMP_TAC[ADD_EQ_0; BITVAL_EQ_0; BITVAL_BOUND; ARITH_RULE
     `a <= 1 /\ b <= 1 ==> a + b < 2 EXP 64`] THEN
    FIRST_X_ASSUM(fun th ->
     GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [SYM th]) THEN
    ASM_CASES_TAC `carry_s8:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THENL
     [REWRITE_TAC[p_256k1] THEN ARITH_TAC; ALL_TAC] THEN
    REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; GSYM NOT_LE] THEN AP_TERM_TAC THEN
    TRANS_TAC EQ_TRANS `2 EXP 256 <= l + 4294968273` THEN CONJ_TAC THENL
     [ALL_TAC; REWRITE_TAC[p_256k1] THEN ARITH_TAC] THEN
    TRANS_TAC EQ_TRANS
     `2 EXP 128 <=
      bignum_of_wordlist[sum_s2; word_and (word_and sum_s4 sum_s6) sum_s8] +
      4294968273` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC FLAG_FROM_CARRY_LE THEN EXISTS_TAC `128` THEN
      REWRITE_TAC[bignum_of_wordlist; MULT_CLAUSES; ADD_CLAUSES] THEN
      REWRITE_TAC[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 BOUNDER_TAC[];
      ALL_TAC] THEN
    EXPAND_TAC "l" THEN ONCE_REWRITE_TAC[bignum_of_wordlist] THEN
    MATCH_MP_TAC(ARITH_RULE
     `l < 2 EXP 64 /\ (a < 2 EXP 64 - 1 <=> h < 2 EXP 192 - 1) /\
      (~(h < 2 EXP 192 - 1)
       ==> (2 EXP 128 <= (l + 2 EXP 64 * a) + 4294968273 <=>
            2 EXP 256 <= (l + 2 EXP 64 * h) + 4294968273))
      ==> (2 EXP 128 <= (l + 2 EXP 64 * a) + 4294968273 <=>
           2 EXP 256 <= (l + 2 EXP 64 * h) + 4294968273)`) THEN
    SIMP_TAC[VAL_BOUND_64; BIGNUM_OF_WORDLIST_LT_MAX; LENGTH;
             ARITH_MULT; ARITH_ADD; ARITH_SUC; EX; DE_MORGAN_THM;
             WORD_BITWISE_RULE
              `word_and a b = word_not(word 0) <=>
               a = word_not(word 0) /\ b = word_not(word 0)`] THEN
    REWRITE_TAC[DISJ_ACI] THEN DISCH_TAC THEN
    ASM_REWRITE_TAC[bignum_of_wordlist] THEN CONV_TAC WORD_REDUCE_CONV THEN
    ARITH_TAC;
    RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP]) THEN
    ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN

  X86_ACCSTEPS_TAC BIGNUM_ADD_P256K1_EXEC [19;21;23;25] (19--26) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN
  ASM_REWRITE_TAC[] THEN DISCARD_STATE_TAC "s23" THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC EQUAL_FROM_CONGRUENT_MOD_MOD THEN
  MAP_EVERY EXISTS_TAC
   [`64 * 4`;
    `if m + n < p_256k1 then &(m + n) else &(m + n) - &p_256k1:real`] THEN
  REPEAT CONJ_TAC THENL
   [CONV_TAC NUM_REDUCE_CONV THEN BOUNDER_TAC[];
    REWRITE_TAC[p_256k1] THEN ARITH_TAC;
    REWRITE_TAC[p_256k1] THEN ARITH_TAC;
    ALL_TAC;
    ASM_SIMP_TAC[MOD_ADD_CASES; GSYM NOT_LE; COND_SWAP] THEN
    COND_CASES_TAC THEN ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; p_256k1] THEN REAL_ARITH_TAC] THEN
  ABBREV_TAC `q <=> m + n < p_256k1` THEN
  UNDISCH_THEN `2 EXP 256 * bitval carry_s8 + l = m + n`
   (SUBST1_TAC o SYM) THEN
  EXPAND_TAC "l" THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN
  REWRITE_TAC[WORD_AND_MASK; GSYM NOT_LE] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist; p_256k1] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC WORD_REDUCE_CONV THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC);;

let BIGNUM_ADD_P256K1_SUBROUTINE_CORRECT = time prove
 (`!z x y m n pc stackpointer returnaddress.
        nonoverlapping (word pc,0x65) (z,8 * 4) /\
        nonoverlapping (stackpointer,8) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_add_p256k1_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSP; RSI; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_add_p256k1_mc BIGNUM_ADD_P256K1_CORRECT);;



let windows_bignum_add_p256k1_mc = define_from_elf
   "windows_bignum_add_p256k1_mc" "x86/secp256k1/bignum_add_p256k1.obj";;

let WINDOWS_BIGNUM_ADD_P256K1_SUBROUTINE_CORRECT = time prove
 (`!z x y m n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0x72); (x,8 * 4); (y,8 * 4)] /\
        nonoverlapping (word pc,0x72) (z,8 * 4) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 4)
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_add_p256k1_mc /\
                  read RIP s = word pc /\
                  read RSP s = stackpointer /\
                  read (memory :> bytes64 stackpointer) s = returnaddress /\
                  WINDOWS_C_ARGUMENTS [z; x; y] s /\
                  bignum_from_memory (x,4) s = m /\
                  bignum_from_memory (y,4) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (m < p_256k1 /\ n < p_256k1
                   ==> bignum_from_memory (z,4) s = (m + n) MOD p_256k1))
          (MAYCHANGE [RIP; RSP; RDX; RAX; RCX; R8; R9; R10] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC windows_bignum_add_p256k1_mc
    bignum_add_p256k1_mc BIGNUM_ADD_P256K1_CORRECT);;
