Module PAC

Require Import Values.
Require Import AST.
Require Linear.

Inductive pac_kind := PAC_NONE.

Definition choose_pac_kind (f : Linear.function) := PAC_NONE.


Definition pointer_auth_encode (kind : pac_kind) (ptr modifier : val) := ptr.

Lemma pointer_auth_Tptr :
  forall kind (ptr modifier : val),
    Val.has_type ptr Tptr -> Val.has_type modifier Tptr ->
    Val.has_type (pointer_auth_encode kind ptr modifier) Tptr.