### Install Rocq Dependencies and Build ArchSem

Source: https://context7.com/rems-project/archsem/llms.txt

Commands to set up Rocq opam repository, create a switch, install dependencies, build the project, run tests, and install ArchSem as an opam package.

```bash
# Add the Rocq opam repository
opam repo add rocq-released --set-default https://rocq-prover.org/opam/released

# Create a dedicated switch (recommended)
opam switch create --empty archsem-switch

# Install all locked dependencies
opam install . --deps-only --locked --with-test

# Build all Rocq and OCaml code
dune build

# Run all tests (sequential and promising model tests, OCaml unit tests)
dune runtests

# Install as an opam package (makes 5 top-level Rocq modules available)
opam pin .

# Build HTML documentation
dune build @doc
# Output: _build/default/Common/ASCommon.html/toc.html
#         _build/default/ArchSem/ArchSem.html/toc.html
#         _build/default/ArchSemArm/ArchSemArm.html/toc.html
```

--------------------------------

### Install Lock File Dependencies

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Install project dependencies as specified in the lock file. Includes tests by default. Add --with-dev-setup for development tools or --with-doc for documentation.

```bash
opam install . --deps-only --locked --with-test
```

--------------------------------

### Final Architectural State from Candidate (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

An example function to convert a candidate into its final architectural state.

```coq
Example final_state {et nmth} (cd : Candidate.t et nmth) : archState nmth :=
  Candidate.cd_to_archState cd.
```

--------------------------------

### Dependency Relations (Address/Data/Control) (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

An example function to extract address dependencies from a candidate.

```coq
Example address_dep {et nmth} (cd : Candidate.t et nmth) : grel EID.t :=
  Candidate.Deps.addr cd.
```

--------------------------------

### Example: Transporting Bitvector Across Size Equality

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates transporting a bitvector across a proof of equality between two size types (N).

```coq
(* Example: transporting a bitvector across a size equality *)
Example bv_transport (n m : N) (eq : n = m) (v : bv n) : bv m :=
  ctrans n m eq v.
```

--------------------------------

### Constructing an EID

Source: https://context7.com/rems-project/archsem/llms.txt

Example of constructing a specific EID for thread 0, instruction 3, ISA-event 1, with no byte split.

```coq
Example my_eid : EID.t := EID.make 0 3 1 None.
```

--------------------------------

### Looking up a Specific Instruction Trace

Source: https://context7.com/rems-project/archsem/llms.txt

Example function to look up a specific instruction trace within a pre-execution by providing the thread and instruction index.

```coq
Example instr_lookup
    {et nmth} (pe : Candidate.pre et nmth) : option (iTrace ()) :=
  Candidate.lookup_instruction pe 0 2.  (* thread 0, instruction 2 *)
```

--------------------------------

### Collect All Register Reads in Candidate (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

An example function to collect all register reads within a given candidate.

```coq
Example all_reg_reads {et nmth} (cd : Candidate.t et nmth) : gset EID.t :=
  Candidate.reg_reads cd.
```

--------------------------------

### Coq: Inspecting Memory Event Size

Source: https://context7.com/rems-project/archsem/llms.txt

Provides an example of how to inspect the size of a memory event using `get_size`. Returns `Some 8` for an 8-byte access, otherwise `None`.

```coq
Example inspect_mem_event (ev : iEvent) : option N :=
  get_size ev.
```

--------------------------------

### Full Well-formedness Check (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

An example function that checks the overall well-formedness of a candidate, returning a boolean result.

```coq
Example check_wf {et nmth} (cd : Candidate.t et nmth) : bool :=
  if decide (Candidate.wf cd) then true else false.
```

--------------------------------

### Coq: Generating Address Range

Source: https://context7.com/rems-project/archsem/llms.txt

Example of generating a list of addresses within a specified range using `addr_range`. Creates a list from `base` up to `base + 7` for a size of 8.

```coq
Example addr_range_example (base : address) : list address :=
  addr_range base 8.
```

--------------------------------

### Collect Memory Writes by Access Kind (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

An example function to collect exclusive memory writes within a given candidate.

