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

(* ========================================================================= *)
(* Little-endian transformation (just copying in this little-endian model).  *)
  There are three different correctness variants corresponding to the three
  aliases with different types ( littleendian , fromlebytes and tolebytes ) .   
(* ========================================================================= *)

(**** print_literal_from_elf "arm/p256/bignum_littleendian_4.o";;
 ****)

let bignum_littleendian_4_mc =
  define_assert_from_elf "bignum_littleendian_4_mc" "arm/p256/bignum_littleendian_4.o"
[
  arm_LDRB   ( Immediate_Offset ( word 0 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 1 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 2 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 3 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 4 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 5 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 6 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 7 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 0 ) )
  arm_LDRB   ( Immediate_Offset ( word 8) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 9 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 10 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 11 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 12 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 13 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 14 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 15 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 16 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 17 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 18 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 19 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 20 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 21 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 22 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 23 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 16 ) )
  arm_LDRB   ( Immediate_Offset ( word 24 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 25 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 26 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 27 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 28 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 29 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 30 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 31 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 24 ) )
  arm_RET X30
];;

let BIGNUM_LITTLEENDIAN_4_EXEC = ARM_MK_EXEC_RULE bignum_littleendian_4_mc;;

(* ------------------------------------------------------------------------- *)
(* Proof as a "fromlebytes" function.                                          *)
(* ------------------------------------------------------------------------- *)

let BIGNUM_FROMLEBYTES_4_CORRECT = time prove
 (`!z x l pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                read (memory :> bytelist(x,32)) s = l)
           (\s. read PC s = word (pc + 0x110) /\
                bignum_from_memory(z,4) s = num_of_bytelist l)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `l:byte list`; `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
  BYTELIST_DIGITIZE_TAC "b_" `read (memory :> bytelist (x,32)) s0` THEN
  ARM_STEPS_TAC BIGNUM_LITTLEENDIAN_4_EXEC (1--68) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  EXPAND_TAC "l" THEN REWRITE_TAC[num_of_bytelist; val_def] THEN
  ASM_REWRITE_TAC[] THEN REWRITE_TAC[num_of_bytelist; val_def] THEN
  REWRITE_TAC[DIMINDEX_8; ARITH_RULE `i < 8 <=> 0 <= i /\ i <= 7`] THEN
  REWRITE_TAC[DIMINDEX_64; ARITH_RULE `i < 64 <=> 0 <= i /\ i <= 63`] THEN
  REWRITE_TAC[GSYM IN_NUMSEG; IN_GSPEC] THEN CONV_TAC NUM_REDUCE_CONV THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_NSUM_CONV) THEN
  REWRITE_TAC[BIT_WORD_SUBWORD; BIT_WORD_JOIN; BIT_WORD_ZX] THEN
  REWRITE_TAC[DIMINDEX_128; DIMINDEX_64; DIMINDEX_32; DIMINDEX_8] THEN
  CONV_TAC NUM_REDUCE_CONV THEN ARITH_TAC);;

let BIGNUM_FROMLEBYTES_4_SUBROUTINE_CORRECT = time prove
 (`!z x l pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                read (memory :> bytelist(x,32)) s = l)
           (\s. read PC s = returnaddress /\
                bignum_from_memory (z,4) s = num_of_bytelist l)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_FROMLEBYTES_4_CORRECT);;

(* ------------------------------------------------------------------------- *)
(* As a "tolebytes" function.                                                  *)
(* ------------------------------------------------------------------------- *)

let BIGNUM_TOLEBYTES_4_CORRECT = time prove
 (`!z x n pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = word (pc + 0x110) /\
                read (memory :> bytelist(z,32)) s = bytelist_of_num 32 n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
  ONCE_REWRITE_TAC[READ_BYTES_EQ_BYTELIST; READ_BYTELIST_EQ_BYTES] THEN
  REWRITE_TAC[LENGTH_BYTELIST_OF_NUM] THEN
  MP_TAC(ISPECL [`z:int64`; `x:int64`; `bytelist_of_num 32 n`; `pc:num`]
        BIGNUM_FROMLEBYTES_4_CORRECT) THEN
  ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
  CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
  MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ENSURES_PRECONDITION_THM) THEN
  SIMP_TAC[]);;

