Module DemoSpec

Require Import CoqlibC Maps.
Require Import ASTC Integers ValuesC EventsC Memory Globalenvs.
Require Import Op Registers.
Require Import sflib.
Require Import SmallstepC.
Require Export Simulation.
Require Import Skeleton Mod ModSem.
Require Import AsmC.
Require Import DemoHeader.

Set Implicit Arguments.

Local Obligation Tactic := ii; ss; des; inv_all_once; ss; clarify.

Section MODSEM.

  Definition prog : AST.program (AST.fundef (signature)) unit :=
    {| prog_defs :=
         [(func_id, Gfun (Internal ((mksignature [Tlong] (Some Tfloat) cc_default true))))];
       prog_public := [func_id; main_id];
       prog_main := main_id |}.

  Variable skenv_link: SkEnv.t.
  Variable p: unit.
  Let skenv: SkEnv.t := skenv_link.(SkEnv.project) prog.(Sk.of_program id).

  Record state := mkstate { get_arg: int64; get_mem: mem; }.

  Inductive initial_frame (args: Args.t): state -> Prop :=
  | initial_frame1_intro
      st
      (VS: args.(Args.vs) = [Vlong st.(get_arg)])
      (M: args.(Args.m) = st.(get_mem))
    :
      initial_frame args st
  .

  Inductive final_frame: state -> Retv.t -> Prop :=
  | final_frame_return
      st v_ret
      (SPEC: Val.floatoflongu (Vlong st.(get_arg)) = Some v_ret)
    :
      final_frame st (Retv.mk v_ret st.(get_mem))
  .

  Program Definition modsem: ModSem.t :=
    {|
      ModSem.state := state;
      ModSem.genvtype := unit;
      ModSem.step := bot5;
      ModSem.at_external := bot2;
      ModSem.initial_frame := initial_frame;
      ModSem.final_frame := final_frame;
      ModSem.after_external := bot3;
      ModSem.globalenv := tt;
      ModSem.skenv := skenv;
      ModSem.skenv_link := skenv_link;
    |}
  .

End MODSEM.

Program Definition module: Mod.t :=
  {| Mod.data := tt; Mod.get_sk := fun _ => prog; Mod.get_modsem := modsem; |}.