```coq
Example all_exclusive_reads {et nmth} (cd : Candidate.t et nmth) : gset EID.t :=
  Candidate.exclusive_reads cd.
```

--------------------------------

### Coq: Outcome Effect Type Examples

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates the `outcome` effect type in Coq, including register reads/writes, memory operations, and handling results. Requires `ASCommon` and `Interface` imports.

```coq
From ASCommon Require Import FMon.
Require Import Interface.

Module Ex (A : Arch).
  Module I := Interface A.
  Import I.

  (* The outcome effect type is parameterized by its return type via [Effect] *)
  (* outcome_ret : Effect outcome *)
  (*   RegRead r _       → reg_type r          (the register value)       *)
  (*   MemRead mr        → result abort (bv * bv) (value + tag or abort)  *)
  (*   MemWrite _ _ _    → result abort ()      (success/exclusive/abort)  *)
  (*   GenericFail _     → ∅                   (no return — fatal)        *)
  (*   all others        → unit                                             *)

  (* An ISA instruction semantic is a value of type [iMon ()].
     [iMon] = [cMon outcome] = choice monad over outcome effects *)
  Example reg_read_then_write : iMon () :=
    val ← mcall (RegRead pc_reg default_racc);   (* read the PC *)
    mcall (RegWrite pc_reg default_racc val).     (* write it back *)

  (* Construct a MemReq for an 8-byte non-secure read *)
  Example make_mem_req (addr : address) : MemReq.t :=
    MemReq.make relaxed_read addr PAS_NonSecure 8 0.

  (* Issue a memory read effect and handle abort vs. success *)
  Example read_8_bytes (addr : address) : iMon (bv 64) :=
    let req := make_mem_req addr in
    result ← mcall (MemRead req);
    match result with
    | Ok (val, _tags) => mret val
    | Error _abort    => throw "physical memory abort"
    end.
End Ex.
```

--------------------------------

### Build Project with Dune

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Build all Rocq code and a fake OCaml library for smoke testing.

```bash
dune build
```

--------------------------------

### Coq Proof Tactic Formatting

Source: https://github.com/rems-project/archsem/blob/main/STYLE.md

Shows how to format composed tactics using 'all:' for better readability and step-through debugging in Coq.

```coq
  tactic1.
  all: tactic2.
  all: tactic3.
```

--------------------------------

### Run Project Tests

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Execute tests for sequential and promising models, as well as OCaml unit tests and CLI tests. Axiomatic models are not yet run.

```bash
dune runtests
```

--------------------------------

### Pin Project with Opam

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Pin the current project using opam. This makes the library available as top-level modules and adds the 'archsem' CLI tool to your PATH.

```bash
opam pin .
```

--------------------------------

### Apply Arm Axiomatic Model with UMArm

Source: https://context7.com/rems-project/archsem/llms.txt

Applies the Arm user-mode axiomatic model (UMArm) to a candidate execution. Demonstrates checking the acyclicity of the observed-by relation.

```coq
Require Import ArmInst.
Require Import GenAxiomaticArm.
Require Import UMArm.

Section UMArmExample.
  Import Candidate.
  Context {nmth : nat}.
  Context (cd : Candidate.t NMS nmth).

  (* Import standard Arm relation name aliases *)
  Import AxArmNames.

  (* Arm-standard relation aliases on this candidate *)
  Notation int  := (same_thread (pre_exec cd)).
  Notation addr := (Candidate.Deps.addr cd).
  Notation data := (Candidate.Deps.data cd).
  Notation ctrl := (Candidate.Deps.ctrl cd).
  Notation rf   := (reads_from cd).
  Notation co   := (coherence cd).

  (* The axiomatic model predicate *)
  (* UMArm.allowed : gset reg → Candidate.t NMS n → result string (behavior ∅) *)
  Definition model_result : result string (behavior ∅) :=
    UMArm.allowed ∅ cd.

  (* Check acyclicity of Arm's observed-by relation *)
  (* The model rejects a candidate if e.g. (obs ∪ hb) has a cycle *)
  Lemma wf_implies_consistent :
    wf cd → model_result = Ok Allowed →
    grel_irreflexive (UMArm.ob cd).
  Proof. (* ... follows from UMArm axioms ... *) Admitted.
End UMArmExample.
```

