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

(* ========================================================================= *)
  8x8 - > 16 squaring , for uarchs with higher multiplier throughput .         
(* ========================================================================= *)

(**** print_literal_from_elf "arm/fastmul/bignum_sqr_8_16_alt.o";;
 ****)

let bignum_sqr_8_16_alt_mc = define_assert_from_elf "bignum_sqr_8_16_alt_mc" "arm/fastmul/bignum_sqr_8_16_alt.o"
[
  arm_STP X19 X20 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP X21 X22 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP X23 X24 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP    ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_LDP X2 X3 X1 ( Immediate_Offset ( iword ( & 0 ) ) )
  arm_MUL X11 X2 X3
  arm_UMULH X12 X2 X3
  arm_LDP X4 X5 X1 ( Immediate_Offset ( iword ( & 16 ) ) )
  arm_MUL X10 X2 X4
  arm_UMULH X13 X2 X4
  0xab0a018c;       (* arm_ADDS X12 X12 X10 *)
  arm_LDP X6 X7 X1 ( Immediate_Offset ( iword ( & 32 ) ) )
  arm_MUL X10 X2 X5
  arm_UMULH X14 X2 X5
  arm_ADCS X13 X13 X10
  arm_LDP X8 X9 X1 ( Immediate_Offset ( iword ( & 48 ) ) )
  arm_MUL X10 X2 X6
    X2 X6
  arm_ADCS X14 X14 X10
  arm_MUL X10 X2 X7
  arm_UMULH X16 X2 X7
  arm_ADCS X15 X15 X10
  arm_MUL X10 X2 X8
  arm_UMULH X17 X2 X8
  arm_ADCS X16 X16 X10
  arm_MUL X10 X2 X9
  arm_UMULH X19 X2 X9
  arm_ADCS X17 X17 X10
  0x9a1f0273;       (* arm_ADC X19 X19 XZR *)
  arm_MUL X10 X3 X4
  0xab0a01ad;       (* arm_ADDS X13 X13 X10 *)
  arm_MUL X10 X3 X5
  arm_ADCS X14 X14 X10
  arm_MUL X10 X3 X6
  arm_ADCS X15 X15 X10
  arm_MUL X10 X3 X7
  arm_ADCS X16 X16 X10
  arm_MUL X10 X3 X8
  arm_ADCS X17 X17 X10
  arm_MUL X10 X3 X9
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_CSET X20 
  arm_UMULH X10 X3 X4
  0xab0a01ce;       (* arm_ADDS X14 X14 X10 *)
  arm_UMULH X10 X3 X5
  arm_ADCS X15 X15 X10
  arm_UMULH X10 X3 X6
  arm_ADCS X16 X16 X10
  arm_UMULH X10 X3 X7
  arm_ADCS X17 X17 X10
  arm_UMULH X10 X3 X8
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_UMULH X10  
  0x9a0a0294;       (* arm_ADC X20 X20 X10 *)
  arm_MUL X10 X6 X7
  arm_UMULH X21 X6 X7
  0xab0a0294;       (* arm_ADDS X20 X20 X10 *)
  arm_ADC X21 X21 XZR
  arm_MUL X10 X4 X5
  0xab0a01ef;       (* arm_ADDS X15 X15 X10 *)
  arm_MUL X10 X4 X6
  arm_ADCS X16 X16 X10
  arm_MUL X10 X4 X7
  arm_ADCS X17 X17 X10
  arm_MUL X10 X4 X8
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_MUL X10 X4 X9
  0xba0a0294;       (* arm_ADCS X20 X20 X10 *)
  arm_MUL X10 X6 X8
  0xba0a02b5;       (* arm_ADCS X21 X21 X10 *)
  0x9a9f37f6;       (* arm_CSET X22 Condition_CS *)
  arm_UMULH X10 X4 X5
  arm_ADDS X16 X16 X10
  arm_UMULH X10 X4 X6
  arm_ADCS X17 X17 X10
  arm_UMULH X10 X4 X7
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_UMULH X10 X4 X8
  0xba0a0294;       (* arm_ADCS X20 X20 X10 *)
  arm_UMULH X10 X4 X9
  0xba0a02b5;       (* arm_ADCS X21 X21 X10 *)
  arm_UMULH X10 X6 X8
  arm_ADC   X10
  arm_MUL X10 X7 X8
  arm_UMULH X23 X7 X8
  0xab0a02d6;       (* arm_ADDS X22 X22 X10 *)
  arm_ADC   
  arm_MUL X10 X5 X6
  arm_ADDS X17 X17 X10
  arm_MUL X10 X5 X7
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_MUL X10 X5 X8
  0xba0a0294;       (* arm_ADCS X20 X20 X10 *)
  arm_MUL X10 X5 X9
  0xba0a02b5;       (* arm_ADCS X21 X21 X10 *)
  arm_MUL X10 X6 X9
  arm_ADCS X22 X22 X10
  arm_MUL X10 X7 X9
  arm_ADCS X23 X23 X10
  arm_CSET X24 Condition_CS
  arm_UMULH X10 X5 X6
  0xab0a0273;       (* arm_ADDS X19 X19 X10 *)
  arm_UMULH X10 X5 X7
  0xba0a0294;       (* arm_ADCS X20 X20 X10 *)
  arm_UMULH X10 X5 X8
  0xba0a02b5;       (* arm_ADCS X21 X21 X10 *)
  arm_UMULH X10 X5 X9
  arm_ADCS X22 X22 X10
  arm_UMULH X10 X6 X9
  arm_ADCS X23 X23 X10
  arm_UMULH X10 X7 X9
  arm_ADC X24 X24 X10
  arm_MUL X10 X8 X9
    X8 X9
  arm_ADDS X24 X24 X10
  arm_ADC   
  0xab0b016b;       (* arm_ADDS X11 X11 X11 *)
  arm_ADCS X12 X12 X12
  arm_ADCS X13 X13 X13
  arm_ADCS X14 X14 X14
  arm_ADCS   
  arm_ADCS X16 X16 X16
  arm_ADCS X17 X17 X17
  0xba130273;       (* arm_ADCS X19 X19 X19 *)
  0xba140294;       (* arm_ADCS X20 X20 X20 *)
  0xba1502b5;       (* arm_ADCS X21 X21 X21 *)
  arm_ADCS   
  arm_ADCS X23 X23 X23
  arm_ADCS X24 X24 X24
  arm_ADCS   
  0x9a9f37fa;       (* arm_CSET X26 Condition_CS *)
  arm_UMULH X10 X2 X2
  arm_MUL X2 X2 X2
  0xab0a016b;       (* arm_ADDS X11 X11 X10 *)
  arm_MUL X10 X3 X3
  arm_ADCS X12 X12 X10
  arm_UMULH X10 X3 X3
  arm_ADCS X13 X13 X10
  arm_MUL X10 X4 X4
  arm_ADCS X14 X14 X10
  arm_UMULH X10 X4 X4
  arm_ADCS X15 X15 X10
  arm_MUL X10 X5 X5
  arm_ADCS X16 X16 X10
  arm_UMULH X10 X5 X5
  arm_ADCS X17 X17 X10
  arm_MUL X10 X6 X6
  0xba0a0273;       (* arm_ADCS X19 X19 X10 *)
  arm_UMULH X10 X6 X6
  0xba0a0294;       (* arm_ADCS X20 X20 X10 *)
  arm_MUL X10 X7 X7
  0xba0a02b5;       (* arm_ADCS X21 X21 X10 *)
  arm_UMULH X10 X7 X7
  arm_ADCS X22 X22 X10
  arm_MUL X10 X8 X8
  arm_ADCS X23 X23 X10
  arm_UMULH X10 X8 X8
  arm_ADCS X24 X24 X10
  arm_MUL X10  
  arm_ADCS   X10
  arm_UMULH X10  
  arm_ADC   X10
  arm_STP X2 X11  ( Immediate_Offset ( iword ( & 0 ) ) )
  arm_STP X12 X13 X0 ( Immediate_Offset ( iword ( & 16 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 32 ) ) )
  arm_STP X16 X17  ( Immediate_Offset ( iword ( & 48 ) ) )
  arm_STP X19 X20  ( Immediate_Offset ( iword ( & 64 ) ) )
  arm_STP X21   ( Immediate_Offset ( iword ( & 80 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 96 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 112 ) ) )
  arm_LDP    ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP X23 X24 SP ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP    ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP X19 X20 SP ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_RET X30
];;

