diff options
Diffstat (limited to 'src/BoundedArithmetic/Interface.v')
| -rw-r--r-- | src/BoundedArithmetic/Interface.v | 168 |
1 files changed, 123 insertions, 45 deletions
diff --git a/src/BoundedArithmetic/Interface.v b/src/BoundedArithmetic/Interface.v index 4a14a160b..fe64cd37e 100644 --- a/src/BoundedArithmetic/Interface.v +++ b/src/BoundedArithmetic/Interface.v @@ -53,18 +53,32 @@ Section InstructionGallery. decode_shift_left_immediate : forall r count, 0 <= count < n -> decode (shl r count) = (decode r << count) mod 2^n. - Record spread_left_immediate := { sprl :> W -> imm -> W * W (* [(high, low)] *) }. + Record shift_right_immediate := { shr :> W -> imm -> W }. + + Class is_shift_right_immediate (shr : shift_right_immediate) := + decode_shift_right_immediate : + forall r count, 0 <= count < n -> decode (shr r count) = (decode r >> count). + + Record spread_left_immediate := { sprl :> W -> imm -> W * W (* [(low, high)] *) }. Class is_spread_left_immediate (sprl : spread_left_immediate) := { decode_fst_spread_left_immediate : forall r count, - 0 <= count < n - -> decode (fst (sprl r count)) = (decode r << count) >> n; - decode_snd_spread_left_immediate : forall r count, 0 <= count < n - -> decode (snd (sprl r count)) = (decode r << count) mod 2^n + -> decode (fst (sprl r count)) = (decode r << count) mod 2^n; + decode_snd_spread_left_immediate : forall r count, + 0 <= count < n + -> decode (snd (sprl r count)) = (decode r << count) >> n; + }. + Definition Build_is_spread_left_immediate' (sprl : spread_left_immediate) + (pf : forall r count, 0 <= count < n + -> decode (fst (sprl r count)) = (decode r << count) mod 2^n + /\ decode (snd (sprl r count)) = (decode r << count) >> n) + := {| decode_fst_spread_left_immediate r count H := proj1 (pf r count H); + decode_snd_spread_left_immediate r count H := proj2 (pf r count H) |}. + Record mask_keep_low := { mkl :> W -> imm -> W }. Class is_mask_keep_low (mkl : mask_keep_low) := @@ -81,6 +95,11 @@ Section InstructionGallery. decode_snd_add_with_carry : forall x y c, decode (snd (adc x y c)) = (decode x + decode y + bit c) mod (2^n) }. + Definition Build_is_add_with_carry' (adc : add_with_carry) + (pf : forall x y c, bit (fst (adc x y c)) = (decode x + decode y + bit c) >> n /\ decode (snd (adc x y c)) = (decode x + decode y + bit c) mod (2^n)) + := {| bit_fst_add_with_carry x y c := proj1 (pf x y c); + decode_snd_add_with_carry x y c := proj2 (pf x y c) |}. + Record sub_with_carry := { subc :> W -> W -> bool -> bool * W }. Class is_sub_with_carry (subc:W->W->bool->bool*W) := @@ -89,6 +108,11 @@ Section InstructionGallery. decode_snd_sub_with_carry : forall x y c, decode (snd (subc x y c)) = (decode x - decode y - bit c) mod 2^n }. + Definition Build_is_sub_with_carry' (subc : sub_with_carry) + (pf : forall x y c, fst (subc x y c) = ((decode x - decode y - bit c) <? 0) /\ decode (snd (subc x y c)) = (decode x - decode y - bit c) mod 2^n) + := {| fst_sub_with_carry x y c := proj1 (pf x y c); + decode_snd_sub_with_carry x y c := proj2 (pf x y c) |}. + Record multiply := { mul :> W -> W -> W }. Class is_mul (mul : multiply) := @@ -118,12 +142,15 @@ Section InstructionGallery. Class is_add_modulo (addm : add_modulo) := decode_add_modulo : forall x y modulus, - decode (addm x y modulus) = (decode x + decode y) mod (decode modulus). + decode (addm x y modulus) = (if (decode x + decode y) <? decode modulus + then (decode x + decode y) + else (decode x + decode y) - decode modulus)%Z. End InstructionGallery. Global Arguments load_immediate : clear implicits. Global Arguments shift_right_doubleword_immediate : clear implicits. Global Arguments shift_left_immediate : clear implicits. +Global Arguments shift_right_immediate : clear implicits. Global Arguments spread_left_immediate : clear implicits. Global Arguments mask_keep_low : clear implicits. Global Arguments add_with_carry : clear implicits. @@ -137,6 +164,7 @@ Global Arguments add_modulo : clear implicits. Global Arguments ldi {_ _} _. Global Arguments shrd {_ _} _ _ _. Global Arguments shl {_ _} _ _. +Global Arguments shr {_ _} _ _. Global Arguments sprl {_ _} _ _. Global Arguments mkl {_ _} _ _. Global Arguments adc {_ _} _ _ _. @@ -151,6 +179,7 @@ Global Arguments addm {_ _} _ _ _. Existing Class load_immediate. Existing Class shift_right_doubleword_immediate. Existing Class shift_left_immediate. +Existing Class shift_right_immediate. Existing Class spread_left_immediate. Existing Class mask_keep_low. Existing Class add_with_carry. @@ -166,6 +195,7 @@ Global Arguments is_decode {_ _} _. Global Arguments is_load_immediate {_ _ _} _. Global Arguments is_shift_right_doubleword_immediate {_ _ _} _. Global Arguments is_shift_left_immediate {_ _ _} _. +Global Arguments is_shift_right_immediate {_ _ _} _. Global Arguments is_spread_left_immediate {_ _ _} _. Global Arguments is_mask_keep_low {_ _ _} _. Global Arguments is_add_with_carry {_ _ _} _. @@ -177,45 +207,91 @@ Global Arguments is_mul_high_high {_ _ _} _ _. Global Arguments is_select_conditional {_ _ _} _. Global Arguments is_add_modulo {_ _ _} _. -Ltac bounded_sovlver_tac := - solve [ eassumption | typeclasses eauto | omega | auto 6 using decode_range with typeclass_instances omega ]. - -Hint Rewrite @decode_load_immediate @decode_shift_right_doubleword @decode_shift_left_immediate @decode_fst_spread_left_immediate @decode_snd_spread_left_immediate @decode_mask_keep_low @bit_fst_add_with_carry @decode_snd_add_with_carry @fst_sub_with_carry @decode_snd_sub_with_carry @decode_mul @decode_mul_low_low @decode_mul_high_low @decode_mul_high_high @decode_select_conditional @decode_add_modulo using bounded_sovlver_tac : push_decode. - -Ltac push_decode := - repeat first [ erewrite !decode_load_immediate by bounded_sovlver_tac - | erewrite !decode_shift_right_doubleword by bounded_sovlver_tac - | erewrite !decode_shift_left_immediate by bounded_sovlver_tac - | erewrite !decode_fst_spread_left_immediate by bounded_sovlver_tac - | erewrite !decode_snd_spread_left_immediate by bounded_sovlver_tac - | erewrite !decode_mask_keep_low by bounded_sovlver_tac - | erewrite !bit_fst_add_with_carry by bounded_sovlver_tac - | erewrite !decode_snd_add_with_carry by bounded_sovlver_tac - | erewrite !fst_sub_with_carry by bounded_sovlver_tac - | erewrite !decode_snd_sub_with_carry by bounded_sovlver_tac - | erewrite !decode_mul by bounded_sovlver_tac - | erewrite !decode_mul_low_low by bounded_sovlver_tac - | erewrite !decode_mul_high_low by bounded_sovlver_tac - | erewrite !decode_mul_high_high by bounded_sovlver_tac - | erewrite !decode_select_conditional by bounded_sovlver_tac - | erewrite !decode_add_modulo by bounded_sovlver_tac ]. -Ltac pull_decode := - repeat first [ erewrite <- !decode_load_immediate by bounded_sovlver_tac - | erewrite <- !decode_shift_right_doubleword by bounded_sovlver_tac - | erewrite <- !decode_shift_left_immediate by bounded_sovlver_tac - | erewrite <- !decode_fst_spread_left_immediate by bounded_sovlver_tac - | erewrite <- !decode_snd_spread_left_immediate by bounded_sovlver_tac - | erewrite <- !decode_mask_keep_low by bounded_sovlver_tac - | erewrite <- !bit_fst_add_with_carry by bounded_sovlver_tac - | erewrite <- !decode_snd_add_with_carry by bounded_sovlver_tac - | erewrite <- !fst_sub_with_carry by bounded_sovlver_tac - | erewrite <- !decode_snd_sub_with_carry by bounded_sovlver_tac - | erewrite <- !decode_mul by bounded_sovlver_tac - | erewrite <- !decode_mul_low_low by bounded_sovlver_tac - | erewrite <- !decode_mul_high_low by bounded_sovlver_tac - | erewrite <- !decode_mul_high_high by bounded_sovlver_tac - | erewrite <- !decode_select_conditional by bounded_sovlver_tac - | erewrite <- !decode_add_modulo by bounded_sovlver_tac ]. +Ltac bounded_solver_tac := + solve [ eassumption | typeclasses eauto | omega ]. + +Lemma decode_proj n W (dec : W -> Z) + : @decode n W {| decode := dec |} = dec. +Proof. reflexivity. Qed. + +Lemma decode_exponent_nonnegative {n W} (decode : decoder n W) {isdecode : is_decode decode} + (isinhabited : W) + : 0 <= n. +Proof. + pose proof (decode_range isinhabited). + assert (0 < 2^n) by omega. + destruct (Z_lt_ge_dec n 0) as [H'|]; [ | omega ]. + assert (2^n = 0) by auto using Z.pow_neg_r. + omega. +Qed. + +Hint Rewrite @decode_load_immediate @decode_shift_right_doubleword @decode_shift_left_immediate @decode_shift_right_immediate @decode_fst_spread_left_immediate @decode_snd_spread_left_immediate @decode_mask_keep_low @bit_fst_add_with_carry @decode_snd_add_with_carry @fst_sub_with_carry @decode_snd_sub_with_carry @decode_mul @decode_mul_low_low @decode_mul_high_low @decode_mul_high_high @decode_select_conditional @decode_add_modulo @decode_proj using bounded_solver_tac : push_decode. + +Ltac push_decode_step := + first [ rewrite !decode_proj + | erewrite !decode_load_immediate by bounded_solver_tac + | erewrite !decode_shift_right_doubleword by bounded_solver_tac + | erewrite !decode_shift_left_immediate by bounded_solver_tac + | erewrite !decode_shift_right_immediate by bounded_solver_tac + | erewrite !decode_fst_spread_left_immediate by bounded_solver_tac + | erewrite !decode_snd_spread_left_immediate by bounded_solver_tac + | erewrite !decode_mask_keep_low by bounded_solver_tac + | erewrite !bit_fst_add_with_carry by bounded_solver_tac + | erewrite !decode_snd_add_with_carry by bounded_solver_tac + | erewrite !fst_sub_with_carry by bounded_solver_tac + | erewrite !decode_snd_sub_with_carry by bounded_solver_tac + | erewrite !decode_mul by bounded_solver_tac + | erewrite !decode_mul_low_low by bounded_solver_tac + | erewrite !decode_mul_high_low by bounded_solver_tac + | erewrite !decode_mul_high_high by bounded_solver_tac + | erewrite !decode_select_conditional by bounded_solver_tac + | erewrite !decode_add_modulo by bounded_solver_tac ]. +Ltac pull_decode_step := + first [ erewrite <- !decode_load_immediate by bounded_solver_tac + | erewrite <- !decode_shift_right_doubleword by bounded_solver_tac + | erewrite <- !decode_shift_left_immediate by bounded_solver_tac + | erewrite <- !decode_shift_right_immediate by bounded_solver_tac + | erewrite <- !decode_fst_spread_left_immediate by bounded_solver_tac + | erewrite <- !decode_snd_spread_left_immediate by bounded_solver_tac + | erewrite <- !decode_mask_keep_low by bounded_solver_tac + | erewrite <- !bit_fst_add_with_carry by bounded_solver_tac + | erewrite <- !decode_snd_add_with_carry by bounded_solver_tac + | erewrite <- !fst_sub_with_carry by bounded_solver_tac + | erewrite <- !decode_snd_sub_with_carry by bounded_solver_tac + | erewrite <- !decode_mul by bounded_solver_tac + | erewrite <- !decode_mul_low_low by bounded_solver_tac + | erewrite <- !decode_mul_high_low by bounded_solver_tac + | erewrite <- !decode_mul_high_high by bounded_solver_tac + | erewrite <- !decode_select_conditional by bounded_solver_tac + | erewrite <- !decode_add_modulo by bounded_solver_tac ]. +Ltac push_decode := repeat push_decode_step. +Ltac pull_decode := repeat pull_decode_step. + +(* We take special care to handle the case where the decoder is + syntactically different but the decoded expression is judgmentally + the same; we don't want to split apart variables that should be the + same. *) +Ltac set_decode_step check := + match goal with + | [ |- context G[@Interface.decode ?n ?W ?dr ?w] ] + => check w; + first [ match goal with + | [ d := @Interface.decode _ _ _ w |- _ ] + => change (@Interface.decode n W dr w) with d + end + | generalize (@decode_range n W dr _ w); + let d := fresh "d" in + set (d := @Interface.decode n W dr w); + intro ] + end. +Ltac set_decode check := repeat set_decode_step check. +Ltac clearbody_decode := + repeat match goal with + | [ H := @Interface.decode _ _ _ _ |- _ ] => clearbody H + end. +Ltac generalize_decode_by check := set_decode check; clearbody_decode. +Ltac generalize_decode := generalize_decode_by ltac:(fun w => idtac). +Ltac generalize_decode_var := generalize_decode_by ltac:(fun w => is_var w). Module fancy_machine. Local Notation imm := Z (only parsing). @@ -227,6 +303,7 @@ Module fancy_machine. ldi :> load_immediate W; shrd :> shift_right_doubleword_immediate W; shl :> shift_left_immediate W; + shr :> shift_right_immediate W; mkl :> mask_keep_low W; adc :> add_with_carry W; subc :> sub_with_carry W; @@ -243,6 +320,7 @@ Module fancy_machine. load_immediate :> is_load_immediate ldi; shift_right_doubleword_immediate :> is_shift_right_doubleword_immediate shrd; shift_left_immediate :> is_shift_left_immediate shl; + shift_right_immediate :> is_shift_right_immediate shr; mask_keep_low :> is_mask_keep_low mkl; add_with_carry :> is_add_with_carry adc; sub_with_carry :> is_sub_with_carry subc; |