diff options
Diffstat (limited to 'aarch64/aarch64_extras.v')
| -rw-r--r-- | aarch64/aarch64_extras.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v index 94851ef5..67d165cd 100644 --- a/aarch64/aarch64_extras.v +++ b/aarch64/aarch64_extras.v @@ -133,4 +133,12 @@ Definition read_ram {rv e} addrsize size `{ArithFact (size >= 0)} (hexRAM : mwor (*val elf_entry : unit -> integer*) Definition elf_entry (_:unit) := 0. (*declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` -*)
\ No newline at end of file +*) + +Lemma mul_quot_8_helper : forall x, 8 * x = 8 * (Z.quot (8 * x) 8). +intro. +rewrite Z.mul_comm. +rewrite Z.quot_mul; auto with zarith. +Qed. +Hint Resolve mul_quot_8_helper : sail. + |