let BIGNUM_TOLEBYTES_4_SUBROUTINE_CORRECT = time prove
 (`!z x n pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = returnaddress /\
                read (memory :> bytelist(z,32)) s = bytelist_of_num 32 n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_TOLEBYTES_4_CORRECT);;

(* ------------------------------------------------------------------------- *)
(* As a bignum-to-bignum operation.                                          *)
(* ------------------------------------------------------------------------- *)

let BIGNUM_LITTLEENDIAN_4_CORRECT = time prove
 (`!z x n pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = word (pc + 0x110) /\
                bignum_from_memory(z,4) s = n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  BIGNUM_TERMRANGE_TAC `4` `n:num` THEN
  GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV o ONCE_DEPTH_CONV)
        [BIGNUM_FROM_MEMORY_BYTES] THEN
  REWRITE_TAC[READ_BYTES_EQ_BYTELIST] THEN
  CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
  MP_TAC(ISPECL [`z:int64`; `x:int64`; `bytelist_of_num 32 n`; `pc:num`]
        BIGNUM_FROMLEBYTES_4_CORRECT) THEN
  ASM_SIMP_TAC[NUM_OF_BYTELIST_OF_NUM; MOD_LT;
               ARITH_RULE `256 EXP 32 = 2 EXP (64 * 4)`]);;

let BIGNUM_LITTLEENDIAN_4_SUBROUTINE_CORRECT = time prove
 (`!z x n pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = returnaddress /\
                bignum_from_memory(z,4) s = n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_LITTLEENDIAN_4_CORRECT);;

 ========================================================================= 
 Little-endian transformation (just copying in this little-endian model).  
 ========================================================================= 
*** print_literal_from_elf "arm/p256/bignum_littleendian_4.o";;
 ***
 ------------------------------------------------------------------------- 
 Proof as a "fromlebytes" function.                                          
 ------------------------------------------------------------------------- 
 ------------------------------------------------------------------------- 
 As a "tolebytes" function.                                                  
 ------------------------------------------------------------------------- 
 ------------------------------------------------------------------------- 
 As a bignum-to-bignum operation.                                          
 ------------------------------------------------------------------------- 

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

  There are three different correctness variants corresponding to the three
  aliases with different types ( littleendian , fromlebytes and tolebytes ) .   


let bignum_littleendian_4_mc =
  define_assert_from_elf "bignum_littleendian_4_mc" "arm/p256/bignum_littleendian_4.o"
[
  arm_LDRB   ( Immediate_Offset ( word 0 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 1 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 2 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 3 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 4 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 5 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 6 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 7 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 0 ) )
  arm_LDRB   ( Immediate_Offset ( word 8) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 9 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 10 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 11 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 12 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 13 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 14 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 15 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 16 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 17 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 18 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 19 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 20 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 21 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 22 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 23 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 16 ) )
  arm_LDRB   ( Immediate_Offset ( word 24 ) )
  arm_EXTR X3 X2 XZR ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 25 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 26 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 27 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 28 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 29 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 30 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_LDRB   ( Immediate_Offset ( word 31 ) )
  arm_EXTR X3 X2 X3 ( rvalue ( word 8) )
  arm_STR   ( Immediate_Offset ( word 24 ) )
  arm_RET X30
];;

let BIGNUM_LITTLEENDIAN_4_EXEC = ARM_MK_EXEC_RULE bignum_littleendian_4_mc;;


let BIGNUM_FROMLEBYTES_4_CORRECT = time prove
 (`!z x l pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                read (memory :> bytelist(x,32)) s = l)
           (\s. read PC s = word (pc + 0x110) /\
                bignum_from_memory(z,4) s = num_of_bytelist l)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `l:byte list`; `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
  BYTELIST_DIGITIZE_TAC "b_" `read (memory :> bytelist (x,32)) s0` THEN
  ARM_STEPS_TAC BIGNUM_LITTLEENDIAN_4_EXEC (1--68) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  EXPAND_TAC "l" THEN REWRITE_TAC[num_of_bytelist; val_def] THEN
  ASM_REWRITE_TAC[] THEN REWRITE_TAC[num_of_bytelist; val_def] THEN
  REWRITE_TAC[DIMINDEX_8; ARITH_RULE `i < 8 <=> 0 <= i /\ i <= 7`] THEN
  REWRITE_TAC[DIMINDEX_64; ARITH_RULE `i < 64 <=> 0 <= i /\ i <= 63`] THEN
  REWRITE_TAC[GSYM IN_NUMSEG; IN_GSPEC] THEN CONV_TAC NUM_REDUCE_CONV THEN
  CONV_TAC(ONCE_DEPTH_CONV EXPAND_NSUM_CONV) THEN
  REWRITE_TAC[BIT_WORD_SUBWORD; BIT_WORD_JOIN; BIT_WORD_ZX] THEN
  REWRITE_TAC[DIMINDEX_128; DIMINDEX_64; DIMINDEX_32; DIMINDEX_8] THEN
  CONV_TAC NUM_REDUCE_CONV THEN ARITH_TAC);;

let BIGNUM_FROMLEBYTES_4_SUBROUTINE_CORRECT = time prove
 (`!z x l pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                read (memory :> bytelist(x,32)) s = l)
           (\s. read PC s = returnaddress /\
                bignum_from_memory (z,4) s = num_of_bytelist l)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_FROMLEBYTES_4_CORRECT);;