let BIGNUM_SQR_8_16_ALT_EXEC = ARM_MK_EXEC_RULE bignum_sqr_8_16_alt_mc;;

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

let BIGNUM_SQR_8_16_ALT_CORRECT = time prove
 (`!z x a pc.
     nonoverlapping (word pc,0x2bc) (z,8 * 16)
     ==> ensures arm
          (\s. aligned_bytes_loaded s (word pc) bignum_sqr_8_16_alt_mc /\
               read PC s = word(pc + 0x10) /\
               C_ARGUMENTS [z; x] s /\
               bignum_from_memory (x,8) s = a)
          (\s. read PC s = word (pc + 0x2a8) /\
               bignum_from_memory (z,16) s = a EXP 2)
          (MAYCHANGE [PC; X2; X3; X4; X5; X6; X7; X8; X9;
                      X10; X11; X12; X13; X14; X15; X16; X17; X19;
                      X20; X21; X22; X23; X24; X25; X26] ,,
           MAYCHANGE [memory :> bytes(z,8 * 16)] ,,
           MAYCHANGE SOME_FLAGS)`,
  MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `a:num`; `pc:num`] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "x_" `bignum_from_memory (x,8) s0` THEN
  ARM_ACCSTEPS_TAC BIGNUM_SQR_8_16_ALT_EXEC (1--166) (1--166) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[GSYM WORD_BITVAL; COND_SWAP]) THEN
  EXPAND_TAC "a" THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_ARITH_TAC);;

