Require Import compcert.common.AST.
Require Import compcert.common.Memdata.
Require Import Coq.ZArith.ZArith.

(* LKSIZE should match sizeof(semax_conc.tlock).  *)
Definition LKSIZE:= (2 * size_chunk Mptr)%Z.
Definition LKSIZE_nat:= Z.to_nat LKSIZE.

Lemma LKSIZE_pos : (0 < LKSIZE)%Z.
Proof.
(* Goal: Z.lt Z0 LKSIZE *)
  unfold LKSIZE.
(* Goal: Z.lt Z0 (Z.mul (Zpos (xO xH)) (size_chunk Mptr)) *)
  pose proof (size_chunk_pos Mptr); omega.
Qed.

Lemma LKSIZE_int : (size_chunk Mint32 < LKSIZE)%Z.
Proof.
(* Goal: Z.lt (size_chunk Mint32) LKSIZE *)
  unfold LKSIZE; simpl.
(* Goal: Z.lt (Zpos (xO (xO xH))) match size_chunk Mptr with | Z0 => Z0 | Zpos y' => Zpos (xO y') | Zneg y' => Zneg (xO y') end *)
  rewrite size_chunk_Mptr; destruct Archi.ptr64; omega.
Qed.

Ltac lkomega := pose proof LKSIZE_pos; pose proof LKSIZE_int; simpl in *; try omega.
