Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Maps.
Require Import RealParams.
Require Import CommonTactic.
Require Import AuxLemma.

Instance sample_realparams_ops: RealParamsOps :=
  {
    real_mm := ZMap.set 0 (MMValid 0 1073745920 MMUsable) (ZMap.init MMUndef);
    real_size := 1;
    real_vmxinfo := ZMap.init 0
  }.

Global Instance sample_realparams: RealParams.
Proof.
  constructor.
  -
    unfold MM_valid, MM_range.
    intros. simpl in ×.
    destruct (zeq i 0); subst.
    + rewrite ZMap.gss.
      refine_split´; try reflexivity.
      omega.
    + omega.
  -
    unfold MM_correct.
    intros. simpl in ×.
    destruct (zeq i 0); subst.
    + destruct (zeq j 0); subst.
      × rewrite ZMap.gss in ×.
        inv H1. inv H2.
        constructor.
      × omega.
    + omega.
  -
    unfold MM_kern, MM_kern_range.
    intros.
    unfold MM_kern_valid. simpl.
    ∃ 0, 0, 1073745920.
    split. omega.
    split. rewrite ZMap.gss. reflexivity.
    split. omega.
    omega.
  -
    simpl. rewrite int_max.
    omega.
  - intros.
    simpl.
    rewrite ZMap.gi.
    unfold Integers.Int.max_unsigned.
    simpl.
    omega.
Qed.