--------------------------------

### Create New Opam Switch

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Create a new, empty opam switch named 'archsem-switch'. This is recommended to avoid conflicts with existing packages.

```bash
opam switch create --empty archsem-switch
```

--------------------------------

### Use cdestruct Tactic for Hypothesis Simplification

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates the basic usage of the 'cdestruct' tactic for simplifying hypotheses and decomposing goals. It combines multiple simplification strategies into a single step. Requires 'CDestruct' module.

```coq
From ASCommon Require Import CDestruct.

(* Basic forms *)
(* [cdestruct h]          — simplify hypothesis h (and dependents)         *)
(* [cdestruct |- **]      — intro and simplify all antecedents of the goal *)
(* [cdestruct |- ***]     — same, also try to close/simplify the goal      *)
(* [cdestruct h,h2 |- **] — combine both                                   *)

Example use_cdestruct (P Q : Prop) (h : P ∧ Q) : Q ∧ P.
Proof.
  cdestruct h.        (* splits h into h1 : P and h2 : Q *)
  split; assumption.
Qed.
```

--------------------------------

### cdestruct with Goal Splitting and Simplification

Source: https://context7.com/rems-project/archsem/llms.txt

Illustrates 'cdestruct' with the '#CDestrSplitGoal' option to split disjunctive goals, followed by 'lia' for linear arithmetic. Requires 'CDestruct' module.

```coq
(* CDestrSplitGoal: also split disjunctive goals *)
Example split_goal (n : nat) (h : n = 0 ∨ n > 0) : n = 0 ∨ n ≥ 0.
Proof.
  cdestruct h |- *** #CDestrSplitGoal.
  all: lia.
Qed.
```

--------------------------------

### Coq Match Indentation

Source: https://github.com/rems-project/archsem/blob/main/STYLE.md

Demonstrates the required 4-space indentation for match bodies in Coq code.

```coq
match a with
| Constructor =>
    the_body
end
```

--------------------------------

### Add Rocq Opam Repository

Source: https://github.com/rems-project/archsem/blob/main/INSTALL.md

Add the Rocq opam repository to your opam configuration. This is necessary for some project dependencies.

```bash
opam repo add rocq-released --set-default https://rocq-prover.org/opam/released
```

--------------------------------

### GRel Inverse of Sequential Composition

Source: https://context7.com/rems-project/archsem/llms.txt

Proves the property for the inverse of sequential composition of relations using the 'set_solver' tactic. Requires 'GRel' module.

```coq
Lemma inv_seq (r s : grel nat) : (r ⨾ s)⁻¹ = s⁻¹ ⨾ r⁻¹.
Proof. set_solver. Qed.
```

--------------------------------

### cdestruct with Goal Decomposition and Simplification

Source: https://context7.com/rems-project/archsem/llms.txt

Shows 'cdestruct' simplifying a disjunctive hypothesis and applying simplification to the goal. The '- **' argument indicates simplification of antecedents and the goal. Requires 'CDestruct' module.

```coq
Example use_cdestruct2 (A : Type) (l : list A) (h : l = [] ∨ length l > 0) :
    length l = 0 ∨ length l > 0.
Proof.
  cdestruct h |- **.   (* destructs the disjunction and simplifies *)
  - left. by subst.
  - right. assumption.
Qed.
```

--------------------------------

### ISA Completeness Check

Source: https://context7.com/rems-project/archsem/llms.txt

Checks if all instructions in all traces within a pre-execution have completed successfully (ended with FTERet).

```coq
Definition ISA_complete pe : Prop :=
  ∀ thread ∈ vec_to_list pe.(events),
  ∀ instr  ∈ thread,
  instr.2 = FTERet ().
```

--------------------------------

### Run Single-Threaded Instruction Sequence Sequentially

Source: https://context7.com/rems-project/archsem/llms.txt

Provides an operational sequential interpreter for single-threaded execution using `SeqModel`. Manages architectural state and written addresses, running instructions one by one.