let BIGNUM_SQR_8_16_ALT_SUBROUTINE_CORRECT = time prove
 (`!z x a pc stackpointer returnaddress.
     aligned 16 stackpointer /\
     ALL (nonoverlapping (word_sub stackpointer (word 64),64))
         [(word pc,0x2bc); (z,8 * 16); (x,8 * 8)] /\
     nonoverlapping (word pc,0x2bc) (z,8 * 16)
     ==> ensures arm
          (\s. aligned_bytes_loaded s (word pc) bignum_sqr_8_16_alt_mc /\
               read PC s = word pc /\
               read SP s = stackpointer /\
               read X30 s = returnaddress /\
               C_ARGUMENTS [z; x] s /\
               bignum_from_memory (x,8) s = a)
          (\s. read PC s = returnaddress /\
               bignum_from_memory (z,16) s = a EXP 2)
          (MAYCHANGE [PC; X2; X3; X4; X5; X6; X7; X8; X9;
                      X10; X11; X12; X13; X14; X15; X16; X17] ,,
           MAYCHANGE [memory :> bytes(z,8 * 16);
                       memory :> bytes(word_sub stackpointer (word 64),64)] ,,
           MAYCHANGE SOME_FLAGS)`,
  ARM_ADD_RETURN_STACK_TAC
    BIGNUM_SQR_8_16_ALT_EXEC BIGNUM_SQR_8_16_ALT_CORRECT
    `[X19;X20;X21;X22;X23;X24;X25;X26]` 64);;

 ========================================================================= 
 ========================================================================= 
*** print_literal_from_elf "arm/fastmul/bignum_sqr_8_16_alt.o";;
 ***
 arm_ADDS X12 X12 X10 
 arm_ADC X19 X19 XZR 
 arm_ADDS X13 X13 X10 
 arm_ADCS X19 X19 X10 
 arm_ADDS X14 X14 X10 
 arm_ADCS X19 X19 X10 
 arm_ADC X20 X20 X10 
 arm_ADDS X20 X20 X10 
 arm_ADDS X15 X15 X10 
 arm_ADCS X19 X19 X10 
 arm_ADCS X20 X20 X10 
 arm_ADCS X21 X21 X10 
 arm_CSET X22 Condition_CS 
 arm_ADCS X19 X19 X10 
 arm_ADCS X20 X20 X10 
 arm_ADCS X21 X21 X10 
 arm_ADDS X22 X22 X10 
 arm_ADCS X19 X19 X10 
 arm_ADCS X20 X20 X10 
 arm_ADCS X21 X21 X10 
 arm_ADDS X19 X19 X10 
 arm_ADCS X20 X20 X10 
 arm_ADCS X21 X21 X10 
 arm_ADDS X11 X11 X11 
 arm_ADCS X19 X19 X19 
 arm_ADCS X20 X20 X20 
 arm_ADCS X21 X21 X21 
 arm_CSET X26 Condition_CS 
 arm_ADDS X11 X11 X10 
 arm_ADCS X19 X19 X10 
 arm_ADCS X20 X20 X10 
 arm_ADCS X21 X21 X10 
 ------------------------------------------------------------------------- 
 Proof.                                                                    
 ------------------------------------------------------------------------- 

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

  8x8 - > 16 squaring , for uarchs with higher multiplier throughput .         


