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

(* ========================================================================= *)
  Mapping out of reduced Montgomery representation mod p_521 .               
(* ========================================================================= *)

(**** print_literal_from_elf "x86/p521/bignum_demont_p521.o";;
 ****)

let bignum_demont_p521_mc = define_assert_from_elf "bignum_demont_p521_mc" "x86/p521/bignum_demont_p521.o"
[
  MOV ( % rdx ) (   ( % % ( rsi,0 ) ) )
  MOV ( % rax ) ( % rdx )
  MOV ( % rcx ) (   ( % % ( rsi,8 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,0 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,16 ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,8 ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % ( rsi,24 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  SHL ( % rax ) ( Imm8 ( word 9 ) )
  MOV (   ( % % ( rdi,16 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % (  ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % (  ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % ( rsi,40 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,32 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,48 ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,40 ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % (  ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,48 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,64 ) ) )
  OR ( % rdx ) ( % rax )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % (  ) ) ) ( % rcx )
  SHR ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,64 ) ) ) ( % rdx )
  RET

];;

let BIGNUM_DEMONT_P521_EXEC = X86_MK_CORE_EXEC_RULE bignum_demont_p521_mc;;

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

let p_521 = new_definition `p_521 = 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151`;;

let P_521 = prove
 (`p_521 = 2 EXP 521 - 1`,
  REWRITE_TAC[p_521] THEN CONV_TAC NUM_REDUCE_CONV);;

let P_521_AS_WORDLIST = prove
 (`p_521 =
   bignum_of_wordlist
    [word_not(word 0);word_not(word 0);word_not(word 0);word_not(word 0);
     word_not(word 0);word_not(word 0);word_not(word 0);word_not(word 0);
     word(0x1FF)]`,
  REWRITE_TAC[p_521; bignum_of_wordlist] THEN
  CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV);;

let BIGNUM_FROM_MEMORY_EQ_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] = p_521 <=>
   (!i. i < 64
        ==> bit i n0 /\ bit i n1 /\ bit i n2 /\ bit i n3 /\
            bit i n4 /\ bit i n5 /\ bit i n6 /\ bit i n7) /\
   (!i. i < 9 ==> bit i n8) /\ (!i. i < 64 ==> 9 <= i ==> ~bit i n8)`,
  REWRITE_TAC[P_521_AS_WORDLIST; BIGNUM_OF_WORDLIST_EQ] THEN
  REWRITE_TAC[WORD_EQ_BITS_ALT; DIMINDEX_64] THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_CASES_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC WORD_REDUCE_CONV THEN
  CONV_TAC CONJ_ACI_RULE);;

let BIGNUM_FROM_MEMORY_LE_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] <= p_521 <=>
   !i. i < 64 ==> 9 <= i ==> ~bit i n8`,
  SIMP_TAC[P_521; ARITH_RULE `p_521 = 2 EXP 521 - 1 ==>
    (n <= p_521 <=> n DIV 2 EXP (8 * 64) < 2 EXP 9)`] THEN
  REWRITE_TAC[TOP_DEPTH_CONV num_CONV `8`; MULT_CLAUSES; EXP_ADD] THEN
  REWRITE_TAC[GSYM DIV_DIV; BIGNUM_OF_WORDLIST_DIV; EXP; DIV_1] THEN
  REWRITE_TAC[BIGNUM_OF_WORDLIST_SING; GSYM UPPER_BITS_ZERO] THEN
  MP_TAC(ISPEC `n8:int64` BIT_TRIVIAL) THEN REWRITE_TAC[DIMINDEX_64] THEN
  MESON_TAC[NOT_LE]);;

let BIGNUM_FROM_MEMORY_LT_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] < p_521 <=>
   (!i. i < 64 ==> 9 <= i ==> ~bit i n8) /\
   ~((!i. i < 64
          ==> bit i n0 /\ bit i n1 /\ bit i n2 /\ bit i n3 /\
              bit i n4 /\ bit i n5 /\ bit i n6 /\ bit i n7) /\
     (!i. i < 9 ==> bit i n8))`,
  GEN_REWRITE_TAC LAND_CONV [LT_LE] THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_EQ_P521; BIGNUM_FROM_MEMORY_LE_P521] THEN
  MESON_TAC[]);;

let BIGNUM_DEMONT_P521_CORRECT = time prove
 (`!z x n pc.
        nonoverlapping (word pc,0x7d) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_demont_p521_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,9) s = n)
             (\s. read RIP s = word (pc + 0x7c) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9)])`,
  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
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_LDIGITIZE_TAC "n_" `read (memory :> bytes (x,8 * 9)) s0` THEN
  X86_STEPS_TAC BIGNUM_DEMONT_P521_EXEC (1--30) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  DISCH_TAC THEN CONV_TAC SYM_CONV THEN REWRITE_TAC[MOD_UNIQUE] THEN
  CONV_TAC(ONCE_DEPTH_CONV BIGNUM_LEXPAND_CONV) THEN
  UNDISCH_TAC `n < p_521` THEN EXPAND_TAC "n" THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_LT_P521; bignum_of_wordlist] THEN
  ASM_REWRITE_TAC[DIMINDEX_64] THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_CASES_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC
   (LABEL_TAC "*" o CONV_RULE(RAND_CONV CONJ_CANON_CONV))) THEN
  REWRITE_TAC[val_def; DIMINDEX_64; bignum_of_wordlist] THEN
  REWRITE_TAC[ARITH_RULE `i < 64 <=> 0 <= i /\ i <= 63`] THEN
  REWRITE_TAC[GSYM IN_NUMSEG; IN_GSPEC] THEN
  REWRITE_TAC[BIT_WORD_SUBWORD; BIT_WORD_JOIN; BIT_WORD_OR; BIT_WORD_1;
              BIT_WORD_USHR; BIT_WORD_SHL; DIMINDEX_64; DIMINDEX_128] THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV EXPAND_NSUM_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV CONJ_CANON_CONV))) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
  `!e. (e * i == 1) (mod p) /\ (e * x == n) (mod p)
       ==> (i * n == x) (mod p)`) THEN
  EXISTS_TAC `2 EXP 576` THEN
  REWRITE_TAC[GSYM(NUM_REDUCE_CONV `2 EXP 576`); INVERSE_MOD_RMUL_EQ] THEN
  REWRITE_TAC[COPRIME_REXP; COPRIME_2; p_521] THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[REAL_CONGRUENCE] THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
  REAL_INTEGER_TAC);;

let BIGNUM_DEMONT_P521_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        nonoverlapping (word pc,0x7d) (z,8 * 9) /\
        nonoverlapping (stackpointer,8) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_demont_p521_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,9) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RSP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_demont_p521_mc
    BIGNUM_DEMONT_P521_CORRECT);;

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

let windows_bignum_demont_p521_mc = define_from_elf
   "windows_bignum_demont_p521_mc" "x86/p521/bignum_demont_p521.obj";;

let WINDOWS_BIGNUM_DEMONT_P521_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0x87); (x,8 * 9)] /\
        nonoverlapping (word pc,0x87) (z,8 * 9) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_demont_p521_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,9) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RSP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC windows_bignum_demont_p521_mc
    bignum_demont_p521_mc BIGNUM_DEMONT_P521_CORRECT);;

 ========================================================================= 
 ========================================================================= 
*** print_literal_from_elf "x86/p521/bignum_demont_p521.o";;
 ***
 ------------------------------------------------------------------------- 
 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
 *)

  Mapping out of reduced Montgomery representation mod p_521 .               


let bignum_demont_p521_mc = define_assert_from_elf "bignum_demont_p521_mc" "x86/p521/bignum_demont_p521.o"
[
  MOV ( % rdx ) (   ( % % ( rsi,0 ) ) )
  MOV ( % rax ) ( % rdx )
  MOV ( % rcx ) (   ( % % ( rsi,8 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,0 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,16 ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,8 ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % ( rsi,24 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  SHL ( % rax ) ( Imm8 ( word 9 ) )
  MOV (   ( % % ( rdi,16 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % (  ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % (  ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % ( rsi,40 ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,32 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,48 ) ) )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,40 ) ) ) ( % rcx )
  MOV ( % rcx ) (   ( % % (  ) ) )
  0x48; 0x0f; 0xac; 0xca; 0x37;
  SHRD ( % rdx ) ( % rcx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,48 ) ) ) ( % rdx )
  MOV ( % rdx ) (   ( % % ( rsi,64 ) ) )
  OR ( % rdx ) ( % rax )
  0x48; 0x0f; 0xac; 0xd1; 0x37;
  SHRD ( % rcx ) ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % (  ) ) ) ( % rcx )
  SHR ( % rdx ) ( Imm8 ( word 55 ) )
  MOV (   ( % % ( rdi,64 ) ) ) ( % rdx )
  RET

];;

let BIGNUM_DEMONT_P521_EXEC = X86_MK_CORE_EXEC_RULE bignum_demont_p521_mc;;


let p_521 = new_definition `p_521 = 6864797660130609714981900799081393217269435300143305409394463459185543183397656052122559640661454554977296311391480858037121987999716643812574028291115057151`;;

let P_521 = prove
 (`p_521 = 2 EXP 521 - 1`,
  REWRITE_TAC[p_521] THEN CONV_TAC NUM_REDUCE_CONV);;

let P_521_AS_WORDLIST = prove
 (`p_521 =
   bignum_of_wordlist
    [word_not(word 0);word_not(word 0);word_not(word 0);word_not(word 0);
     word_not(word 0);word_not(word 0);word_not(word 0);word_not(word 0);
     word(0x1FF)]`,
  REWRITE_TAC[p_521; bignum_of_wordlist] THEN
  CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV);;

let BIGNUM_FROM_MEMORY_EQ_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] = p_521 <=>
   (!i. i < 64
        ==> bit i n0 /\ bit i n1 /\ bit i n2 /\ bit i n3 /\
            bit i n4 /\ bit i n5 /\ bit i n6 /\ bit i n7) /\
   (!i. i < 9 ==> bit i n8) /\ (!i. i < 64 ==> 9 <= i ==> ~bit i n8)`,
  REWRITE_TAC[P_521_AS_WORDLIST; BIGNUM_OF_WORDLIST_EQ] THEN
  REWRITE_TAC[WORD_EQ_BITS_ALT; DIMINDEX_64] THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_CASES_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC WORD_REDUCE_CONV THEN
  CONV_TAC CONJ_ACI_RULE);;