```coq
From ArchSem Require Import SeqModel.

Module MySeq := SequentialModel MyArch MyInterface MyTermModels MyNoCHERI.
Import MySeq.

(* seq_state: current architectural state + set of written addresses *)
Example initial_seq_state : seq_state :=
  {| sst     := initial_arch_state;
     written := ∅ |}.

(* Read a register from a sequential state *)
Example reg_read (r : reg) (st : seq_state) : option (reg_type r) :=
  read_reg_seq_state r st.

(* Run the sequential model on one instruction (iMon ()) *)
(* Returns a set of possible (result, state) pairs via [Exec.t] *)
Example run_one_instr (isem : iMon ()) (st : seq_state)
    : Exec.t seq_state string unit :=
  SeqModel.run_instruction None isem st.
```

--------------------------------

### ISA Conformance Check

Source: https://context7.com/rems-project/archsem/llms.txt

A predicate to check if every instruction trace in a pre-execution matches the provided ISA semantic.

```coq
Definition ISA_match pe (isem : iMon ()) : Prop :=
  ∀ tid : fin nmth,
  ∀ trc ∈ pe.(events) !!! tid,
  cmatch isem trc.
```

--------------------------------

### cdestruct with Match Expression Unfolding

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates using 'cdestruct' with the '#CDestrMatch' option to unfold match expressions during simplification. Requires 'CDestruct' module.

```coq
(* CDestrMatch: unfold match expressions during cdestruct *)
Example match_unfold (b : bool) (h : (if b then 1 else 0) = 1) : b = true.
Proof.
  cdestruct b, h |- ** #CDestrMatch.
  reflexivity.
Qed.
```

--------------------------------

### GRel Sequential Composition Associativity

Source: https://context7.com/rems-project/archsem/llms.txt

Proves the associative property of sequential composition for relations using the 'set_solver' tactic. Requires 'GRel' module.

```coq
(* set_solver works on grel goals *)
Lemma seq_assoc (r s t : grel nat) : (r ⨾ s) ⨾ t = r ⨾ (s ⨾ t).
Proof. set_solver. Qed.
```

--------------------------------

### Candidate Pre-execution Record Definition

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the 'pre' record which groups the initial architectural state with per-thread instruction traces. It includes type parameters for execution type and number of threads.

```coq
Record pre {et : exec_type} {nmth : nat} :=
  make_pre {
    init   : archState nmth;            (* initial register + memory state *)
    events : vec (list (iTrace ())) nmth (* per-thread instruction traces   *)
  }.
```

--------------------------------

### Run Arm Instructions with UMPromising in Rocq

Source: https://context7.com/rems-project/archsem/llms.txt

Sets up initial register and memory states, defines a termination condition, and executes Arm instructions using the UMPromising model. Verifies the result of a load operation.

```coq
From ArchSemArm Require Import ArmInst UMPromising.
Open Scope bv.

(* Set up initial register state for a single-thread test *)
Definition init_reg : registerMap :=
  ∅
  |> reg_insert _PC    0x500
  |> reg_insert R0     0x1000   (* base address *)
  |> reg_insert R1     0x0
  |> reg_insert SCTLR_EL1 0x0
  |> reg_insert PSTATE (init_pstate 0%bv 0%bv).  (* EL0, SP0 *)

(* Memory: instruction at 0x500, 8-byte datum at 0x1000 *)
Definition init_mem : memoryMap :=
  ∅
  |> mem_insert 0x500  4 0xf8606820  (* LDR X0, [X1, X0] *)
  |> mem_insert 0x1000 8 0x2a.       (* value = 42        *)

Definition termCond : terminationCondition 1 :=
  (λ _tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).

Definition initState :=
  {| archState.memory       := init_mem;
     archState.regs         := [# init_reg];
     archState.address_space := PAS_NonSecure |}.

(* Execute with fuel=2 using the sail-tiny-arm ISA semantic *)
Definition arm_sem := sail_tiny_arm_sem true.

Definition test_results :=
  UMPromising_exe arm_sem 2%nat 1%nat termCond initState.

(* Verify: R0 should contain 0x2a after the load *)
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x2a%Z].
  vm_compute (_ <$> _).
  reflexivity.
Qed.
```

