Library mcertikos.devdrivers.SerialGenLink

Require Import LinkTemplate.
Require Import DSerial.
Require Import SerialGen.
Require Import SerialGenLinkSource.
Require Import DSerialIntro.
Require Import DSerialIntroCSource.
Require Import DSerialIntroCode.

Section WITHCOMPCERTIKOS.
  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{oracle_prop: MultiOracleProp}.

  Lemma init_correct:
    init_correct_type DSerial_module dserial_intro dserial.
  Proof.
    init_correct.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type DSerial_module dserial_intro dserial.
  Proof.
    link_correct_aux.
    - link_cfunction
        serial_init_spec_ref
        DSerialIntroCode_serial_init.DSERIALINTROCODE.serial_init_code_correct.
    - link_cfunction
        serial_putc_spec_ref
        DSerialIntroCode_serial_putc.DSERIALINTROCODE.serial_putc_code_correct.
    - link_cfunction
        serial_getc_spec_ref
        DSerialIntroCode_serial_getc.DSERIALINTROCODE.serial_getc_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type DSerial_module dserial_intro dserial.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type DSerial_module dserial_intro dserial.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.