Library mcertikos.layerlib.Z64Lemma

This file provide the tactic for refinement proof between layers

Require Import Coqlib.
Require Import Integers.

Definition Z64ofwords (i1 i2: Z) :=
  (Z.lor (Z.shiftl i1 32) i2).

Definition Z64_lo_int (i: Z) : int :=
  Int.repr i.

Definition Z64_hi_int (i: Z) : int :=
  Int.repr (Z.shiftr i 32).