let BIGNUM_TOLEBYTES_4_CORRECT = time prove
 (`!z x n pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = word (pc + 0x110) /\
                read (memory :> bytelist(z,32)) s = bytelist_of_num 32 n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
  ONCE_REWRITE_TAC[READ_BYTES_EQ_BYTELIST; READ_BYTELIST_EQ_BYTES] THEN
  REWRITE_TAC[LENGTH_BYTELIST_OF_NUM] THEN
  MP_TAC(ISPECL [`z:int64`; `x:int64`; `bytelist_of_num 32 n`; `pc:num`]
        BIGNUM_FROMLEBYTES_4_CORRECT) THEN
  ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN
  CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
  MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ENSURES_PRECONDITION_THM) THEN
  SIMP_TAC[]);;

let BIGNUM_TOLEBYTES_4_SUBROUTINE_CORRECT = time prove
 (`!z x n pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = returnaddress /\
                read (memory :> bytelist(z,32)) s = bytelist_of_num 32 n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_TOLEBYTES_4_CORRECT);;


let BIGNUM_LITTLEENDIAN_4_CORRECT = time prove
 (`!z x n pc.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = word (pc + 0x110) /\
                bignum_from_memory(z,4) s = n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  REPEAT GEN_TAC THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  BIGNUM_TERMRANGE_TAC `4` `n:num` THEN
  GEN_REWRITE_TAC (RATOR_CONV o LAND_CONV o ONCE_DEPTH_CONV)
        [BIGNUM_FROM_MEMORY_BYTES] THEN
  REWRITE_TAC[READ_BYTES_EQ_BYTELIST] THEN
  CONV_TAC(ONCE_DEPTH_CONV NUM_MULT_CONV) THEN
  MP_TAC(ISPECL [`z:int64`; `x:int64`; `bytelist_of_num 32 n`; `pc:num`]
        BIGNUM_FROMLEBYTES_4_CORRECT) THEN
  ASM_SIMP_TAC[NUM_OF_BYTELIST_OF_NUM; MOD_LT;
               ARITH_RULE `256 EXP 32 = 2 EXP (64 * 4)`]);;

let BIGNUM_LITTLEENDIAN_4_SUBROUTINE_CORRECT = time prove
 (`!z x n pc returnaddress.
      nonoverlapping (word pc,0x114) (z,8 * 4) /\
      (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4))
      ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_littleendian_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [z; x] s /\
                bignum_from_memory(x,4) s = n)
           (\s. read PC s = returnaddress /\
                bignum_from_memory(z,4) s = n)
          (MAYCHANGE [PC; X2; X3] ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_LITTLEENDIAN_4_EXEC
    BIGNUM_LITTLEENDIAN_4_CORRECT);;
