Require Import VST.sepcomp.extspec.
Require Import VST.sepcomp.step_lemmas.
Require Import VST.veric.base.
(*Lenb - do we need these?
  Require Import VST.veric.Clight_new.
Require Import VST.veric.Clight_lemmas.*)
Require Import VST.veric.juicy_extspec.
Require Import VST.veric.juicy_mem.

Definition dryspec : external_specification juicy_mem external_function unit
  := Build_external_specification juicy_mem external_function unit
     (*ext_spec_type*)
     (fun ef => False)
     (*ext_spec_pre*)
     (fun ef Hef ge tys vl m z => False)
     (*ext_spec_post*)
     (fun ef Hef ge ty vl m z => False)
     (*ext_spec_exit*)
     (fun rv m z => False).

Definition Espec : OracleKind.
(* Goal: OracleKind *)
 refine (Build_OracleKind unit (Build_juicy_ext_spec _ dryspec _ _ _)).
Proof.
(* Goal: forall (e : external_function) (t : @ext_spec_type juicy_mem external_function unit dryspec e) (ge_s : injective_PTree block) (tret : option typ) (rv : option val) (z : unit), @predicates_hered.hereditary juicy_mem (@ageable.age juicy_mem juicy_mem_ageable) (@ext_spec_post juicy_mem external_function unit dryspec e t ge_s tret rv z) *)
(* Goal: forall (rv : option val) (z : unit), @predicates_hered.hereditary juicy_mem (@ageable.age juicy_mem juicy_mem_ageable) (@ext_spec_exit juicy_mem external_function unit dryspec rv z) *)
simpl; intros; contradiction.
(* Goal: forall (e : external_function) (t : @ext_spec_type juicy_mem external_function unit dryspec e) (ge_s : injective_PTree block) (tret : option typ) (rv : option val) (z : unit), @predicates_hered.hereditary juicy_mem (@ageable.age juicy_mem juicy_mem_ageable) (@ext_spec_post juicy_mem external_function unit dryspec e t ge_s tret rv z) *)
(* Goal: forall (rv : option val) (z : unit), @predicates_hered.hereditary juicy_mem (@ageable.age juicy_mem juicy_mem_ageable) (@ext_spec_exit juicy_mem external_function unit dryspec rv z) *)
simpl; intros; contradiction.
(* Goal: forall (rv : option val) (z : unit), @predicates_hered.hereditary juicy_mem (@ageable.age juicy_mem juicy_mem_ageable) (@ext_spec_exit juicy_mem external_function unit dryspec rv z) *)
simpl; intros; intros ? ? ? ?; contradiction.
Defined.

