diff options
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ee4a9b51..225c3e98 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -366,10 +366,23 @@ Qed. Hint Resolve arith_op_eq_correct: wlp. Opaque arith_op_eq_correct. +Definition offset_eq (ofs1 ofs2 : offset): ?? bool := + RET (Ptrofs.eq ofs1 ofs2). + +Lemma offset_eq_correct ofs1 ofs2: + WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2. +Proof. + wlp_simplify. + pose (Ptrofs.eq_spec ofs1 ofs2). + rewrite H in *. + trivial. +Qed. +Hint Resolve offset_eq_correct: wlp. + Definition load_op_eq (o1 o2: load_op): ?? bool := match o1 with | OLoadRRO n1 ofs1 => - match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end | OLoadRRR n1 => match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end | OLoadRRRXS n1 => @@ -380,26 +393,14 @@ Lemma load_op_eq_correct o1 o2: WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. destruct o1, o2; wlp_simplify; try discriminate. - - congruence. + - f_equal. pose (Ptrofs.eq_spec ofs ofs0). + rewrite H in *. trivial. - congruence. - congruence. Qed. Hint Resolve load_op_eq_correct: wlp. Opaque load_op_eq_correct. -Definition offset_eq (ofs1 ofs2 : offset): ?? bool := - RET (Ptrofs.eq ofs1 ofs2). - -Lemma offset_eq_correct ofs1 ofs2: - WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2. -Proof. - wlp_simplify. - pose (Ptrofs.eq_spec ofs1 ofs2). - rewrite H in *. - trivial. -Qed. -Hint Resolve offset_eq_correct: wlp. - Definition store_op_eq (o1 o2: store_op): ?? bool := match o1 with | OStoreRRO n1 ofs1 => |