let bignum_sqr_8_16_alt_mc = define_assert_from_elf "bignum_sqr_8_16_alt_mc" "arm/fastmul/bignum_sqr_8_16_alt.o"
[
  arm_STP X19 X20 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP X21 X22 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP X23 X24 SP ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_STP    ( Preimmediate_Offset ( iword ( -- & 16 ) ) )
  arm_LDP X2 X3 X1 ( Immediate_Offset ( iword ( & 0 ) ) )
  arm_MUL X11 X2 X3
  arm_UMULH X12 X2 X3
  arm_LDP X4 X5 X1 ( Immediate_Offset ( iword ( & 16 ) ) )
  arm_MUL X10 X2 X4
  arm_UMULH X13 X2 X4
  arm_LDP X6 X7 X1 ( Immediate_Offset ( iword ( & 32 ) ) )
  arm_MUL X10 X2 X5
  arm_UMULH X14 X2 X5
  arm_ADCS X13 X13 X10
  arm_LDP X8 X9 X1 ( Immediate_Offset ( iword ( & 48 ) ) )
  arm_MUL X10 X2 X6
    X2 X6
  arm_ADCS X14 X14 X10
  arm_MUL X10 X2 X7
  arm_UMULH X16 X2 X7
  arm_ADCS X15 X15 X10
  arm_MUL X10 X2 X8
  arm_UMULH X17 X2 X8
  arm_ADCS X16 X16 X10
  arm_MUL X10 X2 X9
  arm_UMULH X19 X2 X9
  arm_ADCS X17 X17 X10
  arm_MUL X10 X3 X4
  arm_MUL X10 X3 X5
  arm_ADCS X14 X14 X10
  arm_MUL X10 X3 X6
  arm_ADCS X15 X15 X10
  arm_MUL X10 X3 X7
  arm_ADCS X16 X16 X10
  arm_MUL X10 X3 X8
  arm_ADCS X17 X17 X10
  arm_MUL X10 X3 X9
  arm_CSET X20 
  arm_UMULH X10 X3 X4
  arm_UMULH X10 X3 X5
  arm_ADCS X15 X15 X10
  arm_UMULH X10 X3 X6
  arm_ADCS X16 X16 X10
  arm_UMULH X10 X3 X7
  arm_ADCS X17 X17 X10
  arm_UMULH X10 X3 X8
  arm_UMULH X10  
  arm_MUL X10 X6 X7
  arm_UMULH X21 X6 X7
  arm_ADC X21 X21 XZR
  arm_MUL X10 X4 X5
  arm_MUL X10 X4 X6
  arm_ADCS X16 X16 X10
  arm_MUL X10 X4 X7
  arm_ADCS X17 X17 X10
  arm_MUL X10 X4 X8
  arm_MUL X10 X4 X9
  arm_MUL X10 X6 X8
  arm_UMULH X10 X4 X5
  arm_ADDS X16 X16 X10
  arm_UMULH X10 X4 X6
  arm_ADCS X17 X17 X10
  arm_UMULH X10 X4 X7
  arm_UMULH X10 X4 X8
  arm_UMULH X10 X4 X9
  arm_UMULH X10 X6 X8
  arm_ADC   X10
  arm_MUL X10 X7 X8
  arm_UMULH X23 X7 X8
  arm_ADC   
  arm_MUL X10 X5 X6
  arm_ADDS X17 X17 X10
  arm_MUL X10 X5 X7
  arm_MUL X10 X5 X8
  arm_MUL X10 X5 X9
  arm_MUL X10 X6 X9
  arm_ADCS X22 X22 X10
  arm_MUL X10 X7 X9
  arm_ADCS X23 X23 X10
  arm_CSET X24 Condition_CS
  arm_UMULH X10 X5 X6
  arm_UMULH X10 X5 X7
  arm_UMULH X10 X5 X8
  arm_UMULH X10 X5 X9
  arm_ADCS X22 X22 X10
  arm_UMULH X10 X6 X9
  arm_ADCS X23 X23 X10
  arm_UMULH X10 X7 X9
  arm_ADC X24 X24 X10
  arm_MUL X10 X8 X9
    X8 X9
  arm_ADDS X24 X24 X10
  arm_ADC   
  arm_ADCS X12 X12 X12
  arm_ADCS X13 X13 X13
  arm_ADCS X14 X14 X14
  arm_ADCS   
  arm_ADCS X16 X16 X16
  arm_ADCS X17 X17 X17
  arm_ADCS   
  arm_ADCS X23 X23 X23
  arm_ADCS X24 X24 X24
  arm_ADCS   
  arm_UMULH X10 X2 X2
  arm_MUL X2 X2 X2
  arm_MUL X10 X3 X3
  arm_ADCS X12 X12 X10
  arm_UMULH X10 X3 X3
  arm_ADCS X13 X13 X10
  arm_MUL X10 X4 X4
  arm_ADCS X14 X14 X10
  arm_UMULH X10 X4 X4
  arm_ADCS X15 X15 X10
  arm_MUL X10 X5 X5
  arm_ADCS X16 X16 X10
  arm_UMULH X10 X5 X5
  arm_ADCS X17 X17 X10
  arm_MUL X10 X6 X6
  arm_UMULH X10 X6 X6
  arm_MUL X10 X7 X7
  arm_UMULH X10 X7 X7
  arm_ADCS X22 X22 X10
  arm_MUL X10 X8 X8
  arm_ADCS X23 X23 X10
  arm_UMULH X10 X8 X8
  arm_ADCS X24 X24 X10
  arm_MUL X10  
  arm_ADCS   X10
  arm_UMULH X10  
  arm_ADC   X10
  arm_STP X2 X11  ( Immediate_Offset ( iword ( & 0 ) ) )
  arm_STP X12 X13 X0 ( Immediate_Offset ( iword ( & 16 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 32 ) ) )
  arm_STP X16 X17  ( Immediate_Offset ( iword ( & 48 ) ) )
  arm_STP X19 X20  ( Immediate_Offset ( iword ( & 64 ) ) )
  arm_STP X21   ( Immediate_Offset ( iword ( & 80 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 96 ) ) )
  arm_STP    ( Immediate_Offset ( iword ( & 112 ) ) )
  arm_LDP    ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP X23 X24 SP ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP    ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_LDP X19 X20 SP ( Postimmediate_Offset ( iword ( & 16 ) ) )
  arm_RET X30
];;