let BIGNUM_FROM_MEMORY_LE_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] <= p_521 <=>
   !i. i < 64 ==> 9 <= i ==> ~bit i n8`,
  SIMP_TAC[P_521; ARITH_RULE `p_521 = 2 EXP 521 - 1 ==>
    (n <= p_521 <=> n DIV 2 EXP (8 * 64) < 2 EXP 9)`] THEN
  REWRITE_TAC[TOP_DEPTH_CONV num_CONV `8`; MULT_CLAUSES; EXP_ADD] THEN
  REWRITE_TAC[GSYM DIV_DIV; BIGNUM_OF_WORDLIST_DIV; EXP; DIV_1] THEN
  REWRITE_TAC[BIGNUM_OF_WORDLIST_SING; GSYM UPPER_BITS_ZERO] THEN
  MP_TAC(ISPEC `n8:int64` BIT_TRIVIAL) THEN REWRITE_TAC[DIMINDEX_64] THEN
  MESON_TAC[NOT_LE]);;

let BIGNUM_FROM_MEMORY_LT_P521 = prove
 (`bignum_of_wordlist[n0;n1;n2;n3;n4;n5;n6;n7;n8] < p_521 <=>
   (!i. i < 64 ==> 9 <= i ==> ~bit i n8) /\
   ~((!i. i < 64
          ==> bit i n0 /\ bit i n1 /\ bit i n2 /\ bit i n3 /\
              bit i n4 /\ bit i n5 /\ bit i n6 /\ bit i n7) /\
     (!i. i < 9 ==> bit i n8))`,
  GEN_REWRITE_TAC LAND_CONV [LT_LE] THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_EQ_P521; BIGNUM_FROM_MEMORY_LE_P521] THEN
  MESON_TAC[]);;

let BIGNUM_DEMONT_P521_CORRECT = time prove
 (`!z x n pc.
        nonoverlapping (word pc,0x7d) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) (BUTLAST bignum_demont_p521_mc) /\
                  read RIP s = word pc /\
                  C_ARGUMENTS [z; x] s /\
                  bignum_from_memory (x,9) s = n)
             (\s. read RIP s = word (pc + 0x7c) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9)])`,
  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
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN
  BIGNUM_LDIGITIZE_TAC "n_" `read (memory :> bytes (x,8 * 9)) s0` THEN
  X86_STEPS_TAC BIGNUM_DEMONT_P521_EXEC (1--30) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  DISCH_TAC THEN CONV_TAC SYM_CONV THEN REWRITE_TAC[MOD_UNIQUE] THEN
  CONV_TAC(ONCE_DEPTH_CONV BIGNUM_LEXPAND_CONV) THEN
  UNDISCH_TAC `n < p_521` THEN EXPAND_TAC "n" THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_LT_P521; bignum_of_wordlist] THEN
  ASM_REWRITE_TAC[DIMINDEX_64] THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_CASES_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC
   (LABEL_TAC "*" o CONV_RULE(RAND_CONV CONJ_CANON_CONV))) THEN
  REWRITE_TAC[val_def; DIMINDEX_64; bignum_of_wordlist] THEN
  REWRITE_TAC[ARITH_RULE `i < 64 <=> 0 <= i /\ i <= 63`] THEN
  REWRITE_TAC[GSYM IN_NUMSEG; IN_GSPEC] THEN
  REWRITE_TAC[BIT_WORD_SUBWORD; BIT_WORD_JOIN; BIT_WORD_OR; BIT_WORD_1;
              BIT_WORD_USHR; BIT_WORD_SHL; DIMINDEX_64; DIMINDEX_128] THEN
  CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC(ONCE_DEPTH_CONV EXPAND_NSUM_CONV) THEN
  CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN
  CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV CONJ_CANON_CONV))) THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(NUMBER_RULE
  `!e. (e * i == 1) (mod p) /\ (e * x == n) (mod p)
       ==> (i * n == x) (mod p)`) THEN
  EXISTS_TAC `2 EXP 576` THEN
  REWRITE_TAC[GSYM(NUM_REDUCE_CONV `2 EXP 576`); INVERSE_MOD_RMUL_EQ] THEN
  REWRITE_TAC[COPRIME_REXP; COPRIME_2; p_521] THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[REAL_CONGRUENCE] THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
  REAL_INTEGER_TAC);;

let BIGNUM_DEMONT_P521_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        nonoverlapping (word pc,0x7d) (z,8 * 9) /\
        nonoverlapping (stackpointer,8) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) bignum_demont_p521_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,9) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RSP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9)])`,
  X86_PROMOTE_RETURN_NOSTACK_TAC bignum_demont_p521_mc
    BIGNUM_DEMONT_P521_CORRECT);;


