text:
Require Import Bool.
Require Import List.

From sflib Require Import sflib.
From Paco Require Import paco.

From PromisingLib Require Import Basic.
From PromisingLib Require Import Loc.

Require Import Event.
From PromisingLib Require Import Language.
Require Import Time.
Require Import View.
Require Import Cell.
Require Import Memory.
Require Import TView.
Require Import Local.
Require Import Thread.
Require Import Configuration.

Require Import FulfillStep.
Require Import SimMemory.
Require Import SimPromises.
Require Import SimLocal.
Require Import Compatibility.
Require Import SimThread.

Require Import Syntax.
Require Import Semantics.

Set Implicit Arguments.

Definition local_acquired (lc:Local.t) :=
  (Local.mk (TView.read_fence_tview (Local.tview lc) Ordering.acqrel) (Local.promises lc)).

Lemma sim_local_promise_acquired
      lc1_src mem1_src
      lc1_tgt mem1_tgt
      lc2_tgt mem2_tgt
      loc from to msg kind
      (STEP_TGT: Local.promise_step lc1_tgt mem1_tgt loc from to msg lc2_tgt mem2_tgt kind)
      (LOCAL1: sim_local SimPromises.bot lc1_src (local_acquired lc1_tgt))
      (MEM1: sim_memory mem1_src mem1_tgt)
      (WF1_SRC: Local.wf lc1_src mem1_src)
      (WF1_TGT: Local.wf lc1_tgt mem1_tgt)
      (MEM1_SRC: Memory.closed mem1_src)
      (MEM1_TGT: Memory.closed mem1_tgt):
  exists lc2_src mem2_src,
    <<STEP_SRC: Local.promise_step lc1_src mem1_src loc from to msg lc2_src mem2_src kind>> /\
    <<LOCAL2: sim_local SimPromises.bot lc2_src (local_acquired lc2_tgt)>> /\
    <<MEM2: sim_memory mem2_src mem2_tgt>>.
Proof.
  inv LOCAL1. inv STEP_TGT.
  exploit SimPromises.promise_bot; eauto.
  { apply WF1_SRC. }
  { apply WF1_TGT. }
  i. des.
  exploit Memory.promise_future; try apply PROMISE_SRC; try apply WF1_SRC; eauto.
  { destruct msg; ss. inv CLOSED. econs.
    eapply sim_memory_closed_opt_view; eauto. }
  i. des.
  esplits; eauto.
  - econs; eauto.
    destruct msg; ss. inv CLOSED. econs.
    eapply sim_memory_closed_opt_view; eauto.
  - econs; eauto.
Qed.

Lemma sim_local_fulfill_acquired
      lc1_src sc1_src mem1_src
      lc1_tgt sc1_tgt mem1_tgt
      lc2_tgt sc2_tgt
      loc from to val releasedm_src releasedm_tgt released ord_src ord_tgt
      (RELM_LE: View.opt_le releasedm_src releasedm_tgt)
      (RELM_WF: View.opt_wf releasedm_src)
      (RELM_CLOSED: Memory.closed_opt_view releasedm_src mem1_src)
      (RELM_TGT: Time.le (View.rlx (View.unwrap releasedm_tgt) loc) from)
      (WF_RELM_TGT: View.opt_wf releasedm_tgt)
      (ORD: Ordering.le ord_src ord_tgt)
      (ORD_TGT: Ordering.le ord_tgt Ordering.strong_relaxed)
      (STEP_TGT: fulfill_step lc1_tgt sc1_tgt loc from to val releasedm_tgt released ord_tgt lc2_tgt sc2_tgt)
      (LOCAL1: sim_local SimPromises.bot lc1_src (local_acquired lc1_tgt))
      (ACQUIRED1: View.le (TView.cur (Local.tview lc1_src))
                          (View.join (TView.cur (Local.tview lc1_tgt)) (View.unwrap releasedm_tgt)))
      (SC1: TimeMap.le sc1_src sc1_tgt)
      (MEM1: sim_memory mem1_src mem1_tgt)
      (WF1_SRC: Local.wf lc1_src mem1_src)
      (WF1_TGT: Local.wf lc1_tgt mem1_tgt)
      (SC1_SRC: Memory.closed_timemap sc1_src mem1_src)
      (SC1_TGT: Memory.closed_timemap sc1_tgt mem1_tgt)
      (MEM1_SRC: Memory.closed mem1_src)
      (MEM1_TGT: Memory.closed mem1_tgt):
  exists lc2_src sc2_src,
    <<STEP_SRC: fulfill_step lc1_src sc1_src loc from to val releasedm_src released ord_src lc2_src sc2_src>> /\
    <<LOCAL2: sim_local SimPromises.bot lc2_src (local_acquired lc2_tgt)>> /\
    <<SC2: TimeMap.le sc2_src sc2_tgt>>.
Proof.
  inv STEP_TGT.
  assert (RELT_LE:
   View.opt_le
     (TView.write_released (Local.tview lc1_src) sc1_src loc to releasedm_src ord_src)
     (TView.write_released (Local.tview lc1_tgt) sc2_tgt loc to releasedm_tgt ord_tgt)).
  { unfold TView.write_released, TView.write_tview. ss. viewtac.
    repeat (condtac; aggrtac;
            try match goal with
                | [|- View.opt_le _ _] => econs
                end);
      try apply WF1_TGT.
    - etrans; eauto. aggrtac.
    - etrans; [apply WF1_SRC|]. etrans; eauto. aggrtac.
    - etrans; [apply LOCAL1|]. aggrtac.
  }
  assert (RELT_WF:
   View.opt_wf (TView.write_released (Local.tview lc1_src) sc1_src loc to releasedm_src ord_src)).
  { unfold TView.write_released. condtac; econs.
    repeat (try condtac; viewtac; try apply WF1_SRC).
  }
  exploit SimPromises.remove_bot; try exact REMOVE;
    try exact MEM1; try apply LOCAL1; eauto.
  { econs. ss. }
  { apply WF1_SRC. }
  { apply WF1_TGT. }
  { apply WF1_TGT. }
  i. des. esplits.
  - econs; eauto.
    inv WRITABLE. econs.
    eapply TimeFacts.le_lt_lt; [apply ACQUIRED1|]. viewtac.
    eapply TimeFacts.le_lt_lt; eauto.
  - econs; eauto. s. unfold TView.write_tview, TView.read_fence_tview. ss.
    econs; ss; repeat (try condtac; aggrtac).
    all: try by destruct ord_src, ord_tgt.
    all: try by apply WF1_TGT.
    + etrans; [apply LOCAL1|]. aggrtac.
    + etrans; [apply LOCAL1|]. aggrtac.
    + etrans; [apply WF1_SRC|]. etrans; [apply LOCAL1|]. aggrtac.
    + etrans; [apply LOCAL1|]. aggrtac.
  - ss.
Qed.

Lemma sim_local_write_acquired
      lc1_src sc1_src mem1_src
      lc1_tgt sc1_tgt mem1_tgt
      lc2_tgt sc2_tgt mem2_tgt
      loc from to val releasedm_src releasedm_tgt released_tgt ord_src ord_tgt kind
      (RELM_LE: View.opt_le releasedm_src releasedm_tgt)
      (RELM_SRC_WF: View.opt_wf releasedm_src)
      (RELM_SRC_CLOSED: Memory.closed_opt_view releasedm_src mem1_src)
      (RELM_TGT_WF: View.opt_wf releasedm_tgt)
      (RELM_TGT_CLOSED: Memory.closed_opt_view releasedm_tgt mem1_tgt)
      (RELM_TGT: Time.le (View.rlx (View.unwrap releasedm_tgt) loc) from)
      (ORD: Ordering.le ord_src ord_tgt)
      (ORD_TGT: Ordering.le ord_tgt Ordering.strong_relaxed)
      (STEP_TGT: Local.write_step lc1_tgt sc1_tgt mem1_tgt loc from to val releasedm_tgt released_tgt ord_tgt lc2_tgt sc2_tgt mem2_tgt kind)
      (LOCAL1: sim_local SimPromises.bot lc1_src (local_acquired lc1_tgt))
      (ACQUIRED1: View.le (TView.cur (Local.tview lc1_src))
                          (View.join (TView.cur (Local.tview lc1_tgt)) (View.unwrap releasedm_tgt)))
      (SC1: TimeMap.le sc1_src sc1_tgt)
      (MEM1: sim_memory mem1_src mem1_tgt)
      (WF1_SRC: Local.wf lc1_src mem1_src)
      (WF1_TGT: Local.wf lc1_tgt mem1_tgt)
      (SC1_SRC: Memory.closed_timemap sc1_src mem1_src)
      (SC1_TGT: Memory.closed_timemap sc1_tgt mem1_tgt)
      (MEM1_SRC: Memory.closed mem1_src)
      (MEM1_TGT: Memory.closed mem1_tgt):
  exists released_src lc2_src sc2_src mem2_src,
    <<STEP_SRC: Local.write_step lc1_src sc1_src mem1_src loc from to val releasedm_src released_src ord_src lc2_src sc2_src mem2_src kind>> /\
    <<REL2: View.opt_le released_src released_tgt>> /\
    <<LOCAL2: sim_local SimPromises.bot lc2_src (local_acquired lc2_tgt)>> /\
    <<SC2: TimeMap.le sc2_src sc2_tgt>> /\
    <<MEM2: sim_memory mem2_src mem2_tgt>>.
Proof.
  exploit write_promise_fulfill; eauto. i. des.
  exploit Local.promise_step_future; eauto. i. des.
  exploit sim_local_promise_acquired; eauto. i. des.
  exploit Local.promise_step_future; eauto. i. des.
  hexploit sim_local_fulfill_acquired; try apply STEP2;
    try apply LOCAL2; try apply MEM2; eauto.
  { eapply Memory.future_closed_opt_view; eauto. }
  { inv STEP_SRC. inv STEP1. ss. }
  i. des.
  exploit promise_fulfill_write; try exact STEP_SRC; try exact STEP_SRC0; eauto.
  { i. hexploit ORD0; eauto.
    i. des. splits; auto. eapply sim_local_nonsynch_loc; eauto.
  }
  i. des. esplits; eauto. etrans; eauto.
Qed.

Inductive split_acquire: forall (i1 i2:Instr.t), Prop :=
| split_acquire_load
    r l:
    split_acquire (Instr.load r l Ordering.acqrel) (Instr.load r l Ordering.relaxed)
| split_acquire_update
    r l rmw ow
    (OW: Ordering.le ow Ordering.strong_relaxed):
    split_acquire (Instr.update r l rmw Ordering.acqrel ow) (Instr.update r l rmw Ordering.relaxed ow)
.

Inductive sim_acquired: forall (st_src:(Language.state lang)) (lc_src:Local.t) (sc1_src:TimeMap.t) (mem1_src:Memory.t)
                          (st_tgt:(Language.state lang)) (lc_tgt:Local.t) (sc1_tgt:TimeMap.t) (mem1_tgt:Memory.t), Prop :=
| sim_acquired_intro
    rs
    lc1_src sc1_src mem1_src
    lc1_tgt sc1_tgt mem1_tgt
    (LOCAL: sim_local SimPromises.bot lc1_src (local_acquired lc1_tgt))
    (SC: TimeMap.le sc1_src sc1_tgt)
    (MEMORY: sim_memory mem1_src mem1_tgt)
    (WF_SRC: Local.wf lc1_src mem1_src)
    (WF_TGT: Local.wf lc1_tgt mem1_tgt)
    (SC_SRC: Memory.closed_timemap sc1_src mem1_src)
    (SC_TGT: Memory.closed_timemap sc1_tgt mem1_tgt)
    (MEM_SRC: Memory.closed mem1_src)
    (MEM_TGT: Memory.closed mem1_tgt):
    sim_acquired
      (State.mk rs []) lc1_src sc1_src mem1_src
      (State.mk rs [Stmt.instr (Instr.fence Ordering.acqrel Ordering.plain)]) lc1_tgt sc1_tgt mem1_tgt
.

Lemma sim_acquired_mon
      st_src lc_src sc1_src mem1_src
      st_tgt lc_tgt sc1_tgt mem1_tgt
      sc2_src mem2_src
      sc2_tgt mem2_tgt
      (SIM1: sim_acquired st_src lc_src sc1_src mem1_src
                          st_tgt lc_tgt sc1_tgt mem1_tgt)
      (SC_FUTURE_SRC: TimeMap.le sc1_src sc2_src)
      (SC_FUTURE_TGT: TimeMap.le sc1_tgt sc2_tgt)
      (MEM_FUTURE_SRC: Memory.future_weak mem1_src mem2_src)
      (MEM_FUTURE_TGT: Memory.future_weak mem1_tgt mem2_tgt)
      (SC1: TimeMap.le sc2_src sc2_tgt)
      (MEM1: sim_memory mem2_src mem2_tgt)
      (WF_SRC: Local.wf lc_src mem2_src)
      (WF_TGT: Local.wf lc_tgt mem2_tgt)
      (SC_SRC: Memory.closed_timemap sc2_src mem2_src)
      (SC_TGT: Memory.closed_timemap sc2_tgt mem2_tgt)
      (MEM_SRC: Memory.closed mem2_src)
      (MEM_TGT: Memory.closed mem2_tgt):
  sim_acquired st_src lc_src sc2_src mem2_src
               st_tgt lc_tgt sc2_tgt mem2_tgt.