--------------------------------

### Coq: Checking Address Overlap

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates checking if two memory regions overlap using `addr_overlap`. The lemma `overlap_sym` proves symmetry for address overlap checks.

```coq
Example check_overlap (a1 a2 : address) : Prop :=
  addr_overlap a1 8 a2 8.
(* True iff the 8-byte regions [a1,a1+8) and [a2,a2+8) share a byte *)

Lemma overlap_sym : ∀ a1 s1 a2 s2,
  addr_overlap a1 s1 a2 s2 → addr_overlap a2 s2 a1 s1.
Proof. unfold addr_overlap. tauto. Qed.
```

--------------------------------

### GRel Decidable Relational Properties

Source: https://context7.com/rems-project/archsem/llms.txt

Demonstrates checking decidable properties of relations like irreflexivity, transitivity, and symmetry using 'bool_decide' with 'GRel' types. Requires 'GRel' module.

```coq
(* Decidable properties *)
Example rel_props (r : grel nat) : bool :=
  bool_decide (grel_irreflexive r) &&
  bool_decide (grel_transitive r)  &&
  bool_decide (grel_symmetric r).
```

--------------------------------

### Lift Axiomatic Model to Non-Computational ArchModel (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Lifts an axiomatic model into a full non-computational architecture model by pairing it with an ISA semantic.

```coq
Definition Ax.to_archModel_nc
    (isem : iMon ()) (ax : Ax.t et flag) : archModel.nc flag :=
  λ n term initSt,
    {[ res | ∃ cd : Candidate.t et n,
               cd.(init) = initSt
             ∧ wf cd
             ∧ ISA_match cd isem
             ∧ Ax.Res.to_archModel (ax n cd) cd term = Some res ]}.
```

--------------------------------

### Well-formedness Instance for Candidate (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Declares a decidable instance for the well-formedness (wf) of a Candidate.t type.

```coq
Instance wf_dec {et nmth} (cd : Candidate.t et nmth) : Decision (wf cd).
```

--------------------------------

### iEvent Predicates for Filtering

Source: https://context7.com/rems-project/archsem/llms.txt

These computable predicates can be used for filtering iEvents. They return a Prop and can be used in decidable contexts.

```coq
Example event_predicates (ev : iEvent) : Prop :=
  is_reg_read ev ∧            (* any register read                          *)
  is_mem_read ev ∧            (* successful (non-aborted) memory read       *)
  is_mem_write ev ∧           (* successful memory write                    *)
  is_mem_write_addr_announce ev ∧
  is_barrier ev ∧
  is_cacheop ev ∧
  is_tlbop ev.
```

--------------------------------

### Define Custom Effect Type and Program in Free Monad

Source: https://context7.com/rems-project/archsem/llms.txt

Defines a custom effect type 'my_eff' with GetState and PutState constructors and demonstrates creating a program 'increment' within a free monad over this effect. Requires 'FMon' and 'Effects' modules.

```coq
From ASCommon Require Import FMon Effects.

(* Define a custom effect type *)
Inductive my_eff : eff := 
| GetState : my_eff
| PutState (n : nat) : my_eff.

Instance my_eff_ret : Effect my_eff :=
  λ e, match e with
       | GetState   => nat
       | PutState _ => unit
       end.

(* A program in the free monad over my_eff *)
Definition increment : fMon my_eff unit :=
  n ← mcall GetState;
  mcall (PutState (n + 1)).

(* Trace (fTrace): a list of fEvents paired with a termination marker *)
(* An fEvent is: call &→ return_value, e.g. [GetState &→ 5 ; PutState 6 &→ ()] *)

(* cmatch: check that a trace is compatible with a cMon program *)
Example trace_check (prog : iMon ()) (tr : iTrace ()) : Prop :=
  cmatch prog tr.
```

--------------------------------

### Looking up an Event by EID

Source: https://context7.com/rems-project/archsem/llms.txt

