Library mcertikos.ipc.IPCGenLinkSource

Require Import LinkSourceTemplate.
Require Import PIPCIntro.
Require Import PIPCIntroCSource.
Require Import GlobalOracleProp.
Require Import SingleOracle.

Section WITHCERTIKOS.

  Definition PIPC_module: link_module :=
    {|
      lm_cfun :=
        lcf syncsendto_chan_post f_syncsendto_chan ::
            lcf syncreceive_chan f_syncreceive_chan ::
            
            nil;
      lm_asmfun :=
        nil;
      lm_gvar :=
        nil
    |}.

  Definition PIPC_impl `{CompCertiKOS} `{SingleOracleProp} `{RealParams} `{MultiOracleProp} :=
    link_impl PIPC_module pipcintro.

End WITHCERTIKOS.