let windows_bignum_demont_p521_mc = define_from_elf
   "windows_bignum_demont_p521_mc" "x86/p521/bignum_demont_p521.obj";;

let WINDOWS_BIGNUM_DEMONT_P521_SUBROUTINE_CORRECT = time prove
 (`!z x n pc stackpointer returnaddress.
        ALL (nonoverlapping (word_sub stackpointer (word 16),16))
            [(word pc,0x87); (x,8 * 9)] /\
        nonoverlapping (word pc,0x87) (z,8 * 9) /\
        nonoverlapping (word_sub stackpointer (word 16),24) (z,8 * 9) /\
        (x = z \/ nonoverlapping(x,8 * 9) (z,8 * 9))
        ==> ensures x86
             (\s. bytes_loaded s (word pc) windows_bignum_demont_p521_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,9) s = n)
             (\s. read RIP s = returnaddress /\
                  read RSP s = word_add stackpointer (word 8) /\
                  (n < p_521
                   ==> bignum_from_memory (z,9) s =
                       (inverse_mod p_521 (2 EXP 576) * n) MOD p_521))
          (MAYCHANGE [RIP; RSP; RAX; RDX; RCX] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,9);
                      memory :> bytes(word_sub stackpointer (word 16),16)])`,
  WINDOWS_X86_WRAP_NOSTACK_TAC windows_bignum_demont_p521_mc
    bignum_demont_p521_mc BIGNUM_DEMONT_P521_CORRECT);;
