diff options
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 | ||||
| -rw-r--r-- | riscv/coq.patch | 20 |
2 files changed, 1 insertions, 20 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 7a9d16be..eaf75840 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1071,6 +1071,7 @@ Ltac solve_arithfact := (* Attempt a simple proof first to avoid lengthy preparation steps (especially as the large proof terms can upset subsequent proofs). *) intros; (* To solve implications for derive_m *) +try (exact trivial_range); try fill_in_evar_eq; try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end; try (constructor; omega); diff --git a/riscv/coq.patch b/riscv/coq.patch index 983b7ac1..17398e36 100644 --- a/riscv/coq.patch +++ b/riscv/coq.patch @@ -78,26 +78,6 @@ (match w__7 with | PTW_Failure (f) => returnm ((TR39_Failure (f)) : TR39_Result ) | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) => -@@ -8681,7 +8683,7 @@ - | Sbare => returnm ((TR_Address (vAddr)) : TR_Result ) - | SV39 => - translate39 (subrange_vec_dec vAddr 38 0) ac effPriv mxr do_sum -- (build_ex (projT1 (sub_range (build_ex SV39_LEVELS) (build_ex 1)))) >>= fun w__7 : TR39_Result => -+ (build_ex ( (Z.sub ( SV39_LEVELS) ( 1)))) >>= fun w__7 : TR39_Result => - returnm ((match w__7 with - | TR39_Address (pa) => TR_Address (EXTZ 64 pa) - | TR39_Failure (f) => TR_Failure (translationException ac f) -@@ -12178,8 +12180,8 @@ - if sumbool_of_bool ((andb s - (Z.gtb q (projT1 (sub_range (build_ex (projT1 (pow2 31))) (build_ex 1)))))) - then -- projT1 (sub_range (build_ex 0) -- (build_ex (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) -+ (Z.sub ( 0) -+ ( (projT1 ((build_ex (projT1 (ex_int (pow 2 31)))) - : {n : Z & ArithFact (True)})))) - else q in - wX @@ -12374,138 +12376,144 @@ returnm (true : bool). |