This function allows looking up a specific iEvent within a pre-execution using its EID. It returns Some ev if the EID is valid, otherwise None.

```coq
Example lookup_event
    {et nmth} (pe : Candidate.pre et nmth) (eid : EID.t) : option iEvent :=
  pe !! eid.    (* returns Some ev if eid is valid, else None *)
```

--------------------------------

### Define CTransSimpl Class for Trivial Transport

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the CTransSimpl class, ensuring that the transport is definitionally trivial when the equality proof is reflexivity. This is crucial for vm_compute.

```coq
(* CTransSimpl: the transport is definitionally trivial when eq is refl *)
(* This is essential so vm_compute does not get stuck on transports      *)
Class CTransSimpl {T} (F : T → Type) `{CTrans T F} :=
  ctrans_simpl : ∀ x (a : F x), ctrans x x eq_refl a = a.
```

--------------------------------

### GRel Relational Algebra Operations

Source: https://context7.com/rems-project/archsem/llms.txt

Shows basic relational algebra operations on 'grel nat' types, including union, intersection, sequential composition, inverse, transitive closure, and diagonal. Requires 'GRel' module.

```coq
From ASCommon Require Import GRel.

(* grel A = gset (A * A) — all stdpp set operations apply *)
Example rel_ops (r s : grel nat) :=
  let _union  : grel nat := r ∪ s           in  (* relational union      *)
  let _inter  : grel nat := r ∩ s           in  (* relational intersection *)
  let _seq    : grel nat := r ⨾ s           in  (* sequential composition *)
  let _inv    : grel nat := r⁻¹             in  (* inverse               *)
  let _tc     : grel nat := r⁺              in  (* transitive closure     *)
  let _diag   : grel nat := ⦗{[1;2;3]}⦘    in  (* diagonal of a set     *)
  tt.
```

--------------------------------

### Define Candidate Type with Relations (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the Candidate record type, extending pre-execution with four relational components: reads-from (rf), register reads-from (rrf), coherence order (co), and load-reserve/store-conditional pairing (lxsx).

```coq
Record t {et : exec_type} {nmth : nat} :=
  make {
    pre_exec      : pre et nmth;
    reads_from    : grel EID.t;   (* write → read, mem rf   *)
    reg_reads_from: grel EID.t;   (* reg write → reg read   *)
    coherence     : grel EID.t;   (* write coherence order  *)
    lxsx          : grel EID.t;   (* LR/SC exclusive pairs  *)
  }.
```

--------------------------------

### Rocq Module Signature for Architecture Parameters

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the `Arch` module type signature, specifying required parameters for register types, memory access kinds, and other architecture-specific details needed by the `Interface` module.

```coq
Module Type Arch.
  (* Register enumeration *)
  Parameter reg : Type.
  Parameter reg_eq : EqDecision reg.
  Parameter reg_countable : @Countable reg reg_eq.
  Parameter pretty_reg : Pretty reg.
  Parameter reg_of_string : string → option reg.

  (* Dependent register value type *)
  Parameter reg_type : reg → Type.
  Parameter reg_type_eq : ∀ r : reg, EqDecision (reg_type r).
  Parameter ctrans_reg_type : CTrans reg_type. (* Computable transport *)

  (* Program counter *)
  Parameter pc_reg : reg.

  (* Physical address size in bits *)
  Parameter addr_size : N.
  Parameter addr_space : Type.

  (* Memory access kind — carries relaxed/acquire/release/exclusive flags *)
  Parameter mem_acc : Type.
  Parameter is_relaxed    : mem_acc → bool.
  Parameter is_rel_acq_rcsc : mem_acc → bool.
  Parameter is_exclusive  : mem_acc → bool.
  Parameter is_ifetch     : mem_acc → bool.
  Parameter is_ttw        : mem_acc → bool.

  (* Barrier, cache, TLB, exception, and translation types *)
  Parameter barrier  : Type.
  Parameter cache_op : Type.
  Parameter tlbi     : Type.
  Parameter exn      : Type.
  Parameter trans_start : Type.
  Parameter trans_end   : Type.
  Parameter abort    : Type.

  Parameter CHERI : bool.
  Parameter cap_size_log : N.
