From ASCommon Require Import Options.
From ASCommon Require Import Common GRel FMon.

Require Import RiscVInst.
Require Import GenAxiomaticRiscV.

Section UMRiscV.
  Import Candidate.
  Context (regs_whitelist : gset reg).
  Context {nmth : nat}.
  Context (cd : Candidate.t NMS nmth).

  Import AxRiscVNames.

  Notation pe := (pre_exec cd).
  Notation int := (same_thread pe).
  Notation si := (same_instruction_instance cd).
  Notation sca := (same_access cd).
  Notation po := (instruction_order pe).
  Notation full_instruction_order := (full_instruction_order pe).
  Notation iio := (iio pe).

  Notation addr := (addr cd).
  Notation data := (data cd).
  Notation ctrl := (ctrl cd).

  Notation RR := (reg_reads pe).
  Notation RW := (reg_writes pe).
  Notation RE := (RE cd).
  Notation rrf := (reg_reads_from cd).
  Notation rfr := (reg_from_reads cd).

  Notation fences a b := (fences a b pe).
  Notation fences_tso := (fences_tso pe).
  Notation fences_i := (fences_i pe).

  Notation W := (explicit_writes pe).
  Notation R := (explicit_reads pe).
  Notation M := (mem_explicit pe).
  Notation Wx := (exclusive_writes pe).
  Notation Rx := (exclusive_writes pe).
  Notation X := (mem_exclusive pe).
  Notation RL := (RL cd).
  Notation AQ := (AQ cd).
  Notation RCsc := (mem_rel_acq_rcsc pe).
  Notation IF := (ifetch_reads pe).
  Notation IR := (init_mem_reads cd).

  Notation lxsx := (lxsx cd).
  Notation amo := (atomic_update cd).
  Notation rmw := (rmw cd).

  Notation co := (co cd).
  Notation coi := (coi cd).
  Notation coe := (coe cd).

  Notation rf := (rf cd).
  Notation rfi := (rfi cd).
  Notation rfe := (rfe cd).
  Notation fr := (fr cd).
  Notation fri := (fri cd).
  Notation fre := (fre cd).

  Notation rsw := (rsw cd).

  Notation irf := (irf cd).
  Notation irfi := (irfi cd).
  Notation irfe := (irfe cd).
  Notation ifr := (ifr cd).
  Notation ifri := (ifri cd).
  Notation ifre := (ifre cd).


  Definition is_illegal_reg_write (regs : gset reg) :=
    is_reg_writeP (λ reg acc _, reg ∉ regs).
  #[export] Instance is_illegal_reg_write_dec regs ev :
    Decision (is_illegal_reg_write regs ev).
  Proof. unfold_decide. Defined.

  Definition Illegal_RW := collect_all (λ _, is_illegal_reg_write regs_whitelist) cd.

  Definition fenced_acc_set fa :=
    match fa with
    | FA_read ⇒ R
    | FA_write ⇒ W
    | FA_readwrite ⇒ M
    end.

  Definition fence_base :=
    ⋃ (input ←@{list} enum fenced_accesses;
       output ←@{list} enum fenced_accesses;
       [⦗fenced_acc_set input⦘⨾po⨾⦗fences input output⦘⨾po⨾⦗fenced_acc_set output⦘]).

  Definition fence :=
    fence_base
    ∪ ⦗W⦘⨾po⨾⦗fences_tso⦘⨾po⨾⦗W⦘
    ∪ ⦗R⦘⨾po⨾⦗fences_tso⦘⨾po⨾⦗M⦘.

  Definition po_loc := po ∩ same_addr cd.
  Definition po_loc_no_w := po_loc ∖ (po_loc⨾⦗W⦘⨾po_loc).

  Definition ppo :=
    ⦗M⦘⨾po_loc⨾⦗W⦘
    ∪ (⦗R⦘⨾po_loc_no_w⨾⦗R⦘)∖rsw
    ∪ ⦗grel_rng rmw ∪ Wx⦘⨾rfi⨾⦗R⦘
    ∪ fence
    ∪ ⦗AQ⦘⨾po⨾⦗M⦘
    ∪ ⦗M⦘⨾po⨾⦗RL⦘
    ∪ ⦗RCsc⦘⨾po⨾⦗RCsc⦘
    ∪ rmw
    ∪ ⦗M⦘⨾addr⨾⦗M⦘
    ∪ ⦗M⦘⨾data⨾⦗W⦘
    ∪ ⦗M⦘⨾ctrl⨾⦗W⦘
    ∪ ⦗M⦘⨾(addr ∪ data)⨾⦗W⦘⨾rfi⨾⦗R⦘
    ∪ ⦗M⦘⨾addr⨾⦗M⦘⨾po⨾⦗W⦘ .

  Record consistent := {
      memory_coherence : grel_acyclic (co ∪ rf ∪ fr ∪ po_loc);
      register_coherence : reg_coherence cd;
      main_model : grel_acyclic (co ∪ rfe ∪ fr ∪ ppo);
      atomic : (rmw ∩ (fre⨾ coe)) = ∅;
    }.
  #[export] Instance consistent_dec : Decision consistent := ltac:(decide_record).

  Record not_UB := {
      initial_reads : IF ⊆ IR;
      initial_reads_not_delayed : IF ## grel_rng (coherence cd);
      register_write_permitted : Illegal_RW = ∅;
      memory_events_permitted : (mem_events cd) ⊆ M ∪ IF;
      is_nms' : is_nms cd;
    }.
  #[export] Instance not_UB_dec : Decision not_UB := ltac:(decide_record).

  Definition consistent_ok := consistent ∧ not_UB.
  #[export] Instance consistent_ok_dec : Decision consistent_ok := ltac:(unfold_decide).

End UMRiscV.

Require Import ASCommon.CResult.

Definition axmodel regs_whitelist : Ax.t Candidate.NMS ∅ :=
  λ _ cd, if decide (consistent cd) then
            if decide (not_UB regs_whitelist cd) then Ok Ax.Allowed
            else Error ""
          else Ok Ax.Rejected.

Definition archmodel regs_whitelist isem : archModel.nc ∅ :=
  Ax.to_archModel_nc isem (axmodel regs_whitelist).