let BIGNUM_SQR_8_16_ALT_EXEC = ARM_MK_EXEC_RULE bignum_sqr_8_16_alt_mc;;


let BIGNUM_SQR_8_16_ALT_CORRECT = time prove
 (`!z x a pc.
     nonoverlapping (word pc,0x2bc) (z,8 * 16)
     ==> ensures arm
          (\s. aligned_bytes_loaded s (word pc) bignum_sqr_8_16_alt_mc /\
               read PC s = word(pc + 0x10) /\
               C_ARGUMENTS [z; x] s /\
               bignum_from_memory (x,8) s = a)
          (\s. read PC s = word (pc + 0x2a8) /\
               bignum_from_memory (z,16) s = a EXP 2)
          (MAYCHANGE [PC; X2; X3; X4; X5; X6; X7; X8; X9;
                      X10; X11; X12; X13; X14; X15; X16; X17; X19;
                      X20; X21; X22; X23; X24; X25; X26] ,,
           MAYCHANGE [memory :> bytes(z,8 * 16)] ,,
           MAYCHANGE SOME_FLAGS)`,
  MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `a:num`; `pc:num`] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  ENSURES_INIT_TAC "s0" THEN
  BIGNUM_DIGITIZE_TAC "x_" `bignum_from_memory (x,8) s0` THEN
  ARM_ACCSTEPS_TAC BIGNUM_SQR_8_16_ALT_EXEC (1--166) (1--166) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[GSYM WORD_BITVAL; COND_SWAP]) THEN
  EXPAND_TAC "a" THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN
  ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN
  DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_ARITH_TAC);;

let BIGNUM_SQR_8_16_ALT_SUBROUTINE_CORRECT = time prove
 (`!z x a pc stackpointer returnaddress.
     aligned 16 stackpointer /\
     ALL (nonoverlapping (word_sub stackpointer (word 64),64))
         [(word pc,0x2bc); (z,8 * 16); (x,8 * 8)] /\
     nonoverlapping (word pc,0x2bc) (z,8 * 16)
     ==> ensures arm
          (\s. aligned_bytes_loaded s (word pc) bignum_sqr_8_16_alt_mc /\
               read PC s = word pc /\
               read SP s = stackpointer /\
               read X30 s = returnaddress /\
               C_ARGUMENTS [z; x] s /\
               bignum_from_memory (x,8) s = a)
          (\s. read PC s = returnaddress /\
               bignum_from_memory (z,16) s = a EXP 2)
          (MAYCHANGE [PC; X2; X3; X4; X5; X6; X7; X8; X9;
                      X10; X11; X12; X13; X14; X15; X16; X17] ,,
           MAYCHANGE [memory :> bytes(z,8 * 16);
                       memory :> bytes(word_sub stackpointer (word 64),64)] ,,
           MAYCHANGE SOME_FLAGS)`,
  ARM_ADD_RETURN_STACK_TAC
    BIGNUM_SQR_8_16_ALT_EXEC BIGNUM_SQR_8_16_ALT_CORRECT
    `[X19;X20;X21;X22;X23;X24;X25;X26]` 64);;
