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

(* ========================================================================= *)
  Multiplexing ( selection , if - then - else ) for 4 - digit ( 256 - bit ) bignums .     
(* ========================================================================= *)

* * * print_literal_from_elf " arm / p256 / bignum_mux_4.o " ; ; 
  * * *
 ****)

let bignum_mux_4_mc =
  define_assert_from_elf "bignum_mux_4_mc" "arm/p256/bignum_mux_4.o"
[
  arm_CMP  ( rvalue ( word 0 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 0 ) )
  arm_LDR   ( Immediate_Offset ( word 0 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 0 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 8) )
  arm_LDR   ( Immediate_Offset ( word 8) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 8) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 16 ) )
  arm_LDR   ( Immediate_Offset ( word 16 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 16 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 24 ) )
  arm_LDR   ( Immediate_Offset ( word 24 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 24 ) )
  arm_RET X30
];;

let BIGNUM_MUX_4_EXEC = ARM_MK_EXEC_RULE bignum_mux_4_mc;;

(* ------------------------------------------------------------------------- *)
(* Correctness proof.                                                        *)
(* ------------------------------------------------------------------------- *)

let BIGNUM_MUX_4_CORRECT = prove
 (`!p z x y m n pc.
     nonoverlapping (word pc,0x48) (z,8 * 4) /\
     (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4)) /\
     (y = z \/ nonoverlapping (y,8 * 4) (z,8 * 4))
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_mux_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [p; z; x; y] s /\
                bignum_from_memory (x,4) s = m /\
                bignum_from_memory (y,4) s = n)
           (\s. read PC s = word (pc + 0x44) /\
                bignum_from_memory (z,4) s =
                  if ~(p = word 0) then m else n)
          (MAYCHANGE [PC; X0; X4] ,, MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`p:int64`; `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
  ARM_STEPS_TAC BIGNUM_MUX_4_EXEC (1--17) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[WORD_SUB_0; VAL_EQ_0] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;

let BIGNUM_MUX_4_SUBROUTINE_CORRECT = prove
 (`!p z x y m n pc returnaddress.
     nonoverlapping (word pc,0x48) (z,8 * 4) /\
     (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4)) /\
     (y = z \/ nonoverlapping (y,8 * 4) (z,8 * 4))
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_mux_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [p; z; x; y] s /\
                bignum_from_memory (x,4) s = m /\
                bignum_from_memory (y,4) s = n)
           (\s. read PC s = returnaddress /\
                bignum_from_memory (z,4) s =
                  if ~(p = word 0) then m else n)
          (MAYCHANGE [PC; X0; X4] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_MUX_4_EXEC BIGNUM_MUX_4_CORRECT);;

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

  Multiplexing ( selection , if - then - else ) for 4 - digit ( 256 - bit ) bignums .     

* * * print_literal_from_elf " arm / p256 / bignum_mux_4.o " ; ; 
  * * *
 ****)

let bignum_mux_4_mc =
  define_assert_from_elf "bignum_mux_4_mc" "arm/p256/bignum_mux_4.o"
[
  arm_CMP  ( rvalue ( word 0 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 0 ) )
  arm_LDR   ( Immediate_Offset ( word 0 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 0 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 8) )
  arm_LDR   ( Immediate_Offset ( word 8) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 8) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 16 ) )
  arm_LDR   ( Immediate_Offset ( word 16 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 16 ) )
  arm_LDR X4 X2 ( Immediate_Offset ( word 24 ) )
  arm_LDR   ( Immediate_Offset ( word 24 ) )
  arm_CSEL X4 X4 X0 Condition_NE
  arm_STR X4 X1 ( Immediate_Offset ( word 24 ) )
  arm_RET X30
];;

let BIGNUM_MUX_4_EXEC = ARM_MK_EXEC_RULE bignum_mux_4_mc;;


let BIGNUM_MUX_4_CORRECT = prove
 (`!p z x y m n pc.
     nonoverlapping (word pc,0x48) (z,8 * 4) /\
     (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4)) /\
     (y = z \/ nonoverlapping (y,8 * 4) (z,8 * 4))
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_mux_4_mc /\
                read PC s = word pc /\
                C_ARGUMENTS [p; z; x; y] s /\
                bignum_from_memory (x,4) s = m /\
                bignum_from_memory (y,4) s = n)
           (\s. read PC s = word (pc + 0x44) /\
                bignum_from_memory (z,4) s =
                  if ~(p = word 0) then m else n)
          (MAYCHANGE [PC; X0; X4] ,, MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  MAP_EVERY X_GEN_TAC
   [`p:int64`; `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
  ARM_STEPS_TAC BIGNUM_MUX_4_EXEC (1--17) THEN
  ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
  CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[WORD_SUB_0; VAL_EQ_0] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;

let BIGNUM_MUX_4_SUBROUTINE_CORRECT = prove
 (`!p z x y m n pc returnaddress.
     nonoverlapping (word pc,0x48) (z,8 * 4) /\
     (x = z \/ nonoverlapping (x,8 * 4) (z,8 * 4)) /\
     (y = z \/ nonoverlapping (y,8 * 4) (z,8 * 4))
     ==> ensures arm
           (\s. aligned_bytes_loaded s (word pc) bignum_mux_4_mc /\
                read PC s = word pc /\
                read X30 s = returnaddress /\
                C_ARGUMENTS [p; z; x; y] s /\
                bignum_from_memory (x,4) s = m /\
                bignum_from_memory (y,4) s = n)
           (\s. read PC s = returnaddress /\
                bignum_from_memory (z,4) s =
                  if ~(p = word 0) then m else n)
          (MAYCHANGE [PC; X0; X4] ,,
           MAYCHANGE SOME_FLAGS ,,
           MAYCHANGE [memory :> bignum(z,4)])`,
  ARM_ADD_RETURN_NOSTACK_TAC BIGNUM_MUX_4_EXEC BIGNUM_MUX_4_CORRECT);;