Proof.
  inv SIM1. econs; eauto.
Qed.

Lemma sim_acquired_step
      st1_src lc1_src sc1_src mem1_src
      st1_tgt lc1_tgt sc1_tgt mem1_tgt
      (SIM: sim_acquired st1_src lc1_src sc1_src mem1_src
                         st1_tgt lc1_tgt sc1_tgt mem1_tgt):
  _sim_thread_step lang lang ((sim_thread (sim_terminal eq)) \8/ sim_acquired)
                   st1_src lc1_src sc1_src mem1_src
                   st1_tgt lc1_tgt sc1_tgt mem1_tgt.
Proof.
  inv SIM. ii.
  inv STEP_TGT; [inv STEP|inv STEP; inv LOCAL0];
    try (inv STATE; inv INSTR; inv SPLIT); ss.
  - (* promise *)
    right.
    exploit Local.promise_step_future; eauto. i. des.
    exploit sim_local_promise_acquired; try exact LOCAL; eauto. i. des.
    exploit Local.promise_step_future; eauto. i. des.
    esplits; try apply SC; eauto; ss.
    + econs 2. econs. econs; eauto.
    + eauto.
    + right. econs; eauto.
  - (* fence *)
    right.
    exploit Local.fence_step_future; eauto. i. des.
    inv STATE. inv INSTR. inv LOCAL1. ss.
    esplits; (try by econs 1); eauto; ss.
    left. eapply paco9_mon; [apply sim_stmts_nil|]; ss. econs; ss.
    + rewrite TViewFacts.write_fence_tview_strong_relaxed; ss. apply LOCAL.
    + apply LOCAL.
Qed.

Lemma sim_acquired_sim_thread:
  sim_acquired <8= (sim_thread (sim_terminal eq)).
Proof.
  pcofix CIH. i. pfold. ii. ss. splits; ss; ii.
  - inv TERMINAL_TGT. inv PR; ss.
  - exploit SimPromises.cap; try apply LOCAL; eauto.
    inv PR. apply LOCAL.
  - right. esplits; eauto.
    inv PR. eapply sim_local_memory_bot; eauto.
  - exploit sim_acquired_mon; eauto. i.
    exploit sim_acquired_step; eauto. i. des; eauto.
    + right. esplits; eauto.
      left. eapply paco9_mon; eauto. ss.
    + right. esplits; eauto.
Qed.

Lemma sim_local_read_acquired
      lc1_src mem1_src
      lc1_tgt mem1_tgt
      lc2_tgt
      loc ts val released_tgt
      (STEP_TGT: Local.read_step lc1_tgt mem1_tgt loc ts val released_tgt Ordering.relaxed lc2_tgt)
      (LOCAL1: sim_local SimPromises.bot lc1_src lc1_tgt)
      (MEM1: sim_memory mem1_src mem1_tgt)
      (WF1_SRC: Local.wf lc1_src mem1_src)
      (WF1_TGT: Local.wf lc1_tgt mem1_tgt)
      (MEM1_SRC: Memory.closed mem1_src)
      (MEM1_TGT: Memory.closed mem1_tgt):
  exists released_src lc2_src,
    <<REL: View.opt_le released_src released_tgt>> /\
    <<STEP_SRC: Local.read_step lc1_src mem1_src loc ts val released_src Ordering.acqrel lc2_src>> /\
    <<LOCAL2: sim_local SimPromises.bot lc2_src (local_acquired lc2_tgt)>>.
Proof.
  inv LOCAL1. inv STEP_TGT.
  exploit sim_memory_get; try apply GET; try apply MEM1. i. des. inv MSG.
  esplits; eauto.
  - econs; eauto. inv READABLE. econs; ss; i.
    + rewrite <- PLN. apply TVIEW.
    + rewrite <- RLX; ss. apply TVIEW.
  - econs; eauto. s.
    unfold TView.read_tview, TView.read_fence_tview. ss.
    econs; repeat (condtac; aggrtac).
    all: try by apply TVIEW.
    all: try by apply WF1_TGT.
    + rewrite <- ? View.join_l. etrans; [apply TVIEW|]. apply WF1_TGT.
    + inv MEM1_TGT. exploit CLOSED; eauto. i. des.
      apply View.unwrap_opt_wf. inv MSG_WF. ss.
    + rewrite <- ? View.join_l. apply TVIEW.
    + inv MEM1_TGT. exploit CLOSED; eauto. i. des.
      apply View.unwrap_opt_wf. inv MSG_WF. ss.
Qed.

Lemma split_acquire_sim_stmts
      i_src i_tgt
      (SPLIT: split_acquire i_src i_tgt):
  sim_stmts eq
            [Stmt.instr i_src]
            [Stmt.instr i_tgt; Stmt.instr (Instr.fence Ordering.acqrel Ordering.plain)]
            eq.
Proof.
  pcofix CIH. ii. subst. pfold. ii. splits; ii.
  { inv TERMINAL_TGT. }
  { exploit SimPromises.cap; try apply LOCAL; eauto. }
  { right. esplits; eauto.
    inv LOCAL. apply SimPromises.sem_bot_inv in PROMISES; auto. rewrite PROMISES. auto.
  }
  right.
  inv STEP_TGT; [inv STEP|inv STEP; inv LOCAL0];
    try (inv STATE; inv INSTR; inv SPLIT); ss.
  - (* promise *)
    exploit sim_local_promise; eauto. i. des.
    esplits; try apply SC; eauto; ss.
    econs 2. econs 1; eauto. econs; eauto. eauto.
  - (* load *)
    exploit Local.read_step_future; eauto. i. des.
    exploit sim_local_read_acquired; eauto. i. des.
    exploit Local.read_step_future; eauto. i. des.
    esplits; try apply SC; eauto; ss.
    + econs 2. econs 2. econs; cycle 1.
      * econs 2. eauto.
      * econs. econs.
    + auto.
    + left. eapply paco9_mon; [apply sim_acquired_sim_thread|]; ss.
  - (* update-load *)
    exploit Local.read_step_future; eauto. i. des.
    exploit sim_local_read_acquired; eauto. i. des.
    exploit Local.read_step_future; eauto. i. des.
    esplits; try apply SC; eauto; ss.
    + econs 2. econs 2. econs; cycle 1.
      * econs 2. eauto.
      * econs. econs. eauto.
    + auto.
    + left. eapply paco9_mon; [apply sim_acquired_sim_thread|]; ss.
  - (* update *)
    exploit Local.read_step_future; eauto. i. des.
    exploit sim_local_read_acquired; eauto. i. des.
    exploit Local.read_step_future; eauto. i. des.
    exploit Local.write_step_future; eauto. i. des.
    hexploit sim_local_write_acquired; try exact LOCAL2; try exact SC; eauto; try refl.
    { inv LOCAL1. inv MEM_TGT. exploit CLOSED; eauto. i. des.
      inv MSG_TS. ss. }
    { inv STEP_SRC. inv LOCAL1. ss. repeat (condtac; aggrtac).
      - rewrite <- ? View.join_l. apply LOCAL.
      - apply WF_TGT.
      - unfold TimeMap.join. rewrite <- Time.join_l. rewrite <- Time.join_l. rewrite <- Time.join_r.
        unfold View.singleton_ur_if. condtac; ss. unfold TimeMap.singleton, LocFun.add.
        condtac; ss. refl.
    }
    i. des.
    exploit Local.write_step_future; eauto. i. des.
    esplits; try apply SC; eauto; ss.
    + econs 2. econs 2. econs; cycle 1.
      * econs 4; eauto.
      * econs. econs. eauto.
    + auto.
    + left. eapply paco9_mon; [apply sim_acquired_sim_thread|]; ss.
Qed.

author: snu-sf


text:
From Coq Require Import String List ZArith.
From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.
Local Open Scope Z_scope.

Module Info.
  Definition version := "3.7"%string.
  Definition build_number := ""%string.
  Definition build_tag := ""%string.
  Definition arch := "x86"%string.
  Definition model := "32sse2"%string.
  Definition abi := "standard"%string.
  Definition bitsize := 32.
  Definition big_endian := false.
  Definition source_file := "main.c"%string.
  Definition normalized := true.
End Info.

Definition _Apile_add : ident := 73%positive.
Definition _Apile_count : ident := 74%positive.
Definition _Onepile_add : ident := 77%positive.
Definition _Onepile_count : ident := 78%positive.
Definition _Onepile_init : ident := 76%positive.
Definition _Pile_add : ident := 66%positive.
Definition _Pile_count : ident := 69%positive.
Definition _Pile_free : ident := 71%positive.
Definition _Pile_new : ident := 65%positive.
Definition _Triang_nth : ident := 80%positive.
Definition ___builtin_ais_annot : ident := 1%positive.
Definition ___builtin_annot : ident := 10%positive.
Definition ___builtin_annot_intval : ident := 11%positive.
Definition ___builtin_bswap : ident := 3%positive.
Definition ___builtin_bswap16 : ident := 5%positive.
Definition ___builtin_bswap32 : ident := 4%positive.
Definition ___builtin_bswap64 : ident := 2%positive.
Definition ___builtin_clz : ident := 36%positive.
Definition ___builtin_clzl : ident := 37%positive.
Definition ___builtin_clzll : ident := 38%positive.
Definition ___builtin_ctz : ident := 39%positive.
Definition ___builtin_ctzl : ident := 40%positive.
Definition ___builtin_ctzll : ident := 41%positive.
Definition ___builtin_debug : ident := 52%positive.
Definition ___builtin_fabs : ident := 6%positive.
Definition ___builtin_fmadd : ident := 44%positive.
Definition ___builtin_fmax : ident := 42%positive.
Definition ___builtin_fmin : ident := 43%positive.
Definition ___builtin_fmsub : ident := 45%positive.
Definition ___builtin_fnmadd : ident := 46%positive.
Definition ___builtin_fnmsub : ident := 47%positive.
Definition ___builtin_fsqrt : ident := 7%positive.
Definition ___builtin_membar : ident := 12%positive.
Definition ___builtin_memcpy_aligned : ident := 8%positive.
Definition ___builtin_read16_reversed : ident := 48%positive.
Definition ___builtin_read32_reversed : ident := 49%positive.
Definition ___builtin_sel : ident := 9%positive.
Definition ___builtin_va_arg : ident := 14%positive.
Definition ___builtin_va_copy : ident := 15%positive.
Definition ___builtin_va_end : ident := 16%positive.
Definition ___builtin_va_start : ident := 13%positive.
Definition ___builtin_write16_reversed : ident := 50%positive.
Definition ___builtin_write32_reversed : ident := 51%positive.
Definition ___compcert_i64_dtos : ident := 21%positive.
Definition ___compcert_i64_dtou : ident := 22%positive.
Definition ___compcert_i64_sar : ident := 33%positive.
Definition ___compcert_i64_sdiv : ident := 27%positive.
Definition ___compcert_i64_shl : ident := 31%positive.
Definition ___compcert_i64_shr : ident := 32%positive.
Definition ___compcert_i64_smod : ident := 29%positive.
Definition ___compcert_i64_smulh : ident := 34%positive.
Definition ___compcert_i64_stod : ident := 23%positive.
Definition ___compcert_i64_stof : ident := 25%positive.
Definition ___compcert_i64_udiv : ident := 28%positive.
Definition ___compcert_i64_umod : ident := 30%positive.
Definition ___compcert_i64_umulh : ident := 35%positive.
Definition ___compcert_i64_utod : ident := 24%positive.
Definition ___compcert_i64_utof : ident := 26%positive.
Definition ___compcert_va_composite : ident := 20%positive.
Definition ___compcert_va_float64 : ident := 19%positive.
Definition ___compcert_va_int32 : ident := 17%positive.
Definition ___compcert_va_int64 : ident := 18%positive.
Definition _a_pile : ident := 72%positive.
Definition _c : ident := 68%positive.
Definition _c1 : ident := 81%positive.
Definition _c2 : ident := 82%positive.
Definition _c3 : ident := 83%positive.
Definition _exit : ident := 55%positive.
Definition _free : ident := 54%positive.
Definition _head : ident := 61%positive.
Definition _i : ident := 79%positive.
Definition _list : ident := 59%positive.
Definition _main : ident := 57%positive.
Definition _malloc : ident := 53%positive.
Definition _n : ident := 58%positive.
Definition _next : ident := 60%positive.
Definition _p : ident := 63%positive.
Definition _pile : ident := 62%positive.
Definition _placeholder : ident := 56%positive.
Definition _q : ident := 67%positive.
Definition _r : ident := 70%positive.
Definition _surely_malloc : ident := 64%positive.
Definition _the_pile : ident := 75%positive.
Definition _t'1 : ident := 84%positive.
Definition _t'2 : ident := 85%positive.
Definition _t'3 : ident := 86%positive.

