Library mcertikos.objects.CalTicketLock

Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import GlobIdent.
Require Import GlobalOracle.

Opaque Z.of_nat Z.to_nat Z.to_pos.

Fixpoint real_lock_pb (i :nat) (tlp :Lock) : Lock :=
  match i with
  | O ⇒ tlp
  | S x ⇒ ZMap.set (Z.of_nat x) LockFalse (real_lock_pb x tlp)
  end.

Definition real_lock (tlp: Lock) : Lock :=
  real_lock_pb (Z.to_nat lock_range) tlp.

Fixpoint real_multi_log_pb (i :nat) (tlp : MultiLogPool) : MultiLogPool :=
  match i with
  | O ⇒ tlp
  | S x ⇒ ZMap.set (Z.of_nat x) (MultiDef nil) (real_multi_log_pb x tlp)
  end.

Definition real_multi_log (tlp: MultiLogPool) : MultiLogPool :=
  real_multi_log_pb (Z.to_nat lock_range) tlp.


Lemma real_multi_log_pb_in:
  ∀ n i l,
    (0 ≤ i < n)%nat →
    ZMap.get (Z.of_nat i) (real_multi_log_pb n l) = MultiDef nil.
Proof.
  induction n; intros i l Hlelt; [omega|].
  simpl; destruct (eq_nat_dec i n); subst.
  - rewrite ZMap.gss; reflexivity.
  - rewrite ZMap.gso.
    apply IHn; omega.
    rewrite Nat2Z.inj_iff; assumption.
Qed.

Lemma real_multi_log_pb_notin:
  ∀ n i l,
    (i < 0 ∨ Z.of_nat n ≤ i)%Z →
    ZMap.get i (real_multi_log_pb n l) = ZMap.get i l.
Proof.
  induction n; intros i l [Hlt|Hle]; simpl; auto.
  - destruct (zeq i (Z.of_nat n)); subst.
    + assert (Hcon:= Nat2Z.is_nonneg n); omega.
    + rewrite ZMap.gso; auto.
  - rewrite Nat2Z.inj_succ in Hle.
    destruct (zeq i (Z.of_nat n)); subst; try omega.
    rewrite ZMap.gso; auto; apply IHn; omega.
Qed.