End Arch.
```

--------------------------------

### Reads-From Well-formedness Record (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the well-formedness conditions for the reads-from relation, ensuring it's a functional relation from memory writes to memory reads and adheres to validity constraints.

```coq
Record reads_from_wf {cd} :=
  {
    rf_from_writes  : grel_dom (reads_from cd) ⊆ mem_writes cd;
    rf_to_reads     : grel_rng (reads_from cd) ⊆ mem_reads cd;
    rf_functional   : grel_functional (reads_from cd)⁻¹;
    rf_valid        : ∀'(w,r) ∈ reads_from cd, is_valid_rf cd w r;
    rf_valid_initial: ∀ r ∈ init_mem_reads cd, is_valid_init_mem_read cd r }.
```

--------------------------------

### Parameterized iEvent Predicates

Source: https://context7.com/rems-project/archsem/llms.txt

Use parameterized predicates for fine-grained filtering of iEvents based on specific conditions.

```coq
Example only_pc_reads (ev : iEvent) : Prop :=
  is_reg_readP (λ reg _ _, reg = pc_reg) ev.
```

```coq
Example relaxed_writes_only (ev : iEvent) : Prop :=
  is_mem_write_kindP is_relaxed ev.
```

--------------------------------

### Monotonicity Theorem for Wider Models (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

States that if one axiomatic model is wider than another, the corresponding architecture models derived from them will also maintain this wider relationship.

```coq
Lemma Ax.wider_Model (isem : iMon ()) (ax ax' : Ax.t et flag) :
  Ax.wider ax ax' →
  archModel.wider (Ax.to_archModel_nc isem ax) (Ax.to_archModel_nc isem ax').
```

--------------------------------

### LXSX Well-formedness Record (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the well-formedness conditions for the lxsx (load-reserve/store-conditional) relation, ensuring it operates on exclusive accesses and respects instruction order and address.

```coq
Record lxsx_wf {cd} :=
  {
    lxsx_from_reads      : grel_dom (lxsx cd) ⊆ exclusive_reads cd;
    lxsx_to_writes       : grel_rng (lxsx cd) ⊆ exclusive_writes cd;
    lxsx_instruction_order : lxsx cd ⊆ instruction_order cd;
    lxsx_same_pa         : lxsx cd ⊆ same_addr cd }.
```

--------------------------------

### Accessing iEvent Fields with Accessor Functions

Source: https://context7.com/rems-project/archsem/llms.txt

Use these accessor functions to query fields of an iEvent without direct constructor matching. They return an option type, indicating presence or absence of the field.

```coq
Example event_accessors (ev : iEvent) : unit :=
  let _reg      : option reg      := get_reg ev        in  (* Some r  or None *)
  let _reg_val  : option (sigT reg_type) := get_reg_val ev in
  let _mem_req  : option MemReq.t := get_mem_req ev    in
  let _addr     : option address  := get_addr ev       in
  let _size     : option N        := get_size ev       in
  let _val      : option bvn      := get_mem_value ev  in  (* dynamic bv      *)
  let _barrier  : option barrier  := get_barrier ev    in
  let _cacheop  : option cache_op := get_cacheop ev    in
  let _tlbi     : option tlbi     := get_tlbi ev       in
  tt.
```

--------------------------------

### ISA Failure Check

Source: https://context7.com/rems-project/archsem/llms.txt

Checks if at least one instruction in any trace within a pre-execution has resulted in a generic failure (FTEOpenCall GenericFail).

```coq
Definition ISA_failed pe : Prop :=
  ∃ thread ∈ vec_to_list pe.(events),
  ∃ instr  ∈ thread,
  ∃ msg, instr.2 = FTEOpenCall (GenericFail msg).
```

--------------------------------

### Define Behavior Type (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the 'behavior' inductive type, which can be 'Allowed', 'Rejected', or 'Flagged' with a specific flag.

```coq
Inductive behavior {flag} :=
| Allowed
| Rejected
| Flagged (f : flag).
```

--------------------------------

### Coq: MemReq Record Definition

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the `MemReq.t` record for memory access requests, including access kind, address, space, size, and tag count. This record is used as a payload for memory outcomes.

```coq
Module MemReq.
  Record t :=
    make
      { access_kind   : mem_acc;   (* e.g. relaxed, acquire, exclusive … *)
        address       : address;   (* bv addr_size                       *)
        address_space : addr_space;
        size          : N;         (* byte count, e.g. 8 for 64-bit      *)
        num_tag       : N;         (* MTE tag count, 0 for untagged       *)
      }.
End MemReq.
```

--------------------------------

### Implicit CTrans Usage in ISA Models

Source: https://context7.com/rems-project/archsem/llms.txt

Notes that ISA models implicitly use ctrans when register types must be transported across register name equality proofs, handled by the EffCTrans instance on [outcome].

```coq
(* In practice, ISA models use ctrans implicitly when the RegRead return
   type [reg_type r] must be transported across a proof that two register
   names are equal. The EffCTrans instance on [outcome] handles this. *)
```

--------------------------------

### Coherence Well-formedness Record (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the well-formedness conditions for the coherence relation, requiring transitivity, irreflexivity, and that overlapping writes are ordered.

```coq
Record coherence_wf {cd} :=
  {
    co_transitive   : grel_transitive (coherence cd);
    co_irreflexive  : grel_irreflexive (coherence cd);
    co_contains_overlapping_writes :
      ∀ w1 w2 ∈ mem_writes cd,
        is_overlapping cd w1 w2 →
        (w1,w2) ∈ coherence cd ∨ (w2,w1) ∈ coherence cd }.
```

--------------------------------

### Define Axiomatic Model Type (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the type for an axiomatic model (Ax.t), which is a function mapping a candidate to a behavior result.

```coq
Definition Ax.t et flag := ∀ n, Candidate.t et n → result string (behavior flag).
```

--------------------------------

### Define Model Comparison (Wider) (Coq)

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the 'wider' relation between two axiomatic models, indicating that the second model is at least as permissive as the first.

```coq
Definition Ax.wider (ax ax' : Ax.t et flag) :=
  ∀ n cd, Ax.Res.wider (ax n cd) (ax' n cd).
```

--------------------------------

### EID.t Record Definition

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the Event ID (EID) structure for uniquely identifying events within a candidate execution, including thread, instruction, and event indices.

```coq
Module EID.
  Record t :=
    make {
      tid  : nat;        (* thread index, zero-based       *)
      iid  : nat;        (* instruction index in thread    *)
      ieid : nat;        (* event index within instruction *)
      byte : option N    (* byte split index (MS mode)     *)
    }.
  (* Program-order comparison *)
  Definition po_lt (id1 id2 : t) : Prop :=
    id1.(tid) = id2.(tid) ∧ id1.(iid) < id2.(iid).
  Notation "x <ₚ y" := (po_lt x y).

  (* Intra-instruction order *)
  Definition iio_lt (id1 id2 : t) : Prop :=
    id1.(tid) = id2.(tid) ∧ id1.(iid) = id2.(iid) ∧ id1.(ieid) < id2.(ieid).
  Notation "x <ᵢ y" := (iio_lt x y).
End EID.
```

--------------------------------

### Define Computable Transport Class (CTrans)

Source: https://github.com/rems-project/archsem/blob/main/Common/README.md

Defines the CTrans typeclass for providing computable transport on indexed type families, based on equalities on an index. This is used when general transport functions are not feasible.

```Coq
Class CTrans {T : Type} (F : T → Type) :=
  ctrans : ∀ (x y : T) (eq : x = y) (a : F x), F y.
```

--------------------------------

### Define CTrans Typeclass for Computable Transport

Source: https://context7.com/rems-project/archsem/llms.txt

Defines the CTrans typeclass for type-based computable transport of indexed type families across type equalities, ensuring executability.

```coq
From ASCommon Require Import Common.

(* The CTrans class *)
Class CTrans {T : Type} (F : T → Type) :=
  ctrans : ∀ (x y : T) (eq : x = y) (a : F x), F y.
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.