Definition f_main := {|
  fn_return := tint;
  fn_callconv := cc_default;
  fn_params := nil;
  fn_vars := nil;
  fn_temps := ((_i, tint) :: (_c1, tint) :: (_c2, tint) :: (_c3, tint) ::
               (_t'3, tint) :: (_t'2, tint) :: (_t'1, tint) :: nil);
  fn_body :=
(Ssequence
  (Ssequence
    (Scall None (Evar _Onepile_init (Tfunction Tnil tvoid cc_default)) nil)
    (Ssequence
      (Ssequence
        (Sset _i (Econst_int (Int.repr 0) tint))
        (Sloop
          (Ssequence
            (Sifthenelse (Ebinop Olt (Etempvar _i tint)
                           (Econst_int (Int.repr 10) tint) tint)
              Sskip
              Sbreak)
            (Ssequence
              (Scall None
                (Evar _Onepile_add (Tfunction (Tcons tint Tnil) tvoid
                                     cc_default))
                ((Ebinop Oadd (Etempvar _i tint)
                   (Econst_int (Int.repr 1) tint) tint) :: nil))
              (Scall None
                (Evar _Apile_add (Tfunction (Tcons tint Tnil) tvoid
                                   cc_default))
                ((Ebinop Oadd (Etempvar _i tint)
                   (Econst_int (Int.repr 1) tint) tint) :: nil))))
          (Sset _i
            (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr 1) tint)
              tint))))
      (Ssequence
        (Ssequence
          (Scall (Some _t'1)
            (Evar _Onepile_count (Tfunction Tnil tint cc_default)) nil)
          (Sset _c1 (Etempvar _t'1 tint)))
        (Ssequence
          (Ssequence
            (Scall (Some _t'2)
              (Evar _Apile_count (Tfunction Tnil tint cc_default)) nil)
            (Sset _c2 (Etempvar _t'2 tint)))
          (Ssequence
            (Ssequence
              (Scall (Some _t'3)
                (Evar _Triang_nth (Tfunction (Tcons tint Tnil) tint
                                    cc_default))
                ((Econst_int (Int.repr 10) tint) :: nil))
              (Sset _c3 (Etempvar _t'3 tint)))
            (Sreturn (Some (Ebinop Osub
                             (Ebinop Oadd (Etempvar _c1 tint)
                               (Etempvar _c2 tint) tint)
                             (Ebinop Omul (Econst_int (Int.repr 2) tint)
                               (Etempvar _c3 tint) tint) tint))))))))
  (Sreturn (Some (Econst_int (Int.repr 0) tint))))
|}.

Definition composites : list composite_definition :=
nil.

Definition global_definitions : list (ident * globdef fundef type) :=
((___builtin_ais_annot,
   Gfun(External (EF_builtin "__builtin_ais_annot"
                   (mksignature (AST.Tint :: nil) AST.Tvoid
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons (tptr tschar) Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (___builtin_bswap64,
   Gfun(External (EF_builtin "__builtin_bswap64"
                   (mksignature (AST.Tlong :: nil) AST.Tlong cc_default))
     (Tcons tulong Tnil) tulong cc_default)) ::
 (___builtin_bswap,
   Gfun(External (EF_builtin "__builtin_bswap"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tuint cc_default)) ::
 (___builtin_bswap32,
   Gfun(External (EF_builtin "__builtin_bswap32"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tuint cc_default)) ::
 (___builtin_bswap16,
   Gfun(External (EF_builtin "__builtin_bswap16"
                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
                     cc_default)) (Tcons tushort Tnil) tushort cc_default)) ::
 (___builtin_fabs,
   Gfun(External (EF_builtin "__builtin_fabs"
                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
     (Tcons tdouble Tnil) tdouble cc_default)) ::
 (___builtin_fsqrt,
   Gfun(External (EF_builtin "__builtin_fsqrt"
                   (mksignature (AST.Tfloat :: nil) AST.Tfloat cc_default))
     (Tcons tdouble Tnil) tdouble cc_default)) ::
 (___builtin_memcpy_aligned,
   Gfun(External (EF_builtin "__builtin_memcpy_aligned"
                   (mksignature
                     (AST.Tint :: AST.Tint :: AST.Tint :: AST.Tint :: nil)
                     AST.Tvoid cc_default))
     (Tcons (tptr tvoid)
       (Tcons (tptr tvoid) (Tcons tuint (Tcons tuint Tnil)))) tvoid
     cc_default)) ::
 (___builtin_sel,
   Gfun(External (EF_builtin "__builtin_sel"
                   (mksignature (AST.Tint :: nil) AST.Tvoid
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons tbool Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (___builtin_annot,
   Gfun(External (EF_builtin "__builtin_annot"
                   (mksignature (AST.Tint :: nil) AST.Tvoid
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons (tptr tschar) Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (___builtin_annot_intval,
   Gfun(External (EF_builtin "__builtin_annot_intval"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
                     cc_default)) (Tcons (tptr tschar) (Tcons tint Tnil))
     tint cc_default)) ::
 (___builtin_membar,
   Gfun(External (EF_builtin "__builtin_membar"
                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
     cc_default)) ::
 (___builtin_va_start,
   Gfun(External (EF_builtin "__builtin_va_start"
                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
 (___builtin_va_arg,
   Gfun(External (EF_builtin "__builtin_va_arg"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
     tvoid cc_default)) ::
 (___builtin_va_copy,
   Gfun(External (EF_builtin "__builtin_va_copy"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
                     cc_default))
     (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) ::
 (___builtin_va_end,
   Gfun(External (EF_builtin "__builtin_va_end"
                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
     (Tcons (tptr tvoid) Tnil) tvoid cc_default)) ::
 (___compcert_va_int32,
   Gfun(External (EF_external "__compcert_va_int32"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons (tptr tvoid) Tnil) tuint cc_default)) ::
 (___compcert_va_int64,
   Gfun(External (EF_external "__compcert_va_int64"
                   (mksignature (AST.Tint :: nil) AST.Tlong cc_default))
     (Tcons (tptr tvoid) Tnil) tulong cc_default)) ::
 (___compcert_va_float64,
   Gfun(External (EF_external "__compcert_va_float64"
                   (mksignature (AST.Tint :: nil) AST.Tfloat cc_default))
     (Tcons (tptr tvoid) Tnil) tdouble cc_default)) ::
 (___compcert_va_composite,
   Gfun(External (EF_external "__compcert_va_composite"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tint
                     cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil))
     (tptr tvoid) cc_default)) ::
 (___compcert_i64_dtos,
   Gfun(External (EF_runtime "__compcert_i64_dtos"
                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
     (Tcons tdouble Tnil) tlong cc_default)) ::
 (___compcert_i64_dtou,
   Gfun(External (EF_runtime "__compcert_i64_dtou"
                   (mksignature (AST.Tfloat :: nil) AST.Tlong cc_default))
     (Tcons tdouble Tnil) tulong cc_default)) ::
 (___compcert_i64_stod,
   Gfun(External (EF_runtime "__compcert_i64_stod"
                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
     (Tcons tlong Tnil) tdouble cc_default)) ::
 (___compcert_i64_utod,
   Gfun(External (EF_runtime "__compcert_i64_utod"
                   (mksignature (AST.Tlong :: nil) AST.Tfloat cc_default))
     (Tcons tulong Tnil) tdouble cc_default)) ::
 (___compcert_i64_stof,
   Gfun(External (EF_runtime "__compcert_i64_stof"
                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
     (Tcons tlong Tnil) tfloat cc_default)) ::
 (___compcert_i64_utof,
   Gfun(External (EF_runtime "__compcert_i64_utof"
                   (mksignature (AST.Tlong :: nil) AST.Tsingle cc_default))
     (Tcons tulong Tnil) tfloat cc_default)) ::
 (___compcert_i64_sdiv,
   Gfun(External (EF_runtime "__compcert_i64_sdiv"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
     cc_default)) ::
 (___compcert_i64_udiv,
   Gfun(External (EF_runtime "__compcert_i64_udiv"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
     cc_default)) ::
 (___compcert_i64_smod,
   Gfun(External (EF_runtime "__compcert_i64_smod"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
     cc_default)) ::
 (___compcert_i64_umod,
   Gfun(External (EF_runtime "__compcert_i64_umod"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
     cc_default)) ::
 (___compcert_i64_shl,
   Gfun(External (EF_runtime "__compcert_i64_shl"
                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
     cc_default)) ::
 (___compcert_i64_shr,
   Gfun(External (EF_runtime "__compcert_i64_shr"
                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
                     cc_default)) (Tcons tulong (Tcons tint Tnil)) tulong
     cc_default)) ::
 (___compcert_i64_sar,
   Gfun(External (EF_runtime "__compcert_i64_sar"
                   (mksignature (AST.Tlong :: AST.Tint :: nil) AST.Tlong
                     cc_default)) (Tcons tlong (Tcons tint Tnil)) tlong
     cc_default)) ::
 (___compcert_i64_smulh,
   Gfun(External (EF_runtime "__compcert_i64_smulh"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tlong (Tcons tlong Tnil)) tlong
     cc_default)) ::
 (___compcert_i64_umulh,
   Gfun(External (EF_runtime "__compcert_i64_umulh"
                   (mksignature (AST.Tlong :: AST.Tlong :: nil) AST.Tlong
                     cc_default)) (Tcons tulong (Tcons tulong Tnil)) tulong
     cc_default)) ::
 (___builtin_clz,
   Gfun(External (EF_builtin "__builtin_clz"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_clzl,
   Gfun(External (EF_builtin "__builtin_clzl"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_clzll,
   Gfun(External (EF_builtin "__builtin_clzll"
                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
     (Tcons tulong Tnil) tint cc_default)) ::
 (___builtin_ctz,
   Gfun(External (EF_builtin "__builtin_ctz"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_ctzl,
   Gfun(External (EF_builtin "__builtin_ctzl"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tuint Tnil) tint cc_default)) ::
 (___builtin_ctzll,
   Gfun(External (EF_builtin "__builtin_ctzll"
                   (mksignature (AST.Tlong :: nil) AST.Tint cc_default))
     (Tcons tulong Tnil) tint cc_default)) ::
 (___builtin_fmax,
   Gfun(External (EF_builtin "__builtin_fmax"
                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
     tdouble cc_default)) ::
 (___builtin_fmin,
   Gfun(External (EF_builtin "__builtin_fmin"
                   (mksignature (AST.Tfloat :: AST.Tfloat :: nil) AST.Tfloat
                     cc_default)) (Tcons tdouble (Tcons tdouble Tnil))
     tdouble cc_default)) ::
 (___builtin_fmadd,
   Gfun(External (EF_builtin "__builtin_fmadd"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     AST.Tfloat cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fmsub,
   Gfun(External (EF_builtin "__builtin_fmsub"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     AST.Tfloat cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fnmadd,
   Gfun(External (EF_builtin "__builtin_fnmadd"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     AST.Tfloat cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_fnmsub,
   Gfun(External (EF_builtin "__builtin_fnmsub"
                   (mksignature
                     (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil)
                     AST.Tfloat cc_default))
     (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble
     cc_default)) ::
 (___builtin_read16_reversed,
   Gfun(External (EF_builtin "__builtin_read16_reversed"
                   (mksignature (AST.Tint :: nil) AST.Tint16unsigned
                     cc_default)) (Tcons (tptr tushort) Tnil) tushort
     cc_default)) ::
 (___builtin_read32_reversed,
   Gfun(External (EF_builtin "__builtin_read32_reversed"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons (tptr tuint) Tnil) tuint cc_default)) ::
 (___builtin_write16_reversed,
   Gfun(External (EF_builtin "__builtin_write16_reversed"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
                     cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil))
     tvoid cc_default)) ::
 (___builtin_write32_reversed,
   Gfun(External (EF_builtin "__builtin_write32_reversed"
                   (mksignature (AST.Tint :: AST.Tint :: nil) AST.Tvoid
                     cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil))
     tvoid cc_default)) ::
 (___builtin_debug,
   Gfun(External (EF_external "__builtin_debug"
                   (mksignature (AST.Tint :: nil) AST.Tvoid
                     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|}))
     (Tcons tint Tnil) tvoid
     {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) ::
 (_Apile_add,
   Gfun(External (EF_external "Apile_add"
                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
     (Tcons tint Tnil) tvoid cc_default)) ::
 (_Apile_count,
   Gfun(External (EF_external "Apile_count"
                   (mksignature nil AST.Tint cc_default)) Tnil tint
     cc_default)) ::
 (_Onepile_init,
   Gfun(External (EF_external "Onepile_init"
                   (mksignature nil AST.Tvoid cc_default)) Tnil tvoid
     cc_default)) ::
 (_Onepile_add,
   Gfun(External (EF_external "Onepile_add"
                   (mksignature (AST.Tint :: nil) AST.Tvoid cc_default))
     (Tcons tint Tnil) tvoid cc_default)) ::
 (_Onepile_count,
   Gfun(External (EF_external "Onepile_count"
                   (mksignature nil AST.Tint cc_default)) Tnil tint
     cc_default)) ::
 (_Triang_nth,
   Gfun(External (EF_external "Triang_nth"
                   (mksignature (AST.Tint :: nil) AST.Tint cc_default))
     (Tcons tint Tnil) tint cc_default)) :: (_main, Gfun(Internal f_main)) ::
 nil).

Definition public_idents : list ident :=
(_main :: _Triang_nth :: _Onepile_count :: _Onepile_add :: _Onepile_init ::
 _Apile_count :: _Apile_add :: ___builtin_debug ::
 ___builtin_write32_reversed :: ___builtin_write16_reversed ::
 ___builtin_read32_reversed :: ___builtin_read16_reversed ::
 ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub ::
 ___builtin_fmadd :: ___builtin_fmin :: ___builtin_fmax ::
 ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll ::
 ___builtin_clzl :: ___builtin_clz :: ___compcert_i64_umulh ::
 ___compcert_i64_smulh :: ___compcert_i64_sar :: ___compcert_i64_shr ::
 ___compcert_i64_shl :: ___compcert_i64_umod :: ___compcert_i64_smod ::
 ___compcert_i64_udiv :: ___compcert_i64_sdiv :: ___compcert_i64_utof ::
 ___compcert_i64_stof :: ___compcert_i64_utod :: ___compcert_i64_stod ::
 ___compcert_i64_dtou :: ___compcert_i64_dtos :: ___compcert_va_composite ::
 ___compcert_va_float64 :: ___compcert_va_int64 :: ___compcert_va_int32 ::
 ___builtin_va_end :: ___builtin_va_copy :: ___builtin_va_arg ::
 ___builtin_va_start :: ___builtin_membar :: ___builtin_annot_intval ::
 ___builtin_annot :: ___builtin_sel :: ___builtin_memcpy_aligned ::
 ___builtin_fsqrt :: ___builtin_fabs :: ___builtin_bswap16 ::
 ___builtin_bswap32 :: ___builtin_bswap :: ___builtin_bswap64 ::
 ___builtin_ais_annot :: nil).

Definition prog : Clight.program :=
  mkprogram composites global_definitions public_idents _main Logic.I.

author: Ereboas

repo: PL-Final-Project


text:
Require Export Arith.EqNat.
Require Export Arith.Lt.
Require Export Arith.Compare_dec.
Require Export List.
Require Export ListLocal.
Require Import String.
Require Import TypeAssignmentPoly.
Require Import ResultOpenClose.
Require Import ResultBasics.
Require Import ResultWeaken.
Require Import ResultRename.
Require Import TacticsSF.
Require Import TacticsCPDT.
Require Import TacticsLocal.
Require Import ResultStrengthen.
Require Import ResultStructTyped.
Require Import ResultSubst.
Require Import ResultSubjectReduction.

Lemma ctx_preservation_in :
  forall f1 f2 G1 G2 v vo s,
    f1 <> f2 ->
    ctx_preservation G1 G2 (VOInteract v f2 vo) ->
    CTX.In (ValName (Nm (Free f1)), TChannel s) G1 ->
    CTX.In (ValName (Nm (Free f1)), TChannel s) G2.
Proof.
  intros f1 f2 G1 G2 v vo s Hneq Hpres Hin.

  inversion Hpres; subst.
  rewrite H3; clear H3.

  assert (ValName (Nm (Free f1)) <> nm1) as Hneq1.
  inversion H4; subst;
    (try solve [discriminate]);
    (try solve [contradict Hneq; injection Hneq; intros; subst; auto]).

  assert (ValName (Nm (Free f1)) <> (dual_name nm1)) as Hneq2.
  inversion H4; subst;
    (try solve [discriminate]);
    (try solve [contradict Hneq; injection Hneq; intros; subst; auto]).

  repeat unfold ctx_replace in *.
  repeat (rewrite CTXFacts.add_iff in * || rewrite CTXFacts.remove_iff in *).
  right; split.
  right; split; auto.
  contradict Hneq2; injection Hneq2; intros; subst; clear Hneq2; symmetry.
  destruct nm1; simpl in *.
  discriminate H3.
  injection H3; intros; subst; auto.

  contradict Hneq1; injection Hneq1; intros; subst; clear Hneq1; auto.
Qed.

Lemma lookup_functional :
  forall G u sigma1 sigma2,
    G |-wf
    ->
    CTX.In (u, sigma1) G
    ->
    CTX.In (u, sigma2) G
    ->
    sigma1 = sigma2.
Proof.
  intros G u sigma1 sigma2 Hwf Hinu1 Hinu2.
  inversion Hwf; subst.
  eapply H0; eauto.
Qed.

(* ============================================================================= *)

Theorem conformance :
  forall G P Q f s alphas,
    reductions P Q alphas
    ->
    G |-p P
    ->
    balanced G
    ->
    CTX.In (ValName (Nm (Free f)), TChannel s) G
    ->
    traces f (project f alphas) s.
Proof.
  intros G P Q f s alphas Hredns; generalize G f s; induction Hredns; intros G' f' s' Htyp Hpre Hin; [ simpl; constructor | ].
  clear G; rename G' into G; clear f; rename f' into f; clear s; rename s' into s.
  assert (G |-wf) as HwfG.
  eapply typed_ctx_wf; eauto.

  apply subject_reduction with (G1:=G) in H; auto.
  destruct H as [G2 Hconj]; destruct Hconj as [Htyp2 Hpres].

  destruct vo.
  unfold project; simpl.
  eapply IHHredns; eauto.

  inversion Hpres; subst; [
    eapply balanced_equals; eauto
    | inversion H4
  ].
  inversion Hpres; subst; [
    rewrite H; auto
    | inversion H4
  ].

  simpl; destruct (string_dec f f0); subst.
  inversion Hpres; subst.
  inversion H4; subst; simpl in *;
    (eapply lookup_functional in Hin; [ | apply typed_ctx_wf in Htyp; eauto | eauto ]).

  injection Hin; intros; subst; clear Hin;
    eapply TRCCons; eauto; eapply IHHredns; eauto; [
      eapply ctx_preservation_preserves_balanced; eauto
      | auto
    ].
  rewrite H3; unfold ctx_replace; rewrite CTXFacts.add_iff; auto.

  injection Hin; intros; subst; clear Hin;
    eapply TRCCons; eauto; eapply IHHredns; eauto; [
      eapply ctx_preservation_preserves_balanced; eauto
      | auto
    ].
  rewrite H3; unfold ctx_replace; rewrite CTXFacts.add_iff; auto.

  injection Hin; intros; subst; clear Hin;
    eapply TRCCons; eauto.
  constructor; eauto.
  simpl.
  constructor.
  eapply IHHredns; eauto; [
      eapply ctx_preservation_preserves_balanced; eauto
      | auto
    ].
  rewrite H3; unfold ctx_replace; (repeat (rewrite CTXFacts.add_iff || rewrite CTXFacts.remove_iff)); auto.
  right; split; auto; discriminate.

  injection Hin; intros; subst; clear Hin;
    eapply TRCCons; eauto.
  constructor; eauto.
  simpl.
  constructor.
  eapply IHHredns; eauto; [
      eapply ctx_preservation_preserves_balanced; eauto
      | auto
    ].
  rewrite H3; unfold ctx_replace; (repeat (rewrite CTXFacts.add_iff || rewrite CTXFacts.remove_iff)); auto.
  right; split; auto; discriminate.

  eapply IHHredns; eauto; [
    eapply ctx_preservation_preserves_balanced; eauto
    | eapply ctx_preservation_in; eauto
  ].
Qed.

author: cmcl

repo: msci

save_path: github-repos/coq/cmcl-msci


text:
(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics.
Require Import Types.
Require Import Cubical.
Require Import HProp.
Require Import HSet.
Require Import NullHomotopy.
Require Import Extensions.
Require Import Colimits.Pushout.
Require Import Truncations.
Import TrM.

Local Open Scope path_scope.

(** * Joins *)

(** The join is the pushout of two types under their product. *)
Section Join.

  Definition Join (A : Type@{i}) (B : Type@{j})
    := Pushout@{k i j k} (@fst A B) (@snd A B).

  Definition joinl {A B} : A -> Join A B
    := fun a => @pushl (A*B) A B fst snd a.

  Definition joinr {A B} : B -> Join A B
    := fun b => @pushr (A*B) A B fst snd b.

  Definition jglue {A B} a b : joinl a = joinr b
    := @pglue (A*B) A B fst snd (a , b).

  Definition Join_ind {A B : Type} (P : Join A B -> Type)
    (P_A : forall a, P (joinl a)) (P_B : forall b, P (joinr b))
    (P_g : forall a b, DPath P (jglue a b) (P_A a) (P_B b))
    : forall (x : Join A B), P x.
  Proof.
    serapply (Pushout_ind P P_A P_B).
    intros [a b].
    apply dp_path_transport^-1.
    exact (P_g a b).
  Defined.

  Definition Join_ind_beta_jglue {A B : Type} (P : Join A B -> Type)
    (P_A : forall a, P (joinl a)) (P_B : forall b, P (joinr b))
    (P_g : forall a b, DPath P (jglue a b) (P_A a) (P_B b)) a b
    : dp_apD (Join_ind P P_A P_B P_g) (jglue a b) = P_g a b.
  Proof.
    apply dp_apD_path_transport.
    serapply Pushout_ind_beta_pglue.
  Defined.

  Definition Join_rec {A B P : Type} (P_A : A -> P) (P_B : B -> P)
    (P_g : forall a b, P_A a = P_B b) : Join A B -> P.
  Proof.
    serapply (Pushout_rec P P_A P_B).
    intros [a b].
    apply P_g.
  Defined.

  Definition Join_rec_beta_jglue {A B P : Type} (P_A : A -> P)
    (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a b
    : ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b.
  Proof.
    serapply Pushout_rec_beta_pglue.
  Defined.

  (** Joining with a contractible type produces a contractible type *)
  Global Instance contr_join A B `{Contr A} : Contr (Join A B).
  Proof.
    exists (pushl (center A)).
    intros y; simple refine (Pushout_ind _ _ _ _ y).
    - intros a; apply ap, contr.
    - intros b; exact (pglue (center A , b)).
    - intros [a b]; cbn.
      refine ( _ @ apD (fun a' => jglue a' b) (contr a)^).
      rewrite transport_paths_r, transport_paths_FlFr; cbn.
      rewrite ap_V, inv_V, concat_pp_p.
      rewrite ap_const, concat_p1.
      reflexivity.
  Defined.

  (** Join is symmetric *)
  Definition join_sym A B : Join A B <~> Join B A.
  Proof.
    unfold Join; refine (pushout_sym oE _).
    refine (equiv_pushout (equiv_prod_symm A B) 1 1 _ _);
      intros [a b]; reflexivity.
  Defined.

  Definition join_natsq_v {A B : Type} {a a' : A} {b b' : B}
    (p : a = a') (q : b = b')
    : PathSquare (ap joinl p) (ap joinr q) (jglue a b) (jglue a' b').
  Proof.
    destruct p, q.
    apply sq_refl_v.
  Defined.

  Definition join_natsq_h {A B : Type} {a a' : A} {b b' : B}
    (p : a = a') (q : b = b')
    : PathSquare (jglue a b) (jglue a' b') (ap joinl p) (ap joinr q).
  Proof.
    destruct p, q.
    apply sq_refl_h.
  Defined.

  Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
    : Join A B -> Join C D.
  Proof.
    serapply Join_rec.
    1: intro a; apply joinl, f, a.
    1: intro b; apply joinr, g, b.
    intros a b.
    apply jglue.
  Defined.

  Definition functor_join_compose {A B C D E F}
    (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F)
    : functor_join (h o f) (i o g) == functor_join h i o functor_join f g.
  Proof.
    serapply Join_ind.
    1,2: reflexivity.
    intros a b.
    simpl.
    apply sq_dp^-1.
    apply sq_1G.
    symmetry.
    rewrite ap_compose.
    rewrite 3 Join_rec_beta_jglue.
    reflexivity.
  Defined.

  Definition functor_join_idmap {A}
    : functor_join idmap idmap == (idmap : Join A A -> Join A A).
  Proof.
    serapply Join_ind.
    1,2: reflexivity.
    intros a b.
    cbn; apply dp_paths_FlFr.
    rewrite Join_rec_beta_jglue.
    rewrite ap_idmap, concat_p1.
    apply concat_Vp.
  Defined.

  Global Instance isequiv_functor_join {A B C D}
    (f : A -> C) `{!IsEquiv f} (g : B -> D) `{!IsEquiv g}
    : IsEquiv (functor_join f g).
  Proof.
    serapply isequiv_adjointify.
    1: apply (functor_join f^-1 g^-1).
    1,2: serapply Join_ind.
    1,2: intro; simpl; apply ap, eisretr.
    2,3: intro; simpl; apply ap, eissect.
    1,2: intros c d.
    1,2: apply sq_dp^-1.
     1 : rewrite (ap_compose _ (functor_join f g)).
     2 : rewrite (ap_compose (functor_join f g)).
    1,2: rewrite 2 Join_rec_beta_jglue, ap_idmap.
    1,2: apply join_natsq_v.
  Defined.

  Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
    : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.

  (** The join of hprops is an hprop *)
  Global Instance ishprop_join `{Funext} A B `{IsHProp A} `{IsHProp B} : IsHProp (Join A B).
  Proof.
    apply hprop_inhabited_contr.
    unfold Join.
    refine (Pushout_rec _ _ _ (fun _ => path_ishprop _ _)).
    - intros a; apply contr_join.
      exact (contr_inhabited_hprop A a).
    - intros b; refine (trunc_equiv (Join B A) (join_sym B A)).
      apply contr_join.
      exact (contr_inhabited_hprop B b).
  Defined.

  (** And coincides with their disjunction *)
  Definition equiv_join_hor `{Funext} A B `{IsHProp A} `{IsHProp B}
    : Join A B <~> hor A B.
  Proof.
    apply equiv_iff_hprop.
    - refine (Pushout_rec _ (fun a => tr (inl a)) (fun b => tr (inr b)) (fun _ => path_ishprop _ _)).
    - apply Trunc_rec, push.
  Defined.

  (** Joins add connectivity *)
  Global Instance isconnected_join `{Univalence} {m n : trunc_index}
         (A B : Type) `{IsConnected m A} `{IsConnected n B}
    : IsConnected (m +2+ n) (Join A B).
  Proof.
    apply isconnected_from_elim; intros C ? k.
    pose proof (istrunc_extension_along_conn
                  (fun b:B => tt) (fun _ => C) (k o pushr)).
    unfold ExtensionAlong in *.
    transparent assert (f : (A -> {s : Unit -> C &
                                   forall x, s tt = k (pushr x)})).
    { intros a; exists (fun _ => k (pushl a)); intros b.
      exact (ap k (jglue a b)). }
    assert (h := isconnected_elim
                   m {s : Unit -> C & forall x : B, s tt = k (pushr x)} f).
    unfold NullHomotopy in *; destruct h as [[c g] h].
    exists (c tt).
    srefine (Pushout_ind _ _ _ _).
    - intros a; cbn. exact (ap10 (h a)..1 tt).
    - intros b; cbn. exact ((g b)^).
    - intros [a b].
      rewrite transport_paths_FlFr, ap_const, concat_p1; cbn.
      subst f; set (ha := h a); clearbody ha; clear h;
      assert (ha2 := ha..2); set (ha1 := ha..1) in *;
      clearbody ha1; clear ha; cbn in *.
      rewrite <- (inv_V (ap10 ha1 tt)).
      rewrite <- inv_pp.
      apply inverse2.
      refine (_ @ apD10 ha2 b); clear ha2.
      rewrite transport_forall_constant, transport_paths_FlFr.
      rewrite ap_const, concat_p1.
      reflexivity.
  Defined.

End Join.

(** Diamond lemmas for Join *)
Section Diamond.

  Context {A B : Type}.

  Definition Diamond (a a' : A) (b b' : B)
    := PathSquare (jglue a b) (jglue a' b')^ (jglue a b') (jglue a' b)^.

  Definition diamond_h {a a' : A} (b b' : B) (p : a = a')
    : Diamond a a' b b'.
  Proof.
    destruct p.
    apply sq_path.
    exact (concat_pV _ @ (concat_pV _)^).
  Defined.

  Definition diamond_v (a a' : A) {b b' : B} (p : b = b')
    : Diamond a a' b b'.
  Proof.
    destruct p.
    by apply sq_path.
  Defined.

  Lemma diamond_symm (a : A) (b : B)
    : diamond_v a a 1 = diamond_h b b 1.
  Proof.
    unfold diamond_v, diamond_h.
    symmetry; apply ap, concat_pV.
  Defined.

End Diamond.

Definition diamond_twist {A : Type} {a a' : A} (p : a = a')
  : DPath (fun x => Diamond a' x a x) p
    (diamond_v a' a 1) (diamond_h a a' 1).
Proof.
  destruct p.
  apply diamond_symm.
Defined.

repo: Universal-Algebra-in-HoTT


text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** The Cminor language after instruction selection. *)

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Events.
Require Import Values.
Require Import Memory.
Require Import Cminor.
Require Import Op.
Require Import Globalenvs.
Require Import Switch.
Require Import Smallstep.
Require Import BuiltinFunctions.

(** * Abstract syntax *)

(** CminorSel programs share the general structure of Cminor programs:
  functions, statements and expressions.  However, CminorSel uses
  machine-dependent operations, addressing modes and conditions,
  as defined in module [Op] and used in lower-level intermediate
  languages ([RTL] and below).  Moreover, to express sharing of
  sub-computations, a "let" binding is provided (constructions
  [Elet] and [Eletvar]), using de Bruijn indices to refer to "let"-bound
  variables. *)

Inductive expr : Type :=
  | Evar : ident -> expr
  | Eop : operation -> exprlist -> expr
  | Eload : memory_chunk -> addressing -> exprlist -> expr
  | Econdition : condition -> exprlist -> expr -> expr -> expr
  | Elet : expr -> expr -> expr
  | Eletvar : nat -> expr

with exprlist : Type :=
  | Enil: exprlist
  | Econs: expr -> exprlist -> exprlist.

Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.

(** Statements are as in Cminor, except that the [Sifthenelse]
  construct uses a machine-dependent condition (with multiple
  arguments), and the [Sstore] construct uses a machine-dependent
  addressing mode. *)

Inductive stmt : Type :=
  | Sskip: stmt
  | Sassign : ident -> expr -> stmt
  | Sstore : memory_chunk -> addressing -> exprlist -> expr -> stmt
  | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt
  | Stailcall: signature -> expr + ident -> exprlist -> stmt
  | Sbuiltin : option ident -> builtin_function -> exprlist -> stmt
  | Sseq: stmt -> stmt -> stmt
  | Sifthenelse: condition -> exprlist -> stmt -> stmt -> stmt
  | Sloop: stmt -> stmt
  | Sblock: stmt -> stmt
  | Sexit: nat -> stmt
  | Sswitch: expr -> list (int * nat) -> nat -> stmt
  | Sreturn: option expr -> stmt
  | Slabel: label -> stmt -> stmt
  | Sgoto: label -> stmt.

Section WITHMEM.
Context `{Hcc: CompilerConfiguration}.

Record function : Type := mkfunction {
  fn_sig: signature;
  fn_params: list ident;
  fn_vars: list ident;
  fn_stackspace: Z;
  fn_body: stmt
}.

Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.

Definition funsig (fd: fundef) :=
  match fd with
  | Internal f => fn_sig f
  | External ef => ef_sig ef
  end.

(** * Operational semantics *)

(** Three kinds of evaluation environments are involved:
- [genv]: global environments, define symbols and functions;
- [env]: local environments, map local variables to values;
- [lenv]: let environments, map de Bruijn indices to values.
*)

Definition genv := Genv.t fundef unit.
Definition letenv := list val.

(** Continuations *)

Inductive cont: Type :=
  | Kstop: cont                         (**r stop program execution *)
  | Kseq: stmt -> cont -> cont          (**r execute stmt, then cont *)
  | Kblock: cont -> cont                (**r exit a block, then do cont *)
  | Kcall: option ident -> function -> val -> env -> cont -> cont.
                                        (**r return to caller *)

(** States *)

Inductive state `{mem_ops: Mem.MemoryOps mem}: Type :=
  | State:                              (**r execution within a function *)
      forall (f: function)              (**r currently executing function  *)
             (s: stmt)                  (**r statement under consideration *)
             (k: cont)                  (**r its continuation -- what to do next *)
             (sp: val)                  (**r current stack pointer *)
             (e: env)                   (**r current local environment *)
             (m: mem),                  (**r current memory state *)
      state
  | Callstate:                          (**r invocation of a fundef  *)
      forall (f: fundef)                (**r fundef to invoke *)
             (args: list val)           (**r arguments provided by caller *)
             (k: cont)                  (**r what to do next  *)
             (m: mem),                  (**r memory state *)
      state
  | Returnstate:
      forall (v: val)                   (**r return value *)
             (k: cont)                  (**r what to do next *)
             (m: mem),                  (**r memory state *)
      state.

Section RELSEM.

Variable ge: genv.

(** The evaluation predicates have the same general shape as those
    of Cminor.  Refer to the description of Cminor semantics for
    the meaning of the parameters of the predicates. *)

Section EVAL_EXPR.

Variable sp: val.
Variable e: env.
Variable m: mem.

Inductive eval_expr: letenv -> expr -> val -> Prop :=
  | eval_Evar: forall le id v,
      PTree.get id e = Some v ->
      eval_expr le (Evar id) v
  | eval_Eop: forall le op al vl v,
      eval_exprlist le al vl ->
      eval_operation ge sp op vl m = Some v ->
      eval_expr le (Eop op al) v
  | eval_Eload: forall le chunk addr al vl vaddr v,
      eval_exprlist le al vl ->
      eval_addressing ge sp addr vl = Some vaddr ->
      Mem.loadv chunk m vaddr = Some v ->
      eval_expr le (Eload chunk addr al) v
  | eval_Econdition: forall le cond al b c vl vb v,
      eval_exprlist le al vl ->
      eval_condition cond vl m = Some vb ->
      eval_expr le (if vb then b else c) v ->
      eval_expr le (Econdition cond al b c) v
  | eval_Elet: forall le a b v1 v2,
      eval_expr le a v1 ->
      eval_expr (v1 :: le) b v2 ->
      eval_expr le (Elet a b) v2
  | eval_Eletvar: forall le n v,
      nth_error le n = Some v ->
      eval_expr le (Eletvar n) v

with eval_exprlist: letenv -> exprlist -> list val -> Prop :=
  | eval_Enil: forall le,
      eval_exprlist le Enil nil
  | eval_Econs: forall le a1 al v1 vl,
      eval_expr le a1 v1 -> eval_exprlist le al vl ->
      eval_exprlist le (Econs a1 al) (v1 :: vl).

Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop
  with eval_exprlist_ind2 := Minimality for eval_exprlist Sort Prop.

Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
  | eval_eos_e: forall le e v,
      eval_expr le e v ->
      eval_expr_or_symbol le (inl _ e) v
  | eval_eos_s: forall le id b,
      Genv.find_symbol ge id = Some b ->
      eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero).

End EVAL_EXPR.

(** Pop continuation until a call or stop *)

Fixpoint call_cont (k: cont) : cont :=
  match k with
  | Kseq s k => call_cont k
  | Kblock k => call_cont k
  | _ => k
  end.

Definition is_call_cont (k: cont) : Prop :=
  match k with
  | Kstop => True
  | Kcall _ _ _ _ _ => True
  | _ => False
  end.

(** Find the statement and manufacture the continuation
  corresponding to a label *)

Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
                    {struct s}: option (stmt * cont) :=
  match s with
  | Sseq s1 s2 =>
      match find_label lbl s1 (Kseq s2 k) with
      | Some sk => Some sk
      | None => find_label lbl s2 k
      end
  | Sifthenelse cond al s1 s2 =>
      match find_label lbl s1 k with
      | Some sk => Some sk
      | None => find_label lbl s2 k
      end
  | Sloop s1 =>
      find_label lbl s1 (Kseq (Sloop s1) k)
  | Sblock s1 =>
      find_label lbl s1 (Kblock k)
  | Slabel lbl' s' =>
      if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k
  | _ => None
  end.

(** One step of execution *)

Inductive step: state -> trace -> state -> Prop :=

  | step_skip_seq: forall f s k sp e m,
      step (State f Sskip (Kseq s k) sp e m)
        E0 (State f s k sp e m)
  | step_skip_block: forall f k sp e m,
      step (State f Sskip (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_skip_call: forall f k sp e m m',
      is_call_cont k ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f Sskip k (Vptr sp Int.zero) e m)
        E0 (Returnstate Vundef k m')

  | step_assign: forall f id a k sp e m v,
      eval_expr sp e m nil a v ->
      step (State f (Sassign id a) k sp e m)
        E0 (State f Sskip k sp (PTree.set id v e) m)

  | step_store: forall f chunk addr al b k sp e m vl v vaddr m',
      eval_exprlist sp e m nil al vl ->
      eval_expr sp e m nil b v ->
      eval_addressing ge sp addr vl = Some vaddr ->
      Mem.storev chunk m vaddr v = Some m' ->
      step (State f (Sstore chunk addr al b) k sp e m)
        E0 (State f Sskip k sp e m')

  | step_call: forall f optid sig a bl k sp e m vf vargs fd,
      eval_expr_or_symbol sp e m nil a vf ->
      eval_exprlist sp e m nil bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      step (State f (Scall optid sig a bl) k sp e m)
        E0 (Callstate fd vargs (Kcall optid f sp e k) m)

  | step_tailcall: forall f sig a bl k sp e m vf vargs fd m',
      eval_expr_or_symbol (Vptr sp Int.zero) e m nil a vf ->
      eval_exprlist (Vptr sp Int.zero) e m nil bl vargs ->
      Genv.find_funct ge vf = Some fd ->
      funsig fd = sig ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
        E0 (Callstate fd vargs (call_cont k) m')

  | step_builtin: forall f optid ef al k sp e m vl t v m',
      eval_exprlist sp e m nil al vl ->
      external_call ef ge vl m t v m' ->
      step (State f (Sbuiltin optid ef al) k sp e m)
         t (State f Sskip k sp (set_optvar optid v e) m')

  | step_seq: forall f s1 s2 k sp e m,
      step (State f (Sseq s1 s2) k sp e m)
        E0 (State f s1 (Kseq s2 k) sp e m)

  | step_ifthenelse: forall f cond al s1 s2 k sp e m vl b,
      eval_exprlist sp e m nil al vl ->
      eval_condition cond vl m = Some b ->
      step (State f (Sifthenelse cond al s1 s2) k sp e m)
        E0 (State f (if b then s1 else s2) k sp e m)

  | step_loop: forall f s k sp e m,
      step (State f (Sloop s) k sp e m)
        E0 (State f s (Kseq (Sloop s) k) sp e m)

  | step_block: forall f s k sp e m,
      step (State f (Sblock s) k sp e m)
        E0 (State f s (Kblock k) sp e m)

  | step_exit_seq: forall f n s k sp e m,
      step (State f (Sexit n) (Kseq s k) sp e m)
        E0 (State f (Sexit n) k sp e m)
  | step_exit_block_0: forall f k sp e m,
      step (State f (Sexit O) (Kblock k) sp e m)
        E0 (State f Sskip k sp e m)
  | step_exit_block_S: forall f n k sp e m,
      step (State f (Sexit (S n)) (Kblock k) sp e m)
        E0 (State f (Sexit n) k sp e m)

  | step_switch: forall f a cases default k sp e m n,
      eval_expr sp e m nil a (Vint n) ->
      step (State f (Sswitch a cases default) k sp e m)
        E0 (State f (Sexit (switch_target n default cases)) k sp e m)

  | step_return_0: forall f k sp e m m',
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f (Sreturn None) k (Vptr sp Int.zero) e m)
        E0 (Returnstate Vundef (call_cont k) m')
  | step_return_1: forall f a k sp e m v m',
      eval_expr (Vptr sp Int.zero) e m nil a v ->
      Mem.free m sp 0 f.(fn_stackspace) = Some m' ->
      step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m)
        E0 (Returnstate v (call_cont k) m')

  | step_label: forall f lbl s k sp e m,
      step (State f (Slabel lbl s) k sp e m)
        E0 (State f s k sp e m)

  | step_goto: forall f lbl k sp e m s' k',
      find_label lbl f.(fn_body) (call_cont k) = Some(s', k') ->
      step (State f (Sgoto lbl) k sp e m)
        E0 (State f s' k' sp e m)

  | step_internal_function: forall f vargs k m m' sp e,
      Mem.alloc m 0 f.(fn_stackspace) = (m', sp) ->
      set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
      step (Callstate (Internal f) vargs k m)
        E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
  | step_external_function: forall ef vargs k m t vres m',
      external_call ef ge vargs m t vres m' ->
      step (Callstate (External ef) vargs k m)
         t (Returnstate vres k m')

  | step_return: forall v optid f sp e k m,
      step (Returnstate v (Kcall optid f sp e k) m)
        E0 (State f Sskip k sp (set_optvar optid v e) m).

End RELSEM.

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = mksignature nil (Some Tint) ->
      initial_state p (Callstate f nil Kstop m0).

Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall r m,
      final_state (Returnstate (Vint r) Kstop m) r.

Definition semantics (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).

Hint Constructors eval_expr eval_exprlist: evalexpr.

(** * Lifting of let-bound variables *)

(** Instruction selection sometimes generate [Elet] constructs to
  share the evaluation of a subexpression.  Owing to the use of de
  Bruijn indices for let-bound variables, we need to shift de Bruijn
  indices when an expression [b] is put in a [Elet a b] context. *)

Fixpoint lift_expr (p: nat) (a: expr) {struct a}: expr :=
  match a with
  | Evar id => Evar id
  | Eop op bl => Eop op (lift_exprlist p bl)
  | Eload chunk addr bl => Eload chunk addr (lift_exprlist p bl)
  | Econdition cond al b c =>
      Econdition cond (lift_exprlist p al) (lift_expr p b) (lift_expr p c)
  | Elet b c => Elet (lift_expr p b) (lift_expr (S p) c)
  | Eletvar n =>
      if le_gt_dec p n then Eletvar (S n) else Eletvar n
  end

with lift_exprlist (p: nat) (a: exprlist) {struct a}: exprlist :=
  match a with
  | Enil => Enil
  | Econs b cl => Econs (lift_expr p b) (lift_exprlist p cl)
  end.

Definition lift (a: expr): expr := lift_expr O a.

(** We now relate the evaluation of a lifted expression with that
    of the original expression. *)

Inductive insert_lenv: letenv -> nat -> val -> letenv -> Prop :=
  | insert_lenv_0:
      forall le v,
      insert_lenv le O v (v :: le)
  | insert_lenv_S:
      forall le p w le' v,
      insert_lenv le p w le' ->
      insert_lenv (v :: le) (S p) w (v :: le').

Lemma insert_lenv_lookup1:
  forall le p w le',
  insert_lenv le p w le' ->
  forall n v,
  nth_error le n = Some v -> (p > n)%nat ->
  nth_error le' n = Some v.
Proof.
  induction 1; intros.
  omegaContradiction.
  destruct n; simpl; simpl in H0. auto.
  apply IHinsert_lenv. auto. omega.
Qed.

Lemma insert_lenv_lookup2:
  forall le p w le',
  insert_lenv le p w le' ->
  forall n v,
  nth_error le n = Some v -> (p <= n)%nat ->
  nth_error le' (S n) = Some v.
Proof.
  induction 1; intros.
  simpl. assumption.
  simpl. destruct n. omegaContradiction.
  apply IHinsert_lenv. exact H0. omega.
Qed.

Lemma eval_lift_expr:
  forall ge sp e m w le a v,
  eval_expr ge sp e m le a v ->
  forall p le', insert_lenv le p w le' ->
  eval_expr ge sp e m le' (lift_expr p a) v.
Proof.
  intros until w.
  apply (eval_expr_ind2 ge sp e m
    (fun le a v =>
      forall p le', insert_lenv le p w le' ->
      eval_expr ge sp e m le' (lift_expr p a) v)
    (fun le al vl =>
      forall p le', insert_lenv le p w le' ->
      eval_exprlist ge sp e m le' (lift_exprlist p al) vl));
  simpl; intros; eauto with evalexpr.

  eapply eval_Econdition; eauto. destruct vb; eauto.

  eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto.

  case (le_gt_dec p n); intro.
  apply eval_Eletvar. eapply insert_lenv_lookup2; eauto.
  apply eval_Eletvar. eapply insert_lenv_lookup1; eauto.
Qed.

Lemma eval_lift:
  forall ge sp e m le a v w,
  eval_expr ge sp e m le a v ->
  eval_expr ge sp e m (w::le) (lift a) v.
Proof.
  intros. unfold lift. eapply eval_lift_expr.
  eexact H. apply insert_lenv_0.
Qed.

End WITHMEM.

Hint Constructors eval_expr eval_exprlist: evalexpr.
Hint Resolve eval_lift: evalexpr.

author: jeremie-koenig

repo: compcert


text:
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Converted imports: *)

Require Control.Monad.Fail.
Require Control.Monad.Signatures.
Require Control.Monad.Trans.Class.
Require Data.Functor.Identity.
Require Data.Tuple.
Require GHC.Base.
Import GHC.Base.Notations.

(* Converted type declarations: *)

Inductive StateT s m a : Type
  := | Mk_StateT (runStateT : s -> m (a * s)%type) : StateT s m a.

Definition State s :=
  (StateT s Data.Functor.Identity.Identity)%type.

Arguments Mk_StateT {_} {_} {_} _.

Definition runStateT {s} {m} {a} (arg_0__ : StateT s m a) :=
  let 'Mk_StateT runStateT := arg_0__ in
  runStateT.

(* Converted value declarations: *)

Local Definition Functor__StateT_fmap {inst_m} {inst_s} `{(GHC.Base.Functor
   inst_m)}
   : forall {a} {b},
     (a -> b) -> (StateT inst_s inst_m) a -> (StateT inst_s inst_m) b :=
  fun {a} {b} =>
    fun f m =>
      Mk_StateT (fun s =>
                   GHC.Base.fmap (fun '(pair a s') => pair (f a) s') (runStateT m s)).

Local Definition Functor__StateT_op_zlzd__ {inst_m} {inst_s} `{(GHC.Base.Functor
   inst_m)}
   : forall {a} {b}, a -> (StateT inst_s inst_m) b -> (StateT inst_s inst_m) a :=
  fun {a} {b} => Functor__StateT_fmap GHC.Base.∘ GHC.Base.const.

Program Instance Functor__StateT {m} {s} `{(GHC.Base.Functor m)}
   : GHC.Base.Functor (StateT s m) :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a} {b} => Functor__StateT_fmap ;
           GHC.Base.op_zlzd____ := fun {a} {b} => Functor__StateT_op_zlzd__ |}.

Local Definition Applicative__StateT_op_zlztzg__ {inst_m} {inst_s}
  `{GHC.Base.Functor inst_m} `{GHC.Base.Monad inst_m}
   : forall {a} {b},
     (StateT inst_s inst_m) (a -> b) ->
     (StateT inst_s inst_m) a -> (StateT inst_s inst_m) b :=
  fun {a} {b} =>
    fun arg_0__ arg_1__ =>
      match arg_0__, arg_1__ with
      | Mk_StateT mf, Mk_StateT mx =>
          Mk_StateT (fun s =>
                       let cont_2__ arg_3__ :=
                         let 'pair f s' := arg_3__ in
                         let cont_4__ arg_5__ :=
                           let 'pair x s'' := arg_5__ in
                           GHC.Base.return_ (pair (f x) s'') in
                         mx s' GHC.Base.>>= cont_4__ in
                       mf s GHC.Base.>>= cont_2__)
      end.

Local Definition Applicative__StateT_liftA2 {inst_m} {inst_s} `{GHC.Base.Functor
  inst_m} `{GHC.Base.Monad inst_m}
   : forall {a} {b} {c},
     (a -> b -> c) ->
     (StateT inst_s inst_m) a ->
     (StateT inst_s inst_m) b -> (StateT inst_s inst_m) c :=
  fun {a} {b} {c} =>
    fun f x => Applicative__StateT_op_zlztzg__ (GHC.Base.fmap f x).

Local Definition Applicative__StateT_pure {inst_m} {inst_s} `{GHC.Base.Functor
  inst_m} `{GHC.Base.Monad inst_m}
   : forall {a}, a -> (StateT inst_s inst_m) a :=
  fun {a} => fun a => Mk_StateT (fun s => GHC.Base.return_ (pair a s)).

Definition Applicative__StateT_op_ztzg__ {inst_m} {inst_s} `{_
   : GHC.Base.Functor inst_m} `{_ : GHC.Base.Monad inst_m}
   : forall {a} {b},
     StateT inst_s inst_m a -> StateT inst_s inst_m b -> StateT inst_s inst_m b :=
  fun {a} {b} =>
    fun m k =>
      Applicative__StateT_op_zlztzg__ (Applicative__StateT_op_zlztzg__
                                       (Applicative__StateT_pure (fun x y => x)) k) m.

Program Instance Applicative__StateT {m} {s} `{GHC.Base.Functor m}
  `{GHC.Base.Monad m}
   : GHC.Base.Applicative (StateT s m) :=
  fun _ k__ =>
    k__ {| GHC.Base.liftA2__ := fun {a} {b} {c} => Applicative__StateT_liftA2 ;
           GHC.Base.op_zlztzg____ := fun {a} {b} => Applicative__StateT_op_zlztzg__ ;
           GHC.Base.op_ztzg____ := fun {a} {b} => Applicative__StateT_op_ztzg__ ;
           GHC.Base.pure__ := fun {a} => Applicative__StateT_pure |}.

(* Skipping all instances of class `GHC.Base.Alternative', including
   `Control.Monad.Trans.State.Lazy.Alternative__StateT' *)

Local Definition Monad__StateT_op_zgzgze__ {inst_m} {inst_s} `{(GHC.Base.Monad
   inst_m)}
   : forall {a} {b},
     (StateT inst_s inst_m) a ->
     (a -> (StateT inst_s inst_m) b) -> (StateT inst_s inst_m) b :=
  fun {a} {b} =>
    fun m k =>
      Mk_StateT (fun s =>
                   let cont_0__ arg_1__ := let 'pair a s' := arg_1__ in runStateT (k a) s' in
                   runStateT m s GHC.Base.>>= cont_0__).

Local Definition Monad__StateT_op_zgzg__ {inst_m} {inst_s} `{(GHC.Base.Monad
   inst_m)}
   : forall {a} {b},
     (StateT inst_s inst_m) a ->
     (StateT inst_s inst_m) b -> (StateT inst_s inst_m) b :=
  fun {a} {b} => fun m k => Monad__StateT_op_zgzgze__ m (fun arg_0__ => k).

Local Definition Monad__StateT_return_ {inst_m} {inst_s} `{(GHC.Base.Monad
   inst_m)}
   : forall {a}, a -> (StateT inst_s inst_m) a :=
  fun {a} => GHC.Base.pure.

Program Instance Monad__StateT {m} {s} `{(GHC.Base.Monad m)}
   : GHC.Base.Monad (StateT s m) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zgzg____ := fun {a} {b} => Monad__StateT_op_zgzg__ ;
           GHC.Base.op_zgzgze____ := fun {a} {b} => Monad__StateT_op_zgzgze__ ;
           GHC.Base.return___ := fun {a} => Monad__StateT_return_ |}.

Local Definition MonadFail__StateT_fail {inst_m} {inst_s}
  `{(Control.Monad.Fail.MonadFail inst_m)}
   : forall {a}, GHC.Base.String -> (StateT inst_s inst_m) a :=
  fun {a} => fun str => Mk_StateT (fun arg_0__ => Control.Monad.Fail.fail str).

Program Instance MonadFail__StateT {m} {s} `{(Control.Monad.Fail.MonadFail m)}
   : Control.Monad.Fail.MonadFail (StateT s m) :=
  fun _ k__ =>
    k__ {| Control.Monad.Fail.fail__ := fun {a} => MonadFail__StateT_fail |}.

(* Skipping all instances of class `GHC.Base.MonadPlus', including
   `Control.Monad.Trans.State.Lazy.MonadPlus__StateT' *)

(* Skipping all instances of class `Control.Monad.Fix.MonadFix', including
   `Control.Monad.Trans.State.Lazy.MonadFix__StateT' *)

Local Definition MonadTrans__StateT_lift {inst_s}
   : forall {m} {a}, forall `{(GHC.Base.Monad m)}, m a -> (StateT inst_s) m a :=
  fun {m} {a} `{(GHC.Base.Monad m)} =>
    fun m =>
      Mk_StateT (fun s => m GHC.Base.>>= (fun a => GHC.Base.return_ (pair a s))).

Program Instance MonadTrans__StateT {s}
   : Control.Monad.Trans.Class.MonadTrans (StateT s) :=
  fun _ k__ =>
    k__ {| Control.Monad.Trans.Class.lift__ := fun {m} {a} `{(GHC.Base.Monad m)} =>
             MonadTrans__StateT_lift |}.

(* Skipping all instances of class `Control.Monad.IO.Class.MonadIO', including
   `Control.Monad.Trans.State.Lazy.MonadIO__StateT' *)

Definition state {m} {s} {a} `{(GHC.Base.Monad m)}
   : (s -> (a * s)%type) -> StateT s m a :=
  fun f => Mk_StateT (GHC.Base.return_ GHC.Base.∘ f).

Definition runState {s} {a} : State s a -> s -> (a * s)%type :=
  fun m => Data.Functor.Identity.runIdentity GHC.Base.∘ runStateT m.

Definition evalState {s} {a} : State s a -> s -> a :=
  fun m s => Data.Tuple.fst (runState m s).

Definition execState {s} {a} : State s a -> s -> s :=
  fun m s => Data.Tuple.snd (runState m s).

Definition mapStateT {m} {a} {s} {n} {b}
   : (m (a * s)%type -> n (b * s)%type) -> StateT s m a -> StateT s n b :=
  fun f m => Mk_StateT (f GHC.Base.∘ runStateT m).

Definition mapState {a} {s} {b}
   : ((a * s)%type -> (b * s)%type) -> State s a -> State s b :=
  fun f =>
    mapStateT (Data.Functor.Identity.Mk_Identity GHC.Base.∘
               (f GHC.Base.∘ Data.Functor.Identity.runIdentity)).

Definition withStateT {s} {m} {a} : (s -> s) -> StateT s m a -> StateT s m a :=
  fun f m => Mk_StateT (runStateT m GHC.Base.∘ f).

Definition withState {s} {a} : (s -> s) -> State s a -> State s a :=
  withStateT.

Definition evalStateT {m} {s} {a} `{(GHC.Base.Monad m)}
   : StateT s m a -> s -> m a :=
  fun m s =>
    let cont_0__ arg_1__ := let 'pair a _ := arg_1__ in GHC.Base.return_ a in
    runStateT m s GHC.Base.>>= cont_0__.

Definition execStateT {m} {s} {a} `{(GHC.Base.Monad m)}
   : StateT s m a -> s -> m s :=
  fun m s =>
    let cont_0__ arg_1__ := let 'pair _ s' := arg_1__ in GHC.Base.return_ s' in
    runStateT m s GHC.Base.>>= cont_0__.

Definition get {m} {s} `{(GHC.Base.Monad m)} : StateT s m s :=
  state (fun s => pair s s).

Definition put {m} {s} `{(GHC.Base.Monad m)} : s -> StateT s m unit :=
  fun s => state (fun arg_0__ => pair tt s).

Definition modify {m} {s} `{(GHC.Base.Monad m)} : (s -> s) -> StateT s m unit :=
  fun f => state (fun s => pair tt (f s)).

Definition modify' {m} {s} `{(GHC.Base.Monad m)}
   : (s -> s) -> StateT s m unit :=
  fun f => get GHC.Base.>>= (fun s => put (f s)).

Definition gets {m} {s} {a} `{(GHC.Base.Monad m)} : (s -> a) -> StateT s m a :=
  fun f => state (fun s => pair (f s) s).

Definition liftCallCC {m} {a} {s} {b}
   : Control.Monad.Signatures.CallCC m (a * s)%type (b * s)%type ->
     Control.Monad.Signatures.CallCC (StateT s m) a b :=
  fun callCC f =>
    Mk_StateT (fun s =>
                 callCC (fun c =>
                           runStateT (f (fun a => Mk_StateT (fun arg_0__ => c (pair a s)))) s)).

Definition liftCallCC' {m} {a} {s} {b}
   : Control.Monad.Signatures.CallCC m (a * s)%type (b * s)%type ->
     Control.Monad.Signatures.CallCC (StateT s m) a b :=
  fun callCC f =>
    Mk_StateT (fun s =>
                 callCC (fun c =>
                           runStateT (f (fun a => Mk_StateT (fun s' => c (pair a s')))) s)).

(* Skipping definition `Control.Monad.Trans.State.Lazy.liftCatch' *)

Definition liftListen {m} {w} {a} {s} `{(GHC.Base.Monad m)}
   : Control.Monad.Signatures.Listen w m (a * s)%type ->
     Control.Monad.Signatures.Listen w (StateT s m) a :=
  fun listen m =>
    Mk_StateT (fun s =>
                 let cont_0__ arg_1__ :=
                   let 'pair (pair a s') w := arg_1__ in
                   GHC.Base.return_ (pair (pair a w) s') in
                 listen (runStateT m s) GHC.Base.>>= cont_0__).

Definition liftPass {m} {w} {a} {s} `{(GHC.Base.Monad m)}
   : Control.Monad.Signatures.Pass w m (a * s)%type ->
     Control.Monad.Signatures.Pass w (StateT s m) a :=
  fun pass m =>
    Mk_StateT (fun s =>
                 pass (let cont_0__ arg_1__ :=
                         let 'pair (pair a f) s' := arg_1__ in
                         GHC.Base.return_ (pair (pair a s') f) in
                       runStateT m s GHC.Base.>>= cont_0__)).

(* External variables:
     op_zt__ pair tt unit Control.Monad.Fail.MonadFail Control.Monad.Fail.fail
     Control.Monad.Fail.fail__ Control.Monad.Signatures.CallCC
     Control.Monad.Signatures.Listen Control.Monad.Signatures.Pass
     Control.Monad.Trans.Class.MonadTrans Control.Monad.Trans.Class.lift__
     Data.Functor.Identity.Identity Data.Functor.Identity.Mk_Identity
     Data.Functor.Identity.runIdentity Data.Tuple.fst Data.Tuple.snd
     GHC.Base.Applicative GHC.Base.Functor GHC.Base.Monad GHC.Base.String
     GHC.Base.const GHC.Base.fmap GHC.Base.fmap__ GHC.Base.liftA2__
     GHC.Base.op_z2218U__ GHC.Base.op_zgzg____ GHC.Base.op_zgzgze__
     GHC.Base.op_zgzgze____ GHC.Base.op_zlzd____ GHC.Base.op_zlztzg____
     GHC.Base.op_ztzg____ GHC.Base.pure GHC.Base.pure__ GHC.Base.return_
     GHC.Base.return___
*)

author: antalsz

repo: hs-to-coq

save_path: github-repos/coq/antalsz-hs-to-coq


text:
(** * Sort: Insertion Sort *)

(** Sorting can be done in expected O(N log N) time by various
    algorithms (quicksort, mergesort, heapsort, etc.).  But for
    smallish inputs, a simple quadratic-time algorithm such as
    insertion sort can actually be faster.  It's certainly easier to
    implement -- and to verify. *)

(** If you don't recall insertion sort or haven't seen it in
    a while, see Wikipedia or read any standard textbook; for example:

    - Sections 2.0 and 2.1 of _Algorithms, Fourth Edition_, by
      Sedgewick and Wayne, Addison Wesley 2011; or

    - Section 2.1 of _Introduction to Algorithms, 3rd Edition_, by
      Cormen, Leiserson, and Rivest, MIT Press 2009. *)

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From VFA Require Import Perm.

(* ################################################################# *)
(** * The Insertion-Sort Program *)

(** Insertion sort is usually presented as an imperative program
    operating on arrays.  But it works just as well as a functional
    program operating on linked lists. *)

(* [insert i l] inserts [i] into its sorted place in list [l].
   Precondition: [l] is sorted. *)
Fixpoint insert (i : nat) (l : list nat) :=
  match l with
  | [] => [i]
  | h :: t => if i <=? h then i :: h :: t else h :: insert i t
  end.

Fixpoint sort (l : list nat) : list nat :=
  match l with
  | [] => []
  | h :: t => insert h (sort t)
  end.

Example sort_pi :
  sort [3;1;4;1;5;9;2;6;5;3;5]
  = [1;1;2;3;3;4;5;5;5;6;9].
Proof. simpl. reflexivity. Qed.

(** What Sedgewick/Wayne and Cormen/Leiserson/Rivest don't acknowlege
    is that the arrays-and-swaps model of sorting is not the only one
    in the world.  We are writing _functional programs_, where our
    sequences are (typically) represented as linked lists, and where
    we do _not_ destructively splice elements into those lists. *)

(** As usual with functional lists, the output of [sort] may share
    memory with the input.  For example: *)

Compute insert 7 [1; 3; 4; 8; 12; 14; 18].
(* = [1; 3; 4; 7; 8; 12; 14; 18] *)

(** The tail of this list, [12 :: 14 :: 18 :: []], is not disturbed or
    rebuilt by the [insert] algorithm.  The head [1 :: 3 :: 4 :: 7 :: ...]
    contains new nodes constructed by [insert].  The first three nodes
    of the old list, [1 :: 3 :: 4 :: ...], will likely be
    garbage-collected if no other data structure is still pointing at
    them.  Thus, in this typical case,

     - Time cost = 4X

     - Space cost = (4-3)Y = Y

    where X and Y are constants, independent of the length of the
    tail.  The value Y is the number of bytes in one list node: 2 to 4
    words, depending on how the implementation handles
    constructor-tags.  We write (4-3) to indicate that four list nodes
    are constructed, while three list nodes become eligible for
    garbage collection.

    We will not prove such things about the time and space cost, but
    they are true anyway, and we should keep them in consideration. *)

(* ################################################################# *)
(** * Specification of Correctness *)

(** A sorting algorithm must rearrange the elements into a list
    that is totally ordered. There are many ways we might express that
    idea formally in Coq.  One is with an inductively-defined
    relation that says: *)

(** - The empty list is sorted.

    - Any single-element list is sorted.

    - For any two adjacent elements, they must be in the proper order. *)

Inductive sorted : list nat -> Prop :=
| sorted_nil :
    sorted []
| sorted_1 : forall x,
    sorted [x]
| sorted_cons : forall x y l,
    x <= y -> sorted (y :: l) -> sorted (x :: y :: l).

Hint Constructors sorted : core.

(** This definition might not be the most obvious. Another
    definition, perhaps more familiar, might be: for any two elements
    of the list (regardless of whether they are adjacent), they should
    be in the proper order.  Let's try formalizing that.

    We can think in terms of indices into a list [lst], and say: for
    any valid indices [i] and [j], if [i < j] then [index lst i <=
    index lst j], where [index lst n] means the element of [lst] at
    index [n].  Unfortunately, formalizing this idea becomes messy,
    because any Coq function implementing [index] must be total: it
    must return some result even if the index is out of range for the
    list.  The Coq standard library contains two such functions: *)

Check nth : forall A : Type, nat -> list A -> A -> A.
Check nth_error : forall A : Type, list A -> nat -> option A.

(** These two functions ensure totality in different ways:

    - [nth] takes an additional argument of type [A] --a _default_
      value-- to be returned if the index is out of range, whereas

    - [nth_error] returns [Some v] if the index is in range and [None]
      --an error-- otherwise.

    If we use [nth], we must ensure that indices are in range: *)

Definition sorted'' (al : list nat) := forall i j,
    i < j < length al ->
    nth i al 0 <= nth j al 0.

(** The choice of default value, here 0, is unimportant, because it
    will never be returned for the [i] and [j] we pass.

    If we use [nth_error], we must add additional antecedents: *)

Definition sorted' (al : list nat) := forall i j iv jv,
    i < j ->
    nth_error al i = Some iv ->
    nth_error al j = Some jv ->
    iv <= jv.

(** Here, the validity of [i] and [j] are implicit in the fact
    that we get [Some] results back from each call to [nth_error]. *)

(** All three definitions of sortedness are reasonable.  In practice,
    [sorted'] is easier to work with than [sorted''] because it
    doesn't need to mention the [length] function. And [sorted] is
    easiest, because it doesn't need to mention indices. *)

(** Using [sorted], we specify what it means to be a correct sorting
    algorthm: *)

Definition is_a_sorting_algorithm (f: list nat -> list nat) := forall al,
    Permutation al (f al) /\ sorted (f al).

(** Function [f] is a correct sorting algorithm if [f al] is
    [sorted] and is a permutation of its input. *)

(* ################################################################# *)
(** * Proof of Correctness *)

(** In the following exercises, you will prove the correctness of
    insertion sort. *)

(** **** Exercise: 3 stars, standard (insert_sorted) *)

(* Prove that insertion maintains sortedness. Make use of tactic
   [bdestruct], defined in [Perm]. *)

Lemma insert_sorted:
  forall a l, sorted l -> sorted (insert a l).
Proof.
  intros a l S. induction S; simpl.
  (* FILL IN HERE *) Admitted.

(** [] *)

(** **** Exercise: 2 stars, standard (sort_sorted) *)

(** Using [insert_sorted], prove that insertion sort makes a list
    sorted. *)

Theorem sort_sorted: forall l, sorted (sort l).
Proof.
  (* FILL IN HERE *) Admitted.

(** [] *)

(** **** Exercise: 3 stars, standard (insert_perm) *)

(** The following lemma will be useful soon as a helper. Take
    advantage of helpful theorems from the [Permutation] library. *)

Lemma insert_perm: forall x l,
    Permutation (x :: l) (insert x l).
Proof.
  (* FILL IN HERE *) Admitted.

(** [] *)

(** **** Exercise: 3 stars, standard (sort_perm) *)

(** Prove that [sort] is a permutation, using [insert_perm]. *)

Theorem sort_perm: forall l, Permutation l (sort l).
Proof.
(* FILL IN HERE *) Admitted.

(** [] *)

(** **** Exercise: 1 star, standard (insertion_sort_correct) *)

(** Finish the proof of correctness! *)

Theorem insertion_sort_correct:
    is_a_sorting_algorithm sort.
Proof.
  (* FILL IN HERE *) Admitted.

(** [] *)

(* ################################################################# *)
(** * Validating the Specification (Advanced) *)

(** You can prove that a program satisfies a specification, but how
    can you prove you have the right specification?  Actually, you
    cannot.  The specification is an informal requirement in your
    mind.  As Alan Perlis quipped, "One can't proceed from the
    informal to the formal by formal means."

    But one way to build confidence in a specification is to state it
    in two different ways, then prove they are equivalent. *)

(** **** Exercise: 4 stars, advanced (sorted_sorted') *)
Lemma sorted_sorted': forall al, sorted al -> sorted' al.

(** Hint: Instead of doing induction on the list [al], do induction on
    the sortedness of [al]. This proof is a bit tricky, so you may
    have to think about how to approach it, and try out one or two
    different ideas.*)
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, advanced (sorted'_sorted) *)
Lemma sorted'_sorted : forall al, sorted' al -> sorted al.
Proof.
(** Here, you can't do induction on the sortedness of the list,
    because [sorted'] is not an inductive predicate. But the proof
    is less tricky than the previous. *)
(* FILL IN HERE *) Admitted.
(** [] *)

(* ################################################################# *)
(** * Proving Correctness from the Alternative Spec (Optional) *)

(** Depending on how you write the specification of a program, it can
    be harder or easier to prove correctness.  We saw that predicates
    [sorted] and [sorted'] are equivalent.  It is significantly
    harder, though, to prove correctness of insertion sort directly
    from [sorted'].

    Give it a try!  The best proof we know of makes essential use of
    the auxiliary lemma [nth_error_insert], so you may want to prove
    that first.  And some other auxiliary lemmas may be needed too.
    But maybe you will find a simpler appraoch!

    DO NOT USE [sorted_sorted'], [sorted'_sorted], [insert_sorted], or
    [sort_sorted] in these proofs.  That would defeat the purpose! *)

(** **** Exercise: 5 stars, standard, optional (insert_sorted') *)

Lemma nth_error_insert : forall l a i iv,
    nth_error (insert a l) i = Some iv ->
    a = iv \/ exists i', nth_error l i' = Some iv.
Proof.
(* FILL IN HERE *) Admitted.

Lemma insert_sorted':
  forall a l, sorted' l -> sorted' (insert a l).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)

Theorem sort_sorted': forall l, sorted' (sort l).
Proof.
  induction l.
  - unfold sorted'. intros. destruct i; inv H0.
  - simpl. apply insert_sorted'. auto.
Qed.

(** If you complete the proofs above, you will note that the proof of
    [insert_sorted] is relatively easy compared to the proof of
    [insert_sorted'], even though [sorted al <-> sorted' al].  So,
    suppose someone asked you to prove [sort_sorted'].  Instead of
    proving it directly, it would be much easier to design predicate
    [sorted], then prove [sort_sorted] and [sorted_sorted'].

    The moral of the story is therefore: _Different formulations of
    the functional specification can lead to great differences in the
    difficulty of the correctness proofs_. *)

(* 2022-08-08 17:36 *)

repo: SoftwareFoundationBackup


text:
From mathcomp Require Import all_ssreflect all_algebra.
Require Import tactics binomialz seq_defs.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope ring_scope.

(**** Properties of the sequence c ****)

Fact lt_0_c (i j : int) : 0 <= j <= i -> 0 < c i j.
Proof.
case/andP=> h0j hji; rewrite /c -expfzMl.
by apply/exprz_gt0/mulr_gt0; rewrite ltr0z binz_gt0; lia.
Qed.

(* c is monotonic wrt its first argument *)
Fact c_incr (n m i : int) : 0 <= n -> 0 <= i -> i <= n -> n <= m ->
                            c n i <= c m i.
Proof.
case: n m i => [] // n [] // m [] // i _ _ lein lenm; rewrite /c.
rewrite -!PoszD !binz_nat_nat -!expfzMl -!rmorphM /= !exprz_pintl // ler_nat.
by apply: leq_mul; apply: leq_mul; apply: leq_bin2l; lia.
Qed.

author: coq-community

repo: apery

save_path: github-repos/coq/coq-community-apery


text:
(** A little module for doing naive congruence closure; we don't need anything
    much fancier because in practice, for spatial entailments, we only discover
    a few new equalities in each call to the superposition subsystem.

    Pure entailments are another matter entirely, but for now we seem to be fine
    on those (see, eg, test/test.pure.entailments.sf) *)

Load loadpath.
Require Import List veric.Coqlib2 msl.base.
Require Import VST.msl.predicates_sa.
Require Import veristar.datatypes veristar.clauses veristar.clause_lemmas
               veristar.list_denote veristar.basic veristar.compare.
Require Import veristar.model_type veristar.model.

Section cclosure.
Context (A B : Type).
Variables
  (A_cmp : A -> A -> comparison)
  (B_cmp : B -> B -> comparison)
  (fAB : A -> B).

Notation canons := (list (A*B)).

(*Definition isEq (c : comparison) := match c with Eq => true | _ => false end.*)

Fixpoint lookC (a: A) (cs: canons) : B :=
  match cs with nil => fAB a
  | (a1, b1)::cs' => if isEq (A_cmp a a1) then b1
                     else lookC a cs'
  end.

Fixpoint rewriteC (b1 b2 : B) (cs: canons) : canons :=
  match cs with nil => nil
  | (a1, b1')::cs' =>
    let new_cs := rewriteC b1 b2 cs' in
    if isEq (B_cmp b1 b1') then (a1, b2)::new_cs else (a1, b1')::new_cs end.

Definition mergeC (a1 a2 : A) (cs: canons) : canons :=
  match lookC a1 cs, lookC a2 cs with b1, b2 =>
    if isEq (B_cmp b1 b2) then cs
    else (a1, b2)::(a2, b2)::rewriteC b1 b2 cs end.

(* sanity lemmas *)
(*
Lemma lookC_cons a1 b cs : lookC a1 ((a1, b)::cs) = b.
Proof. unfold lookC; simpl. if_tac; auto. exfalso; apply H; auto. Qed.

Lemma lookC_cons2 a1 a2 b cs :
  lookC a1 ((a2, b)::cs) = if A_eq_dec a1 a2 then b else lookC a1 cs.
Proof. unfold lookC; simpl. if_tac; auto. Qed.

Lemma mergeC_lookC a1 a2 cs :
  lookC a1 (mergeC a1 a2 cs) = lookC a2 (mergeC a1 a2 cs).
Proof with simpl; auto; try solve[congruence].
induction cs... unfold mergeC. if_tac... if_tac... if_tac... if_tac...
unfold mergeC; if_tac; auto.
rewrite lookC_cons. rewrite lookC_cons2. if_tac; auto. rewrite lookC_cons...
Qed.
*)
End cclosure.

(*
Module TestCClosure.
Require Import NatOrderedType. Import Nat_as_DT.

Notation lookC := (lookC _ _ eq_dec (fun n => n)).
Notation rewriteC := (@rewriteC nat nat eq_dec).
Notation mergeC := (mergeC _ _ eq_dec eq_dec (fun n => n)).

Compute mergeC 1 2 nil.
Compute mergeC 1 2 (mergeC 3 4 nil).
Compute lookC 3 (mergeC 1 2 (mergeC 3 4 (mergeC 5 6 nil))).
Compute lookC 3 (mergeC 4 5 (mergeC 3 4 (mergeC 5 6 nil))).
Compute lookC 3 (mergeC 1 8 (mergeC 3 4 (mergeC 1 3 (mergeC 1 2 nil)))).

End TestCClosure.
*)

Notation expr_get := (lookC _ _ expr_cmp (@id _)).
Notation expr_merge := (mergeC _ _ expr_cmp expr_cmp (@id _)).

(* used internally *)
Local Notation expr_rewriteC := (rewriteC expr _ expr_cmp).

Fixpoint cclose_aux (l : list clause) : list (expr * expr) :=
  match l with
  | PureClause nil [Eqv s t] _ _ :: l' => expr_merge s t (cclose_aux l')
  | _ => nil
  end.

Definition cclose (l : list clause) : list clause :=
  map (fun p => match p with (e1, e2) => mkPureClause nil [Eqv e1 e2] end)
    (cclose_aux l).

(** Correctness proof *)

Module CCSound (VSM : VERISTAR_MODEL).
Import VSM VeriStarLogic.

Definition expr_eqs_denote (l : list (expr * expr)) :=
  listd (fun p => match p with (e1, e2) => (e1 === e2) end) inter TT l.

Lemma expr_get_sound e l s : expr_eqs_denote l s -> (e === expr_get e l) s.
Proof with simpl; auto.
induction l... unfold id... intros; apply var_eq_refl.
destruct a. intros [H1 H2]. remember (expr_cmp e e0) as b. destruct b...
assert (H3 : true = expr_eq e e0). unfold expr_eq. rewrite <-Heqb...
apply expr_eq_eq' in H3; subst...
Qed.

Lemma expr_rewriteC_sound e1 e2 l s :
  (e1 === e2) s -> expr_eqs_denote l s ->
  expr_eqs_denote (expr_rewriteC e1 e2 l) s.
Proof with simpl; auto.
intros H0; induction l... intros [H1 H2]; destruct a as [e e0].
spec IHl H2. remember (isEq (expr_cmp e1 e0)). destruct b...
split; auto.
apply var_eq_trans with (y:=e0)...
apply var_eq_trans with (y:=e1)...
do_comp expr_cspec e1 e0; try solve[simpl in Heqb; congruence].
split; auto.
Qed.

Lemma expr_merge_sound e1 e2 l s :
  expr_eqs_denote l s -> (e1 === e2) s ->
  expr_eqs_denote (expr_merge e1 e2 l) s.
Proof with simpl; auto.
induction l... unfold lookC, mergeC, id... if_tac... firstorder.
destruct a. intros [H1 H2]. unfold mergeC.
remember (isEq (expr_cmp (expr_get e1 ((e, e0) :: l))
                             (expr_get e2 ((e, e0) :: l)))) as b.
destruct b. simpl. intros H3. split; auto.
intros H3. unfold expr_eqs_denote. rewrite listd_cons.
split; auto.
assert (H4 : (e2 === expr_get e2 ((e, e0) :: l)) s).
  apply expr_get_sound. simpl. split; auto.
apply var_eq_trans with (y:=e2); auto.
rewrite listd_cons. split.
apply expr_get_sound. simpl. split; auto.
apply expr_rewriteC_sound.
assert (H4 : (e1 === expr_get e1 ((e, e0) :: l)) s).
  apply expr_get_sound... split...
apply var_eq_trans with (y:=e1). apply var_eq_sym; auto.
apply var_eq_trans with (y:=e2); auto. apply expr_get_sound.
split; auto.
simpl; split; auto.
Qed.

Lemma cclose_aux_sound l s :
  listd clause_denote inter TT l s -> expr_eqs_denote (cclose_aux l) s.
Proof with simpl; auto.
induction l...
destruct a... destruct gamma... destruct delta...
destruct p... destruct delta...
intros [H1 H2]. simpl in H1. spec H1. auto.
inversion H1 as [H3|H3]; [|inversion H3].
apply expr_merge_sound...
Qed.

Lemma cclose_sound l s :
  listd clause_denote inter TT l s -> listd clause_denote inter TT (cclose l) s.
Proof.
intros H1. unfold cclose. apply listd_map_pred
  with (f:=(fun p => match p with (e1, e2) => (e1 === e2) end)).
intros [a1 a2]; simpl; firstorder.
apply cclose_aux_sound; auto.
Qed.

End CCSound.

author: PrincetonUniversity

repo: VST