| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1076 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (109 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (76 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (281 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (455 entries) |
Global Index
A
A [abbreviation, in ArchSemArm.VMUMEquivThm]A [abbreviation, in ArchSemArm.VMSA22Arm]
A [abbreviation, in ArchSemArm.UMArm]
A [abbreviation, in ArchSemArm.UMSeqArm]
addr [abbreviation, in ArchSemArm.VMUMEquivThm]
addr [abbreviation, in ArchSemArm.VMSA22Arm]
addr [abbreviation, in ArchSemArm.UMArm]
addr [abbreviation, in ArchSemArm.UMSeqArm]
allow_write [definition, in ArchSemArm.VMPromising]
amo [abbreviation, in ArchSemArm.VMUMEquivThm]
amo [abbreviation, in ArchSemArm.VMSA22Arm]
amo [abbreviation, in ArchSemArm.UMArm]
amo [abbreviation, in ArchSemArm.UMSeqArm]
aob [definition, in ArchSemArm.VMSA22Arm]
aob [definition, in ArchSemArm.UMArm]
Arch [module, in ArchSemArm.ArmInst]
ArchExtra [module, in ArchSemArm.ArmInst]
ArchExtra.pc_reg [definition, in ArchSemArm.ArmInst]
ArchExtra.reg_type_to_gen [definition, in ArchSemArm.ArmInst]
ArchExtra.reg_type_of_gen [definition, in ArchSemArm.ArmInst]
ArchExtra.reg_of_string [definition, in ArchSemArm.ArmInst]
archmodel [definition, in ArchSemArm.VMSA22Arm]
archmodel [definition, in ArchSemArm.UMArm]
archmodel [definition, in ArchSemArm.UMSeqArm]
Arm [module, in ArchSemArm.ArmInst]
ArmInst [library]
asid_ttbr [definition, in ArchSemArm.VMPromising]
asid_ttbr_of_root_ttbr [definition, in ArchSemArm.VMPromising]
atomic [projection, in ArchSemArm.VMSA22Arm]
atomic [projection, in ArchSemArm.UMArm]
atomic [projection, in ArchSemArm.UMSeqArm]
attr_idx [definition, in ArchSemArm.VMPromising]
AxArmNames [module, in ArchSemArm.GenAxiomaticArm]
AxArmNames.A [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.amo [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ArmNames [section, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ArmNames.cd [variable, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ArmNames.et [variable, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ArmNames.nmth [variable, in ArchSemArm.GenAxiomaticArm]
AxArmNames.C [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.co [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.coe [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.coi [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.coi_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ERET [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.Exp [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.exp_internal_dec [instance, in ArchSemArm.GenAxiomaticArm]
AxArmNames.exp_internal [record, in ArchSemArm.GenAxiomaticArm]
AxArmNames.F [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.fr [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.fre [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.frf [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.frfi [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.frfi_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.fri [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.fri_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.full_instruction_order [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ICDC [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.IF [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifr [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifre [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifri [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.iio [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.instruction_order [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.int [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.IR [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.irf [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.irfe [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.irfi [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.ISB [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_translation_read_fault_dec [instance, in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_translation_read_fault [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_mrs [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_msr [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.L [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.lxsx [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.M [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.MRS [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.MSR [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.pe [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.po [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.Q [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.R [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.RE [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.reg_internal_dec [instance, in ArchSemArm.GenAxiomaticArm]
AxArmNames.reg_internal [record, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rf [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfe [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfi [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfi_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfr [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfr_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rmw [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.RR [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rrf [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.rrf_internal [projection, in ArchSemArm.GenAxiomaticArm]
AxArmNames.RW [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.Rx [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.sca [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.si [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.T [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.TE [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfr [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfre [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfri [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.TLBI [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.trf [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.trfe [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.trfi [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.T_f_in_T [lemma, in ArchSemArm.GenAxiomaticArm]
AxArmNames.T_f [definition, in ArchSemArm.GenAxiomaticArm]
AxArmNames.W [abbreviation, in ArchSemArm.GenAxiomaticArm]
AxArmNames.Wx [abbreviation, in ArchSemArm.GenAxiomaticArm]
axmodel [definition, in ArchSemArm.VMSA22Arm]
axmodel [definition, in ArchSemArm.UMArm]
axmodel [definition, in ArchSemArm.UMSeqArm]
B
Barriers [section, in ArchSemArm.GenAxiomaticArm]Barriers.et [variable, in ArchSemArm.GenAxiomaticArm]
Barriers.nmth [variable, in ArchSemArm.GenAxiomaticArm]
BBM [module, in ArchSemArm.VMPromising]
BBM [section, in ArchSemArm.VMPromising]
BBM.check [definition, in ArchSemArm.VMPromising]
BBM.initmem [variable, in ArchSemArm.VMPromising]
BBM.Lax [constructor, in ArchSemArm.VMPromising]
BBM.Off [constructor, in ArchSemArm.VMPromising]
BBM.param [inductive, in ArchSemArm.VMPromising]
BBM.param_sind [definition, in ArchSemArm.VMPromising]
BBM.param_rec [definition, in ArchSemArm.VMPromising]
BBM.param_ind [definition, in ArchSemArm.VMPromising]
BBM.param_rect [definition, in ArchSemArm.VMPromising]
BBM.Strict [constructor, in ArchSemArm.VMPromising]
bob [definition, in ArchSemArm.VMSA22Arm]
bob [definition, in ArchSemArm.UMArm]
C
C [abbreviation, in ArchSemArm.VMUMEquivThm]C [abbreviation, in ArchSemArm.VMSA22Arm]
C [abbreviation, in ArchSemArm.UMArm]
C [abbreviation, in ArchSemArm.UMSeqArm]
check_bbm_violation [definition, in ArchSemArm.VMPromising]
child_lvl_add_one [lemma, in ArchSemArm.VMPromising]
child_lvl [definition, in ArchSemArm.VMPromising]
co [abbreviation, in ArchSemArm.VMUMEquivThm]
co [abbreviation, in ArchSemArm.VMSA22Arm]
co [abbreviation, in ArchSemArm.UMArm]
co [abbreviation, in ArchSemArm.UMSeqArm]
coe [abbreviation, in ArchSemArm.VMUMEquivThm]
coe [abbreviation, in ArchSemArm.VMSA22Arm]
coe [abbreviation, in ArchSemArm.UMArm]
coe [abbreviation, in ArchSemArm.UMSeqArm]
coi [abbreviation, in ArchSemArm.VMUMEquivThm]
coi [abbreviation, in ArchSemArm.VMSA22Arm]
coi [abbreviation, in ArchSemArm.UMArm]
coi [abbreviation, in ArchSemArm.UMSeqArm]
consistent [record, in ArchSemArm.VMSA22Arm]
consistent [record, in ArchSemArm.UMArm]
consistent [record, in ArchSemArm.UMSeqArm]
consistent_ok_dec [instance, in ArchSemArm.VMSA22Arm]
consistent_ok [definition, in ArchSemArm.VMSA22Arm]
consistent_dec [instance, in ArchSemArm.VMSA22Arm]
consistent_ok_dec [instance, in ArchSemArm.UMArm]
consistent_ok [definition, in ArchSemArm.UMArm]
consistent_dec [instance, in ArchSemArm.UMArm]
consistent_ok_dec [instance, in ArchSemArm.UMSeqArm]
consistent_ok [definition, in ArchSemArm.UMSeqArm]
consistent_dec [instance, in ArchSemArm.UMSeqArm]
ContextChange [definition, in ArchSemArm.VMSA22Arm]
ContextChange_obv_false [instance, in ArchSemArm.VMUMEquivThm]
co_contains_TBLI_writes [projection, in ArchSemArm.VMSA22Arm]
CSE [definition, in ArchSemArm.VMSA22Arm]
ctrl [abbreviation, in ArchSemArm.VMUMEquivThm]
ctrl [abbreviation, in ArchSemArm.VMSA22Arm]
ctrl [abbreviation, in ArchSemArm.UMArm]
ctrl [abbreviation, in ArchSemArm.UMSeqArm]
ctxob [definition, in ArchSemArm.VMSA22Arm]
C_obv_false [instance, in ArchSemArm.VMUMEquivThm]
D
data [abbreviation, in ArchSemArm.VMUMEquivThm]data [abbreviation, in ArchSemArm.VMSA22Arm]
data [abbreviation, in ArchSemArm.UMArm]
data [abbreviation, in ArchSemArm.UMSeqArm]
Decision_has_bbm_violation [instance, in ArchSemArm.VMPromising]
Decision_mem_contents_eq [instance, in ArchSemArm.VMPromising]
Decision_is_addr_from_oa [instance, in ArchSemArm.VMPromising]
Decision_allow_write [instance, in ArchSemArm.VMPromising]
Decision_is_global [instance, in ArchSemArm.VMPromising]
Decision_is_tlb_fillable [instance, in ArchSemArm.VMPromising]
Decision_is_accessible_final [instance, in ArchSemArm.VMPromising]
Decision_has_access_flag [instance, in ArchSemArm.VMPromising]
Decision_is_final [instance, in ArchSemArm.VMPromising]
Decision_is_block [instance, in ArchSemArm.VMPromising]
Decision_is_table [instance, in ArchSemArm.VMPromising]
Decision_is_valid [instance, in ArchSemArm.VMPromising]
Decision_match_prefix_at [instance, in ArchSemArm.VMPromising]
Decision_va_in_range [instance, in ArchSemArm.VMPromising]
Decision_is_reg_unknown [instance, in ArchSemArm.VMPromising]
dmb [definition, in ArchSemArm.GenAxiomaticArm]
dmbld [definition, in ArchSemArm.GenAxiomaticArm]
dmbnsh [definition, in ArchSemArm.GenAxiomaticArm]
dmbnshld [definition, in ArchSemArm.GenAxiomaticArm]
dmbnshst [definition, in ArchSemArm.GenAxiomaticArm]
dmbnshsy [definition, in ArchSemArm.GenAxiomaticArm]
dmbst [definition, in ArchSemArm.GenAxiomaticArm]
dmbsy [definition, in ArchSemArm.GenAxiomaticArm]
dmb_store [definition, in ArchSemArm.GenAxiomaticArm]
dmb_load [definition, in ArchSemArm.GenAxiomaticArm]
dmb_full [definition, in ArchSemArm.GenAxiomaticArm]
dob [definition, in ArchSemArm.VMSA22Arm]
dob [definition, in ArchSemArm.UMArm]
dsb [definition, in ArchSemArm.GenAxiomaticArm]
dsbld [definition, in ArchSemArm.GenAxiomaticArm]
dsbnsh [definition, in ArchSemArm.GenAxiomaticArm]
dsbnshld [definition, in ArchSemArm.GenAxiomaticArm]
dsbnshst [definition, in ArchSemArm.GenAxiomaticArm]
dsbnshsy [definition, in ArchSemArm.GenAxiomaticArm]
dsbst [definition, in ArchSemArm.GenAxiomaticArm]
dsbsy [definition, in ArchSemArm.GenAxiomaticArm]
dsb_store [definition, in ArchSemArm.GenAxiomaticArm]
dsb_load [definition, in ArchSemArm.GenAxiomaticArm]
dsb_full [definition, in ArchSemArm.GenAxiomaticArm]
E
EL [definition, in ArchSemArm.VMPromising]ELp [definition, in ArchSemArm.VMPromising]
ELp_to_EL [definition, in ArchSemArm.VMPromising]
emit_promise' [definition, in ArchSemArm.VMPromising]
ERET [abbreviation, in ArchSemArm.VMUMEquivThm]
ERET [abbreviation, in ArchSemArm.VMSA22Arm]
ERET [abbreviation, in ArchSemArm.UMArm]
ERET [abbreviation, in ArchSemArm.UMSeqArm]
ERET_obv_false [instance, in ArchSemArm.VMUMEquivThm]
ets2 [definition, in ArchSemArm.VMPromising]
ets3 [definition, in ArchSemArm.VMPromising]
Ev [module, in ArchSemArm.VMPromising]
Ev.addr_overlap [definition, in ArchSemArm.VMPromising]
Ev.dec [instance, in ArchSemArm.VMPromising]
Ev.Decision_addr_overlap [instance, in ArchSemArm.VMPromising]
Ev.get_tlbi_recipient [definition, in ArchSemArm.VMPromising]
Ev.get_tlbi [definition, in ArchSemArm.VMPromising]
Ev.get_msg [definition, in ArchSemArm.VMPromising]
Ev.Msg [constructor, in ArchSemArm.VMPromising]
Ev.t [inductive, in ArchSemArm.VMPromising]
Ev.tid [definition, in ArchSemArm.VMPromising]
Ev.Tlbi [constructor, in ArchSemArm.VMPromising]
Ev.t_sind [definition, in ArchSemArm.VMPromising]
Ev.t_rec [definition, in ArchSemArm.VMPromising]
Ev.t_ind [definition, in ArchSemArm.VMPromising]
Ev.t_rect [definition, in ArchSemArm.VMPromising]
Exp [abbreviation, in ArchSemArm.VMUMEquivThm]
Exp [abbreviation, in ArchSemArm.VMSA22Arm]
Exp [abbreviation, in ArchSemArm.UMArm]
Exp [abbreviation, in ArchSemArm.UMSeqArm]
external [projection, in ArchSemArm.VMSA22Arm]
external [projection, in ArchSemArm.UMArm]
F
F [abbreviation, in ArchSemArm.VMUMEquivThm]F [abbreviation, in ArchSemArm.VMSA22Arm]
F [abbreviation, in ArchSemArm.UMArm]
F [abbreviation, in ArchSemArm.UMSeqArm]
Fault [definition, in ArchSemArm.VMSA22Arm]
FaultFromAquireR [definition, in ArchSemArm.VMSA22Arm]
FaultFromR [definition, in ArchSemArm.VMSA22Arm]
FaultFromReleaseW [definition, in ArchSemArm.VMSA22Arm]
FaultFromW [definition, in ArchSemArm.VMSA22Arm]
Fault_P [definition, in ArchSemArm.VMSA22Arm]
Fault_T [definition, in ArchSemArm.VMSA22Arm]
filter_tlbi_promises [definition, in ArchSemArm.VMPromising]
find_latest_snapshot_before [definition, in ArchSemArm.VMPromising]
fr [abbreviation, in ArchSemArm.VMUMEquivThm]
fr [abbreviation, in ArchSemArm.VMSA22Arm]
fr [abbreviation, in ArchSemArm.UMArm]
fr [abbreviation, in ArchSemArm.UMSeqArm]
fre [abbreviation, in ArchSemArm.VMUMEquivThm]
fre [abbreviation, in ArchSemArm.VMSA22Arm]
fre [abbreviation, in ArchSemArm.UMArm]
fre [abbreviation, in ArchSemArm.UMSeqArm]
frf [abbreviation, in ArchSemArm.VMUMEquivThm]
frf [abbreviation, in ArchSemArm.VMSA22Arm]
frf [abbreviation, in ArchSemArm.UMArm]
frf [abbreviation, in ArchSemArm.UMSeqArm]
frfi [abbreviation, in ArchSemArm.VMUMEquivThm]
frfi [abbreviation, in ArchSemArm.VMSA22Arm]
frfi [abbreviation, in ArchSemArm.UMArm]
frfi [abbreviation, in ArchSemArm.UMSeqArm]
fri [abbreviation, in ArchSemArm.VMUMEquivThm]
fri [abbreviation, in ArchSemArm.VMSA22Arm]
fri [abbreviation, in ArchSemArm.UMArm]
fri [abbreviation, in ArchSemArm.UMSeqArm]
full_instruction_order [abbreviation, in ArchSemArm.VMUMEquivThm]
full_instruction_order [abbreviation, in ArchSemArm.VMSA22Arm]
full_instruction_order [abbreviation, in ArchSemArm.UMArm]
full_instruction_order [abbreviation, in ArchSemArm.UMSeqArm]
FwdItem [module, in ArchSemArm.VMPromising]
FwdItem [module, in ArchSemArm.UMPromising]
FwdItem.init [definition, in ArchSemArm.UMPromising]
FwdItem.read_fwd_view [definition, in ArchSemArm.UMPromising]
FwdItem.t [record, in ArchSemArm.UMPromising]
FwdItem.time [projection, in ArchSemArm.UMPromising]
FwdItem.view [projection, in ArchSemArm.UMPromising]
FwdItem.xcl_view [projection, in ArchSemArm.UMPromising]
G
GenAxiomaticArm [library]get_ipa_page [definition, in ArchSemArm.VMSA22Arm]
get_va_page [definition, in ArchSemArm.VMSA22Arm]
get_TLBI_addr_kind [definition, in ArchSemArm.VMSA22Arm]
get_asid [definition, in ArchSemArm.VMSA22Arm]
get_vmid [definition, in ArchSemArm.VMSA22Arm]
get_translation_start [definition, in ArchSemArm.VMSA22Arm]
H
has_bbm_violation [definition, in ArchSemArm.VMPromising]has_access_flag [definition, in ArchSemArm.VMPromising]
has_tlbi_shareability [definition, in ArchSemArm.VMSA22Arm]
has_tlbi_regime [definition, in ArchSemArm.VMSA22Arm]
has_tlbi_op [definition, in ArchSemArm.VMSA22Arm]
higher_level [definition, in ArchSemArm.VMPromising]
I
ICDC [abbreviation, in ArchSemArm.VMUMEquivThm]ICDC [abbreviation, in ArchSemArm.VMSA22Arm]
ICDC [abbreviation, in ArchSemArm.UMArm]
ICDC [abbreviation, in ArchSemArm.UMSeqArm]
IF [abbreviation, in ArchSemArm.VMUMEquivThm]
IF [abbreviation, in ArchSemArm.VMSA22Arm]
IF [abbreviation, in ArchSemArm.UMArm]
IF [abbreviation, in ArchSemArm.UMSeqArm]
ifr [abbreviation, in ArchSemArm.VMUMEquivThm]
ifr [abbreviation, in ArchSemArm.VMSA22Arm]
ifr [abbreviation, in ArchSemArm.UMArm]
ifr [abbreviation, in ArchSemArm.UMSeqArm]
ifre [abbreviation, in ArchSemArm.VMUMEquivThm]
ifre [abbreviation, in ArchSemArm.VMSA22Arm]
ifre [abbreviation, in ArchSemArm.UMArm]
ifre [abbreviation, in ArchSemArm.UMSeqArm]
ifri [abbreviation, in ArchSemArm.VMUMEquivThm]
ifri [abbreviation, in ArchSemArm.VMSA22Arm]
ifri [abbreviation, in ArchSemArm.UMArm]
ifri [abbreviation, in ArchSemArm.UMSeqArm]
iio [abbreviation, in ArchSemArm.VMUMEquivThm]
iio [abbreviation, in ArchSemArm.VMSA22Arm]
iio [abbreviation, in ArchSemArm.UMArm]
iio [abbreviation, in ArchSemArm.UMSeqArm]
IIS [module, in ArchSemArm.VMPromising]
IIS [module, in ArchSemArm.UMPromising]
IIS.add [definition, in ArchSemArm.VMPromising]
IIS.add [definition, in ArchSemArm.UMPromising]
IIS.eta [instance, in ArchSemArm.UMPromising]
IIS.init [definition, in ArchSemArm.VMPromising]
IIS.init [definition, in ArchSemArm.UMPromising]
IIS.inv_time [projection, in ArchSemArm.VMPromising]
IIS.rmw_read [projection, in ArchSemArm.VMPromising]
IIS.rmw_read [projection, in ArchSemArm.UMPromising]
IIS.set_inv_time [definition, in ArchSemArm.VMPromising]
IIS.set_trs [definition, in ArchSemArm.VMPromising]
IIS.strict [projection, in ArchSemArm.VMPromising]
IIS.strict [projection, in ArchSemArm.UMPromising]
IIS.t [record, in ArchSemArm.VMPromising]
IIS.t [record, in ArchSemArm.UMPromising]
IIS.TransRes [module, in ArchSemArm.VMPromising]
IIS.TransRes.pop [definition, in ArchSemArm.VMPromising]
IIS.TransRes.remaining [projection, in ArchSemArm.VMPromising]
IIS.TransRes.root [projection, in ArchSemArm.VMPromising]
IIS.TransRes.t [record, in ArchSemArm.VMPromising]
IIS.TransRes.trans_end [projection, in ArchSemArm.VMPromising]
IIS.TransRes.trans_start [projection, in ArchSemArm.VMPromising]
IIS.TransRes.va [projection, in ArchSemArm.VMPromising]
IIS.trs [projection, in ArchSemArm.VMPromising]
Illegal_RW [definition, in ArchSemArm.VMSA22Arm]
Illegal_RW [definition, in ArchSemArm.UMArm]
Illegal_RR [definition, in ArchSemArm.UMSeqArm]
Illegal_RW [definition, in ArchSemArm.UMSeqArm]
IMonFromSail [module, in ArchSemArm.ArmInst]
index_to_offset [definition, in ArchSemArm.VMPromising]
initial_reads_not_delayed [projection, in ArchSemArm.VMSA22Arm]
initial_reads [projection, in ArchSemArm.VMSA22Arm]
initial_reads_not_delayed [projection, in ArchSemArm.UMArm]
initial_reads [projection, in ArchSemArm.UMArm]
initial_reads [projection, in ArchSemArm.UMSeqArm]
instruction_order [abbreviation, in ArchSemArm.VMUMEquivThm]
instruction_order [abbreviation, in ArchSemArm.VMSA22Arm]
instruction_order [abbreviation, in ArchSemArm.UMArm]
instruction_order [abbreviation, in ArchSemArm.UMSeqArm]
int [abbreviation, in ArchSemArm.VMUMEquivThm]
int [abbreviation, in ArchSemArm.VMSA22Arm]
int [abbreviation, in ArchSemArm.UMArm]
int [abbreviation, in ArchSemArm.UMSeqArm]
internal [projection, in ArchSemArm.VMSA22Arm]
internal [projection, in ArchSemArm.UMArm]
ipa_page_overlap [definition, in ArchSemArm.VMSA22Arm]
IR [abbreviation, in ArchSemArm.VMUMEquivThm]
IR [abbreviation, in ArchSemArm.VMSA22Arm]
IR [abbreviation, in ArchSemArm.UMArm]
IR [abbreviation, in ArchSemArm.UMSeqArm]
irf [abbreviation, in ArchSemArm.VMUMEquivThm]
irf [abbreviation, in ArchSemArm.VMSA22Arm]
irf [abbreviation, in ArchSemArm.UMArm]
irf [abbreviation, in ArchSemArm.UMSeqArm]
irfe [abbreviation, in ArchSemArm.VMUMEquivThm]
irfe [abbreviation, in ArchSemArm.VMSA22Arm]
irfe [abbreviation, in ArchSemArm.UMArm]
irfe [abbreviation, in ArchSemArm.UMSeqArm]
irfi [abbreviation, in ArchSemArm.VMUMEquivThm]
irfi [abbreviation, in ArchSemArm.VMSA22Arm]
irfi [abbreviation, in ArchSemArm.UMArm]
irfi [abbreviation, in ArchSemArm.UMSeqArm]
isb [definition, in ArchSemArm.GenAxiomaticArm]
ISB [abbreviation, in ArchSemArm.VMUMEquivThm]
ISB [abbreviation, in ArchSemArm.VMSA22Arm]
ISB [abbreviation, in ArchSemArm.UMArm]
ISB [abbreviation, in ArchSemArm.UMSeqArm]
is_dmbnshT [definition, in ArchSemArm.GenAxiomaticArm]
is_dmbnsh [definition, in ArchSemArm.GenAxiomaticArm]
is_dmbnshP [definition, in ArchSemArm.GenAxiomaticArm]
is_dmbT [definition, in ArchSemArm.GenAxiomaticArm]
is_dmb [definition, in ArchSemArm.GenAxiomaticArm]
is_dmbP [definition, in ArchSemArm.GenAxiomaticArm]
is_dsbnshT [definition, in ArchSemArm.GenAxiomaticArm]
is_dsbnsh [definition, in ArchSemArm.GenAxiomaticArm]
is_dsbnshP [definition, in ArchSemArm.GenAxiomaticArm]
is_dsbT [definition, in ArchSemArm.GenAxiomaticArm]
is_dsb [definition, in ArchSemArm.GenAxiomaticArm]
is_dsbP [definition, in ArchSemArm.GenAxiomaticArm]
is_isb [definition, in ArchSemArm.GenAxiomaticArm]
is_bbm_violation [definition, in ArchSemArm.VMPromising]
is_addr_from_oa [definition, in ArchSemArm.VMPromising]
is_mmu_enabled [definition, in ArchSemArm.VMPromising]
is_contiguous [definition, in ArchSemArm.VMPromising]
is_non_global [definition, in ArchSemArm.VMPromising]
is_global [definition, in ArchSemArm.VMPromising]
is_tlb_fillable [definition, in ArchSemArm.VMPromising]
is_accessible_final [definition, in ArchSemArm.VMPromising]
is_final [definition, in ArchSemArm.VMPromising]
is_block [definition, in ArchSemArm.VMPromising]
is_table [definition, in ArchSemArm.VMPromising]
is_valid [definition, in ArchSemArm.VMPromising]
is_upper_va [definition, in ArchSemArm.VMPromising]
is_reg_unknown [definition, in ArchSemArm.VMPromising]
is_nms' [projection, in ArchSemArm.VMSA22Arm]
is_fault [abbreviation, in ArchSemArm.VMSA22Arm]
is_faultP_dec [instance, in ArchSemArm.VMSA22Arm]
is_faultP_spec [definition, in ArchSemArm.VMSA22Arm]
is_faultP [definition, in ArchSemArm.VMSA22Arm]
is_tlbi_shareability [definition, in ArchSemArm.VMSA22Arm]
is_tlbi_regime [definition, in ArchSemArm.VMSA22Arm]
is_tlbi_op [definition, in ArchSemArm.VMSA22Arm]
is_illegal_reg_write_dec [instance, in ArchSemArm.VMSA22Arm]
is_illegal_reg_write [definition, in ArchSemArm.VMSA22Arm]
is_nms' [projection, in ArchSemArm.UMArm]
is_illegal_reg_write_dec [instance, in ArchSemArm.UMArm]
is_illegal_reg_write [definition, in ArchSemArm.UMArm]
is_nms' [projection, in ArchSemArm.UMSeqArm]
is_illegal_reg_read_dec [instance, in ArchSemArm.UMSeqArm]
is_illegal_reg_read [definition, in ArchSemArm.UMSeqArm]
is_illegal_reg_write_dec [instance, in ArchSemArm.UMSeqArm]
is_illegal_reg_write [definition, in ArchSemArm.UMSeqArm]
L
L [abbreviation, in ArchSemArm.VMUMEquivThm]L [abbreviation, in ArchSemArm.VMSA22Arm]
L [abbreviation, in ArchSemArm.UMArm]
L [abbreviation, in ArchSemArm.UMSeqArm]
leaf_lvl [definition, in ArchSemArm.VMPromising]
LEv [module, in ArchSemArm.VMPromising]
Level [definition, in ArchSemArm.VMPromising]
level_index [definition, in ArchSemArm.VMPromising]
level_prefix [definition, in ArchSemArm.VMPromising]
level_length [definition, in ArchSemArm.VMPromising]
LEv.Cse [constructor, in ArchSemArm.VMPromising]
LEv.get_wsreg [definition, in ArchSemArm.VMPromising]
LEv.get_cse [definition, in ArchSemArm.VMPromising]
LEv.t [inductive, in ArchSemArm.VMPromising]
LEv.t_sind [definition, in ArchSemArm.VMPromising]
LEv.t_rec [definition, in ArchSemArm.VMPromising]
LEv.t_ind [definition, in ArchSemArm.VMPromising]
LEv.t_rect [definition, in ArchSemArm.VMPromising]
LEv.Wsreg [constructor, in ArchSemArm.VMPromising]
lxsx [abbreviation, in ArchSemArm.VMUMEquivThm]
lxsx [abbreviation, in ArchSemArm.VMSA22Arm]
lxsx [abbreviation, in ArchSemArm.UMArm]
lxsx [abbreviation, in ArchSemArm.UMSeqArm]
M
M [abbreviation, in ArchSemArm.VMUMEquivThm]M [abbreviation, in ArchSemArm.VMSA22Arm]
M [abbreviation, in ArchSemArm.UMArm]
M [abbreviation, in ArchSemArm.UMSeqArm]
match_prefix_at [definition, in ArchSemArm.VMPromising]
materialize_tlbi_for_recipient [definition, in ArchSemArm.VMPromising]
maybe_TLB_cached [definition, in ArchSemArm.VMSA22Arm]
Memory [module, in ArchSemArm.VMPromising]
Memory [module, in ArchSemArm.UMPromising]
memory_events_permitted [projection, in ArchSemArm.VMSA22Arm]
memory_events_permitted [projection, in ArchSemArm.UMArm]
memory_events_permitted [projection, in ArchSemArm.UMSeqArm]
Memory.cut_before [definition, in ArchSemArm.VMPromising]
Memory.cut_after [definition, in ArchSemArm.VMPromising]
Memory.cut_before [definition, in ArchSemArm.UMPromising]
Memory.cut_after [definition, in ArchSemArm.UMPromising]
Memory.exclusive [definition, in ArchSemArm.VMPromising]
Memory.exclusive [definition, in ArchSemArm.UMPromising]
Memory.exclusive_dec [instance, in ArchSemArm.VMPromising]
Memory.exclusive_dec [instance, in ArchSemArm.UMPromising]
Memory.fulfill [definition, in ArchSemArm.VMPromising]
Memory.fulfill [definition, in ArchSemArm.UMPromising]
Memory.promise [definition, in ArchSemArm.VMPromising]
Memory.promise [definition, in ArchSemArm.UMPromising]
Memory.read_word [definition, in ArchSemArm.VMPromising]
Memory.read_byte [definition, in ArchSemArm.VMPromising]
Memory.read_from [definition, in ArchSemArm.VMPromising]
Memory.read_initial [definition, in ArchSemArm.VMPromising]
Memory.read_last [definition, in ArchSemArm.VMPromising]
Memory.read_from [definition, in ArchSemArm.UMPromising]
Memory.read_initial [definition, in ArchSemArm.UMPromising]
Memory.read_last [definition, in ArchSemArm.UMPromising]
Memory.t [definition, in ArchSemArm.VMPromising]
Memory.t [definition, in ArchSemArm.UMPromising]
Memory.to_memMap [definition, in ArchSemArm.VMPromising]
Memory.to_memMap [definition, in ArchSemArm.UMPromising]
mem_contents_eq [definition, in ArchSemArm.VMPromising]
MRS [abbreviation, in ArchSemArm.VMUMEquivThm]
MRS [abbreviation, in ArchSemArm.VMSA22Arm]
MRS [abbreviation, in ArchSemArm.UMArm]
MRS [abbreviation, in ArchSemArm.UMSeqArm]
Msg [module, in ArchSemArm.VMPromising]
Msg [module, in ArchSemArm.UMPromising]
Msg.addr [projection, in ArchSemArm.UMPromising]
Msg.eq_dec [instance, in ArchSemArm.UMPromising]
Msg.read_byte [definition, in ArchSemArm.UMPromising]
Msg.size [projection, in ArchSemArm.UMPromising]
Msg.t [record, in ArchSemArm.UMPromising]
Msg.tid [projection, in ArchSemArm.UMPromising]
Msg.val [projection, in ArchSemArm.UMPromising]
MSR [abbreviation, in ArchSemArm.VMUMEquivThm]
MSR [abbreviation, in ArchSemArm.VMSA22Arm]
MSR [abbreviation, in ArchSemArm.UMArm]
MSR [abbreviation, in ArchSemArm.UMSeqArm]
MSR_obv_false [instance, in ArchSemArm.VMUMEquivThm]
N
next_entry_addr [definition, in ArchSemArm.VMPromising]NoCHERI [module, in ArchSemArm.ArmInst]
NoCHERI.no_cheri [definition, in ArchSemArm.ArmInst]
not_UB_dec [instance, in ArchSemArm.VMSA22Arm]
not_UB [record, in ArchSemArm.VMSA22Arm]
not_UB_dec [instance, in ArchSemArm.UMArm]
not_UB [record, in ArchSemArm.UMArm]
not_UB_dec [instance, in ArchSemArm.UMSeqArm]
not_UB [record, in ArchSemArm.UMSeqArm]
no_cacheop [projection, in ArchSemArm.VMSA22Arm]
no_cacheop [projection, in ArchSemArm.UMArm]
no_exceptions [projection, in ArchSemArm.UMArm]
no_exceptions [projection, in ArchSemArm.UMSeqArm]
O
ob [definition, in ArchSemArm.VMSA22Arm]ob [definition, in ArchSemArm.UMArm]
obETS [definition, in ArchSemArm.VMSA22Arm]
obETS2 [definition, in ArchSemArm.VMSA22Arm]
obfault [definition, in ArchSemArm.VMSA22Arm]
obs [definition, in ArchSemArm.VMSA22Arm]
obs [definition, in ArchSemArm.UMArm]
obtlbi [definition, in ArchSemArm.VMSA22Arm]
obtlbi_translate [definition, in ArchSemArm.VMSA22Arm]
ob1 [definition, in ArchSemArm.VMSA22Arm]
ob1 [definition, in ArchSemArm.UMArm]
offset_size [definition, in ArchSemArm.VMPromising]
output_addr [definition, in ArchSemArm.VMPromising]
output_addr_size [definition, in ArchSemArm.VMPromising]
P
page_of_addr [definition, in ArchSemArm.VMSA22Arm]parent_lvl_sub_one [lemma, in ArchSemArm.VMPromising]
parent_lvl [definition, in ArchSemArm.VMPromising]
pe [abbreviation, in ArchSemArm.VMUMEquivThm]
pe [abbreviation, in ArchSemArm.VMSA22Arm]
pe [abbreviation, in ArchSemArm.UMArm]
pe [abbreviation, in ArchSemArm.UMSeqArm]
Phase1 [section, in ArchSemArm.VMUMEquivThm]
Phase1.cd [variable, in ArchSemArm.VMUMEquivThm]
Phase1.cd_complete [variable, in ArchSemArm.VMUMEquivThm]
Phase1.cd_wf [variable, in ArchSemArm.VMUMEquivThm]
Phase1.initial_TTW_reads [variable, in ArchSemArm.VMUMEquivThm]
Phase1.nmth [variable, in ArchSemArm.VMUMEquivThm]
Phase1.NoCacheOp_implies_ob1_equal.NoCacheOp [variable, in ArchSemArm.VMUMEquivThm]
Phase1.NoCacheOp_implies_ob1_equal [section, in ArchSemArm.VMUMEquivThm]
Phase1.no_msr [variable, in ArchSemArm.VMUMEquivThm]
Phase1.no_tlbi [variable, in ArchSemArm.VMUMEquivThm]
Phase1.no_tf [variable, in ArchSemArm.VMUMEquivThm]
Phase1.no_exceptions [variable, in ArchSemArm.VMUMEquivThm]
Phase1.regs_whitelist [variable, in ArchSemArm.VMUMEquivThm]
Phase1.TTW_reads_not_delayed [variable, in ArchSemArm.VMUMEquivThm]
po [abbreviation, in ArchSemArm.VMUMEquivThm]
po [abbreviation, in ArchSemArm.VMSA22Arm]
po [abbreviation, in ArchSemArm.UMArm]
po [abbreviation, in ArchSemArm.UMSeqArm]
prefix [definition, in ArchSemArm.VMPromising]
prefix_to_va [definition, in ArchSemArm.VMPromising]
Q
Q [abbreviation, in ArchSemArm.VMUMEquivThm]Q [abbreviation, in ArchSemArm.VMSA22Arm]
Q [abbreviation, in ArchSemArm.UMArm]
Q [abbreviation, in ArchSemArm.UMSeqArm]
R
R [abbreviation, in ArchSemArm.VMUMEquivThm]R [abbreviation, in ArchSemArm.VMSA22Arm]
R [abbreviation, in ArchSemArm.UMArm]
R [abbreviation, in ArchSemArm.UMSeqArm]
RE [abbreviation, in ArchSemArm.VMUMEquivThm]
RE [abbreviation, in ArchSemArm.VMSA22Arm]
RE [abbreviation, in ArchSemArm.UMArm]
RE [abbreviation, in ArchSemArm.UMSeqArm]
read_fault_vpre [definition, in ArchSemArm.VMPromising]
read_pte [definition, in ArchSemArm.VMPromising]
read_mem_explicit [definition, in ArchSemArm.VMPromising]
read_fwd [definition, in ArchSemArm.VMPromising]
read_candidates [definition, in ArchSemArm.VMPromising]
read_imem [definition, in ArchSemArm.VMPromising]
read_mem [definition, in ArchSemArm.UMPromising]
read_fwd [definition, in ArchSemArm.UMPromising]
read_candidates [definition, in ArchSemArm.UMPromising]
read_imem [definition, in ArchSemArm.UMPromising]
register_write_permitted [projection, in ArchSemArm.VMSA22Arm]
register_write_permitted [projection, in ArchSemArm.UMArm]
register_read_permitted [projection, in ArchSemArm.UMSeqArm]
register_write_permitted [projection, in ArchSemArm.UMSeqArm]
regval_to_val [definition, in ArchSemArm.VMPromising]
reg_internal' [projection, in ArchSemArm.VMSA22Arm]
reg_internal' [projection, in ArchSemArm.UMArm]
relaxed_regs [definition, in ArchSemArm.VMPromising]
rf [abbreviation, in ArchSemArm.VMUMEquivThm]
rf [abbreviation, in ArchSemArm.VMSA22Arm]
rf [abbreviation, in ArchSemArm.UMArm]
rf [abbreviation, in ArchSemArm.UMSeqArm]
rfe [abbreviation, in ArchSemArm.VMUMEquivThm]
rfe [abbreviation, in ArchSemArm.VMSA22Arm]
rfe [abbreviation, in ArchSemArm.UMArm]
rfe [abbreviation, in ArchSemArm.UMSeqArm]
rfi [abbreviation, in ArchSemArm.VMUMEquivThm]
rfi [abbreviation, in ArchSemArm.VMSA22Arm]
rfi [abbreviation, in ArchSemArm.UMArm]
rfi [abbreviation, in ArchSemArm.UMSeqArm]
rfr [abbreviation, in ArchSemArm.VMUMEquivThm]
rfr [abbreviation, in ArchSemArm.VMSA22Arm]
rfr [abbreviation, in ArchSemArm.UMArm]
rfr [abbreviation, in ArchSemArm.UMSeqArm]
rmw [abbreviation, in ArchSemArm.VMUMEquivThm]
rmw [abbreviation, in ArchSemArm.VMSA22Arm]
rmw [abbreviation, in ArchSemArm.UMArm]
rmw [abbreviation, in ArchSemArm.UMSeqArm]
root_ttbr [definition, in ArchSemArm.VMPromising]
root_lvl [definition, in ArchSemArm.VMPromising]
RR [abbreviation, in ArchSemArm.VMUMEquivThm]
RR [abbreviation, in ArchSemArm.VMSA22Arm]
RR [abbreviation, in ArchSemArm.UMArm]
RR [abbreviation, in ArchSemArm.UMSeqArm]
rrf [abbreviation, in ArchSemArm.VMUMEquivThm]
rrf [abbreviation, in ArchSemArm.VMSA22Arm]
rrf [abbreviation, in ArchSemArm.UMArm]
rrf [abbreviation, in ArchSemArm.UMSeqArm]
RunOutcome [section, in ArchSemArm.VMPromising]
RunOutcome [section, in ArchSemArm.UMPromising]
RunOutcome.initmem [variable, in ArchSemArm.VMPromising]
RunOutcome.initmem [variable, in ArchSemArm.UMPromising]
RunOutcome.n_threads [variable, in ArchSemArm.VMPromising]
RunOutcome.tid [variable, in ArchSemArm.VMPromising]
RunOutcome.tid [variable, in ArchSemArm.UMPromising]
run_outcome' [definition, in ArchSemArm.VMPromising]
run_outcome [definition, in ArchSemArm.VMPromising]
run_take_exception [definition, in ArchSemArm.VMPromising]
run_trans_end [definition, in ArchSemArm.VMPromising]
run_trans_start [definition, in ArchSemArm.VMPromising]
run_tlbi [definition, in ArchSemArm.VMPromising]
run_barrier [definition, in ArchSemArm.VMPromising]
run_cse [definition, in ArchSemArm.VMPromising]
run_reg_write [definition, in ArchSemArm.VMPromising]
run_reg_read [definition, in ArchSemArm.VMPromising]
run_reg_trans_read [definition, in ArchSemArm.VMPromising]
run_reg_general_read [definition, in ArchSemArm.VMPromising]
run_outcome' [definition, in ArchSemArm.UMPromising]
run_outcome [definition, in ArchSemArm.UMPromising]
RW [abbreviation, in ArchSemArm.VMUMEquivThm]
RW [abbreviation, in ArchSemArm.VMSA22Arm]
RW [abbreviation, in ArchSemArm.UMArm]
RW [abbreviation, in ArchSemArm.UMSeqArm]
Rx [abbreviation, in ArchSemArm.VMUMEquivThm]
Rx [abbreviation, in ArchSemArm.VMSA22Arm]
Rx [abbreviation, in ArchSemArm.UMArm]
Rx [abbreviation, in ArchSemArm.UMSeqArm]
S
SA [module, in ArchSemArm.ArmInst]sail_tiny_arm_sem [definition, in ArchSemArm.ArmInst]
same_asid [definition, in ArchSemArm.VMSA22Arm]
same_vmid [definition, in ArchSemArm.VMSA22Arm]
same_translation [definition, in ArchSemArm.VMSA22Arm]
sca [abbreviation, in ArchSemArm.VMUMEquivThm]
sca [abbreviation, in ArchSemArm.VMSA22Arm]
sca [abbreviation, in ArchSemArm.UMArm]
sca [abbreviation, in ArchSemArm.UMSeqArm]
shareability [definition, in ArchSemArm.VMPromising]
si [abbreviation, in ArchSemArm.VMUMEquivThm]
si [abbreviation, in ArchSemArm.VMSA22Arm]
si [abbreviation, in ArchSemArm.UMArm]
SI [module, in ArchSemArm.ArmInst]
si [abbreviation, in ArchSemArm.UMSeqArm]
speculative [definition, in ArchSemArm.VMSA22Arm]
speculative [definition, in ArchSemArm.UMArm]
Stage1 [definition, in ArchSemArm.VMSA22Arm]
Stage2 [definition, in ArchSemArm.VMSA22Arm]
strict_regs [definition, in ArchSemArm.VMPromising]
T
T [abbreviation, in ArchSemArm.VMUMEquivThm]T [abbreviation, in ArchSemArm.VMSA22Arm]
T [abbreviation, in ArchSemArm.UMArm]
T [abbreviation, in ArchSemArm.UMSeqArm]
TE [abbreviation, in ArchSemArm.VMUMEquivThm]
TE [abbreviation, in ArchSemArm.VMSA22Arm]
TE [abbreviation, in ArchSemArm.UMArm]
TE [abbreviation, in ArchSemArm.UMSeqArm]
TE_obv_false [instance, in ArchSemArm.VMUMEquivThm]
tfr [abbreviation, in ArchSemArm.VMUMEquivThm]
tfr [abbreviation, in ArchSemArm.VMSA22Arm]
tfr [abbreviation, in ArchSemArm.UMArm]
tfr [abbreviation, in ArchSemArm.UMSeqArm]
tfre [abbreviation, in ArchSemArm.VMUMEquivThm]
tfre [abbreviation, in ArchSemArm.VMSA22Arm]
tfre [abbreviation, in ArchSemArm.UMArm]
tfre [abbreviation, in ArchSemArm.UMSeqArm]
tfri [abbreviation, in ArchSemArm.VMUMEquivThm]
tfri [abbreviation, in ArchSemArm.VMSA22Arm]
tfri [abbreviation, in ArchSemArm.UMArm]
tfri [abbreviation, in ArchSemArm.UMSeqArm]
TLB [module, in ArchSemArm.VMPromising]
TLBI [module, in ArchSemArm.VMPromising]
TLBI [abbreviation, in ArchSemArm.VMUMEquivThm]
TLBI [abbreviation, in ArchSemArm.VMSA22Arm]
TLBI [abbreviation, in ArchSemArm.UMArm]
TLBI [abbreviation, in ArchSemArm.UMSeqArm]
TLBI_obv_false [instance, in ArchSemArm.VMUMEquivThm]
tlbi_translate_same_ipa_page [definition, in ArchSemArm.VMSA22Arm]
tlbi_translate_same_va_page [definition, in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_sind [definition, in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_rec [definition, in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_ind [definition, in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_rect [definition, in ArchSemArm.VMSA22Arm]
TLBI_ak_ipa [constructor, in ArchSemArm.VMSA22Arm]
TLBI_ak_va [constructor, in ArchSemArm.VMSA22Arm]
TLBI_ak_no [constructor, in ArchSemArm.VMSA22Arm]
TLBI_ak_unsupported [constructor, in ArchSemArm.VMSA22Arm]
TLBI_addr_kind [inductive, in ArchSemArm.VMSA22Arm]
tlbi_translate_same_vmid [definition, in ArchSemArm.VMSA22Arm]
tlbi_translate_same_asid [definition, in ArchSemArm.VMSA22Arm]
TLBI_IS [definition, in ArchSemArm.VMSA22Arm]
TLBI_EL2 [definition, in ArchSemArm.VMSA22Arm]
TLBI_EL1 [definition, in ArchSemArm.VMSA22Arm]
TLBI_IPA [definition, in ArchSemArm.VMSA22Arm]
TLBI_VA [definition, in ArchSemArm.VMSA22Arm]
TLBI_VMID [definition, in ArchSemArm.VMSA22Arm]
TLBI_S2 [definition, in ArchSemArm.VMSA22Arm]
TLBI_S1 [definition, in ArchSemArm.VMSA22Arm]
TLBI_ASID [definition, in ArchSemArm.VMSA22Arm]
TLBI.All [constructor, in ArchSemArm.VMPromising]
TLBI.asid [definition, in ArchSemArm.VMPromising]
TLBI.Asid [constructor, in ArchSemArm.VMPromising]
TLBI.asid_opt [definition, in ArchSemArm.VMPromising]
TLBI.dec [instance, in ArchSemArm.VMPromising]
TLBI.last [definition, in ArchSemArm.VMPromising]
TLBI.last_opt [definition, in ArchSemArm.VMPromising]
TLBI.t [inductive, in ArchSemArm.VMPromising]
TLBI.tid [definition, in ArchSemArm.VMPromising]
TLBI.t_sind [definition, in ArchSemArm.VMPromising]
TLBI.t_rec [definition, in ArchSemArm.VMPromising]
TLBI.t_ind [definition, in ArchSemArm.VMPromising]
TLBI.t_rect [definition, in ArchSemArm.VMPromising]
TLBI.upper_opt [definition, in ArchSemArm.VMPromising]
TLBI.va [definition, in ArchSemArm.VMPromising]
TLBI.Va [constructor, in ArchSemArm.VMPromising]
TLBI.Vaa [constructor, in ArchSemArm.VMPromising]
TLBI.va_opt [definition, in ArchSemArm.VMPromising]
tlb_barriered [definition, in ArchSemArm.VMSA22Arm]
tlb_affects [definition, in ArchSemArm.VMSA22Arm]
tlb_might_affect [definition, in ArchSemArm.VMSA22Arm]
TLB.affects [definition, in ArchSemArm.VMPromising]
TLB.affects_va [definition, in ArchSemArm.VMPromising]
TLB.affects_asid [definition, in ArchSemArm.VMPromising]
TLB.apply_tlbi_for_tid [definition, in ArchSemArm.VMPromising]
TLB.candidate_inv_time [projection, in ArchSemArm.VMPromising]
TLB.candidate_end [projection, in ArchSemArm.VMPromising]
TLB.candidate_start [projection, in ArchSemArm.VMPromising]
TLB.candidate_path [projection, in ArchSemArm.VMPromising]
TLB.candidate_ttbr [projection, in ArchSemArm.VMPromising]
TLB.Ctxt [module, in ArchSemArm.VMPromising]
TLB.Ctxt.asid [definition, in ArchSemArm.VMPromising]
TLB.Ctxt.lvl [definition, in ArchSemArm.VMPromising]
TLB.Ctxt.nd [definition, in ArchSemArm.VMPromising]
TLB.Ctxt.t [definition, in ArchSemArm.VMPromising]
TLB.Ctxt.upper [definition, in ArchSemArm.VMPromising]
TLB.Ctxt.va [definition, in ArchSemArm.VMPromising]
TLB.Decision_is_te_invalidated_by_tlbi [instance, in ArchSemArm.VMPromising]
TLB.Decision_affects [instance, in ArchSemArm.VMPromising]
TLB.Decision_affects_va [instance, in ArchSemArm.VMPromising]
TLB.Decision_affects_asid [instance, in ArchSemArm.VMPromising]
TLB.Decision_is_active_asid [instance, in ArchSemArm.VMPromising]
TLB.Entry [module, in ArchSemArm.VMPromising]
TLB.Entry.append [definition, in ArchSemArm.VMPromising]
TLB.Entry.count [instance, in ArchSemArm.VMPromising]
TLB.Entry.eqdep_dec [instance, in ArchSemArm.VMPromising]
TLB.Entry.eq_dec [instance, in ArchSemArm.VMPromising]
TLB.Entry.pte [definition, in ArchSemArm.VMPromising]
TLB.Entry.ptes [projection, in ArchSemArm.VMPromising]
TLB.Entry.t [record, in ArchSemArm.VMPromising]
TLB.Entry.val_ttbr [projection, in ArchSemArm.VMPromising]
TLB.FE [module, in ArchSemArm.VMPromising]
TLB.FE.asid [definition, in ArchSemArm.VMPromising]
TLB.FE.ctxt [definition, in ArchSemArm.VMPromising]
TLB.FE.lvl [definition, in ArchSemArm.VMPromising]
TLB.FE.pte [definition, in ArchSemArm.VMPromising]
TLB.FE.ptes [definition, in ArchSemArm.VMPromising]
TLB.FE.t [definition, in ArchSemArm.VMPromising]
TLB.FE.va [definition, in ArchSemArm.VMPromising]
TLB.get_invalid_entries_from_snapshots [definition, in ArchSemArm.VMPromising]
TLB.get_invalid_entries_from_range [definition, in ArchSemArm.VMPromising]
TLB.get_valid_entries_from_snapshots [definition, in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time [definition, in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time_by_lvl [definition, in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time_by_lvl_asid [definition, in ArchSemArm.VMPromising]
TLB.get_leaf_ptes_with_inv_time [definition, in ArchSemArm.VMPromising]
TLB.get_leaf_ptes_with_inv_time_by_ctxt [definition, in ArchSemArm.VMPromising]
TLB.init [definition, in ArchSemArm.VMPromising]
TLB.invalidation_time [definition, in ArchSemArm.VMPromising]
TLB.invalidation_time_from_evs [definition, in ArchSemArm.VMPromising]
TLB.is_te_invalidated_by_tlbi [definition, in ArchSemArm.VMPromising]
TLB.is_upper_ttbr [definition, in ArchSemArm.VMPromising]
TLB.is_active_asid [definition, in ArchSemArm.VMPromising]
TLB.lookup [definition, in ArchSemArm.VMPromising]
TLB.NDCtxt [module, in ArchSemArm.VMPromising]
TLB.NDCtxt.asid [projection, in ArchSemArm.VMPromising]
TLB.NDCtxt.count [instance, in ArchSemArm.VMPromising]
TLB.NDCtxt.eqdep_dec [instance, in ArchSemArm.VMPromising]
TLB.NDCtxt.eq_dec [instance, in ArchSemArm.VMPromising]
TLB.NDCtxt.t [record, in ArchSemArm.VMPromising]
TLB.NDCtxt.upper [projection, in ArchSemArm.VMPromising]
TLB.NDCtxt.va [projection, in ArchSemArm.VMPromising]
TLB.next_va [definition, in ArchSemArm.VMPromising]
TLB.range_end [projection, in ArchSemArm.VMPromising]
TLB.range_start [projection, in ArchSemArm.VMPromising]
TLB.range_tlb [projection, in ArchSemArm.VMPromising]
TLB.snapshots_from_until [definition, in ArchSemArm.VMPromising]
TLB.snapshots_from [definition, in ArchSemArm.VMPromising]
TLB.snapshot_range [record, in ArchSemArm.VMPromising]
TLB.t [record, in ArchSemArm.VMPromising]
TLB.tlbi_apply [definition, in ArchSemArm.VMPromising]
TLB.trans_candidate [record, in ArchSemArm.VMPromising]
TLB.traverse [definition, in ArchSemArm.VMPromising]
TLB.traverse_lvl [definition, in ArchSemArm.VMPromising]
TLB.traverse_root [definition, in ArchSemArm.VMPromising]
TLB.ttbr_asid_roots_at [definition, in ArchSemArm.VMPromising]
TLB.ttbr_asids_at [definition, in ArchSemArm.VMPromising]
TLB.ttbr_values_at [definition, in ArchSemArm.VMPromising]
TLB.unique_snapshots_until [definition, in ArchSemArm.VMPromising]
TLB.unique_snapshots_between [definition, in ArchSemArm.VMPromising]
TLB.unique_snapshots_va [definition, in ArchSemArm.VMPromising]
TLB.unique_snapshots_va_until [definition, in ArchSemArm.VMPromising]
TLB.unique_snapshots_va_between [definition, in ArchSemArm.VMPromising]
TLB.update [definition, in ArchSemArm.VMPromising]
TLB.update_all [definition, in ArchSemArm.VMPromising]
TLB.vatlb [projection, in ArchSemArm.VMPromising]
TLB.VATLB [module, in ArchSemArm.VMPromising]
TLB.VATLB.elements [instance, in ArchSemArm.VMPromising]
TLB.VATLB.empty [instance, in ArchSemArm.VMPromising]
TLB.VATLB.filter [instance, in ArchSemArm.VMPromising]
TLB.VATLB.final_entries [definition, in ArchSemArm.VMPromising]
TLB.VATLB.get [definition, in ArchSemArm.VMPromising]
TLB.VATLB.getFE [definition, in ArchSemArm.VMPromising]
TLB.VATLB.init [definition, in ArchSemArm.VMPromising]
TLB.VATLB.insert [definition, in ArchSemArm.VMPromising]
TLB.VATLB.setFEs [definition, in ArchSemArm.VMPromising]
TLB.VATLB.singleton [definition, in ArchSemArm.VMPromising]
TLB.VATLB.t [definition, in ArchSemArm.VMPromising]
TLB.VATLB.T [definition, in ArchSemArm.VMPromising]
TLB.VATLB.union [instance, in ArchSemArm.VMPromising]
TLB.VATLB.vatlb_dom [instance, in ArchSemArm.VMPromising]
TLB.va_fill [definition, in ArchSemArm.VMPromising]
TLB.va_fill_lvl [definition, in ArchSemArm.VMPromising]
TLB.va_fill_root [definition, in ArchSemArm.VMPromising]
tob [definition, in ArchSemArm.VMSA22Arm]
total [projection, in ArchSemArm.UMSeqArm]
translation_internal [projection, in ArchSemArm.VMSA22Arm]
trf [abbreviation, in ArchSemArm.VMUMEquivThm]
trf [abbreviation, in ArchSemArm.VMSA22Arm]
trf [abbreviation, in ArchSemArm.UMArm]
trf [abbreviation, in ArchSemArm.UMSeqArm]
trfe [abbreviation, in ArchSemArm.VMUMEquivThm]
trfe [abbreviation, in ArchSemArm.VMSA22Arm]
trfe [abbreviation, in ArchSemArm.UMArm]
trfe [abbreviation, in ArchSemArm.UMSeqArm]
trfe_obv_false [instance, in ArchSemArm.VMUMEquivThm]
trfi [abbreviation, in ArchSemArm.VMUMEquivThm]
trfi [abbreviation, in ArchSemArm.VMSA22Arm]
trfi [abbreviation, in ArchSemArm.UMArm]
trfi [abbreviation, in ArchSemArm.UMSeqArm]
trfi_obv_false [instance, in ArchSemArm.VMUMEquivThm]
trf_obv_false [instance, in ArchSemArm.VMUMEquivThm]
trf_empty [lemma, in ArchSemArm.VMUMEquivThm]
TState [module, in ArchSemArm.VMPromising]
TState [module, in ArchSemArm.UMPromising]
TState.add_wsreg [definition, in ArchSemArm.VMPromising]
TState.clear_xclb [definition, in ArchSemArm.VMPromising]
TState.clear_xclb [definition, in ArchSemArm.UMPromising]
TState.coh [projection, in ArchSemArm.VMPromising]
TState.coh [projection, in ArchSemArm.UMPromising]
TState.cse [definition, in ArchSemArm.VMPromising]
TState.cse_candidates [definition, in ArchSemArm.VMPromising]
TState.cse_position [definition, in ArchSemArm.VMPromising]
TState.Decision_no_write_promises_until [instance, in ArchSemArm.VMPromising]
TState.Decision_no_promises_until [instance, in ArchSemArm.VMPromising]
TState.Decision_tcohs_before_inv_time [instance, in ArchSemArm.VMPromising]
TState.Decision_no_promises_until [instance, in ArchSemArm.UMPromising]
TState.eta [instance, in ArchSemArm.VMPromising]
TState.eta [instance, in ArchSemArm.UMPromising]
TState.filter_cse [definition, in ArchSemArm.VMPromising]
TState.filter_wsreg [definition, in ArchSemArm.VMPromising]
TState.fwdb [projection, in ArchSemArm.VMPromising]
TState.fwdb [projection, in ArchSemArm.UMPromising]
TState.get_tcoh [definition, in ArchSemArm.VMPromising]
TState.init [definition, in ArchSemArm.VMPromising]
TState.init [definition, in ArchSemArm.UMPromising]
TState.levs [projection, in ArchSemArm.VMPromising]
TState.lev_cur [definition, in ArchSemArm.VMPromising]
TState.max_cohs [definition, in ArchSemArm.VMPromising]
TState.min_promise [definition, in ArchSemArm.VMPromising]
TState.no_write_promises_until [definition, in ArchSemArm.VMPromising]
TState.no_promises_until [definition, in ArchSemArm.VMPromising]
TState.no_promises_until [definition, in ArchSemArm.UMPromising]
TState.prom [projection, in ArchSemArm.UMPromising]
TState.promise [definition, in ArchSemArm.UMPromising]
TState.promise_tlbi [definition, in ArchSemArm.VMPromising]
TState.promise_write [definition, in ArchSemArm.VMPromising]
TState.prom_tlbi [projection, in ArchSemArm.VMPromising]
TState.prom_wr [projection, in ArchSemArm.VMPromising]
TState.read_reg [definition, in ArchSemArm.VMPromising]
TState.read_sreg_at [definition, in ArchSemArm.VMPromising]
TState.read_sreg_indirect [definition, in ArchSemArm.VMPromising]
TState.read_sreg_direct [definition, in ArchSemArm.VMPromising]
TState.read_sreg_by_cse [definition, in ArchSemArm.VMPromising]
TState.read_sreg_last [definition, in ArchSemArm.VMPromising]
TState.regs [projection, in ArchSemArm.VMPromising]
TState.regs [projection, in ArchSemArm.UMPromising]
TState.reg_map [definition, in ArchSemArm.VMPromising]
TState.reg_map [definition, in ArchSemArm.UMPromising]
TState.set_xclb [definition, in ArchSemArm.VMPromising]
TState.set_fwdbs [definition, in ArchSemArm.VMPromising]
TState.set_fwdb [definition, in ArchSemArm.VMPromising]
TState.set_coh [definition, in ArchSemArm.VMPromising]
TState.set_reg [definition, in ArchSemArm.VMPromising]
TState.set_xclb [definition, in ArchSemArm.UMPromising]
TState.set_fwdbs [definition, in ArchSemArm.UMPromising]
TState.set_fwdb [definition, in ArchSemArm.UMPromising]
TState.set_coh [definition, in ArchSemArm.UMPromising]
TState.set_reg [definition, in ArchSemArm.UMPromising]
TState.t [record, in ArchSemArm.VMPromising]
TState.t [record, in ArchSemArm.UMPromising]
TState.tcoh [projection, in ArchSemArm.VMPromising]
TState.tcohs_before_inv_time [definition, in ArchSemArm.VMPromising]
TState.update [definition, in ArchSemArm.VMPromising]
TState.update [definition, in ArchSemArm.UMPromising]
TState.update_tcohs [definition, in ArchSemArm.VMPromising]
TState.update_tcoh [definition, in ArchSemArm.VMPromising]
TState.update_cohs [definition, in ArchSemArm.VMPromising]
TState.update_coh [definition, in ArchSemArm.VMPromising]
TState.update_cohs [definition, in ArchSemArm.UMPromising]
TState.update_coh [definition, in ArchSemArm.UMPromising]
TState.update2 [definition, in ArchSemArm.VMPromising]
TState.update2 [definition, in ArchSemArm.UMPromising]
TState.vacq [projection, in ArchSemArm.VMPromising]
TState.vacq [projection, in ArchSemArm.UMPromising]
TState.va_page_offsets [definition, in ArchSemArm.VMPromising]
TState.vcap [projection, in ArchSemArm.UMPromising]
TState.vcse [projection, in ArchSemArm.VMPromising]
TState.vdmb [projection, in ArchSemArm.VMPromising]
TState.vdmb [projection, in ArchSemArm.UMPromising]
TState.vdmbst [projection, in ArchSemArm.VMPromising]
TState.vdmbst [projection, in ArchSemArm.UMPromising]
TState.vdsb [projection, in ArchSemArm.VMPromising]
TState.visb [projection, in ArchSemArm.UMPromising]
TState.vmsr [projection, in ArchSemArm.VMPromising]
TState.vrd [projection, in ArchSemArm.VMPromising]
TState.vrd [projection, in ArchSemArm.UMPromising]
TState.vrel [projection, in ArchSemArm.VMPromising]
TState.vrel [projection, in ArchSemArm.UMPromising]
TState.vspec [projection, in ArchSemArm.VMPromising]
TState.vtlbi_other [projection, in ArchSemArm.VMPromising]
TState.vtlbi_self [projection, in ArchSemArm.VMPromising]
TState.vwr [projection, in ArchSemArm.VMPromising]
TState.vwr [projection, in ArchSemArm.UMPromising]
TState.xclb [projection, in ArchSemArm.VMPromising]
TState.xclb [projection, in ArchSemArm.UMPromising]
ttbrs [definition, in ArchSemArm.VMPromising]
T_f_obv_false [instance, in ArchSemArm.VMUMEquivThm]
T_f [abbreviation, in ArchSemArm.VMUMEquivThm]
T_f [abbreviation, in ArchSemArm.VMSA22Arm]
U
UM [module, in ArchSemArm.VMUMEquivThm]UMArm [section, in ArchSemArm.UMArm]
UMArm [library]
UMArm.cd [variable, in ArchSemArm.UMArm]
UMArm.ms [variable, in ArchSemArm.UMArm]
UMArm.nmth [variable, in ArchSemArm.UMArm]
UMArm.regs_whitelist [variable, in ArchSemArm.UMArm]
UMPromising [definition, in ArchSemArm.UMPromising]
UMPromising [library]
UMPromising_opmodel_pf [definition, in ArchSemArm.UMPromising]
UMPromising_opmodel [definition, in ArchSemArm.UMPromising]
UMPromising_pf [definition, in ArchSemArm.UMPromising]
UMPromising_exe [definition, in ArchSemArm.UMPromising]
UMPromising_cert [definition, in ArchSemArm.UMPromising]
UMPromising_nocert [definition, in ArchSemArm.UMPromising]
UMSeqArm [section, in ArchSemArm.UMSeqArm]
UMSeqArm [library]
UMSeqArm.cd [variable, in ArchSemArm.UMSeqArm]
UMSeqArm.nmth [variable, in ArchSemArm.UMSeqArm]
UMSeqArm.regs_whitelist [variable, in ArchSemArm.UMSeqArm]
UM_to_VM_speculative [lemma, in ArchSemArm.VMUMEquivThm]
UM_to_VMSA_bob [lemma, in ArchSemArm.VMUMEquivThm]
UM_to_VMSA_dob [lemma, in ArchSemArm.VMUMEquivThm]
UM_VMSA_aob [lemma, in ArchSemArm.VMUMEquivThm]
UM_VMSA_obs [lemma, in ArchSemArm.VMUMEquivThm]
V
valid_eids_compl [definition, in ArchSemArm.VMSA22Arm]valid_eids_rc [definition, in ArchSemArm.VMSA22Arm]
val_to_regval [definition, in ArchSemArm.VMPromising]
val_to_addr [definition, in ArchSemArm.VMPromising]
VATLB [module, in ArchSemArm.VMPromising]
va_ranges_overlap [definition, in ArchSemArm.VMPromising]
va_to_vpn [definition, in ArchSemArm.VMPromising]
va_in_range [definition, in ArchSemArm.VMPromising]
va_page_overlap [definition, in ArchSemArm.VMSA22Arm]
view [definition, in ArchSemArm.VMPromising]
view [definition, in ArchSemArm.UMPromising]
view_if [definition, in ArchSemArm.VMPromising]
view_if [definition, in ArchSemArm.UMPromising]
VMPromising [definition, in ArchSemArm.VMPromising]
VMPromising [library]
VMPromising_opmodel_pf [definition, in ArchSemArm.VMPromising]
VMPromising_opmodel [definition, in ArchSemArm.VMPromising]
VMPromising_pf [definition, in ArchSemArm.VMPromising]
VMPromising_exe [definition, in ArchSemArm.VMPromising]
VMPromising_cert [definition, in ArchSemArm.VMPromising]
VMPromising_nocert [definition, in ArchSemArm.VMPromising]
VMSA [module, in ArchSemArm.VMUMEquivThm]
VMSAArm [section, in ArchSemArm.VMSA22Arm]
VMSAArm.cd [variable, in ArchSemArm.VMSA22Arm]
VMSAArm.isFault [section, in ArchSemArm.VMSA22Arm]
VMSAArm.isFault.P [variable, in ArchSemArm.VMSA22Arm]
VMSAArm.isFault.Pdec [variable, in ArchSemArm.VMSA22Arm]
VMSAArm.nmth [variable, in ArchSemArm.VMSA22Arm]
VMSAArm.regs_whitelist [variable, in ArchSemArm.VMSA22Arm]
~~ _ (stdpp_scope) [notation, in ArchSemArm.VMSA22Arm]
_ ? (stdpp_scope) [notation, in ArchSemArm.VMSA22Arm]
id [notation, in ArchSemArm.VMSA22Arm]
VMSA_UM_ob [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_UM_ob1 [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_obETS_obv_false [instance, in ArchSemArm.VMUMEquivThm]
VMSA_obETS_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_obfault_obv_false [instance, in ArchSemArm.VMUMEquivThm]
VMSA_obfault_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_Fault_T_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_ctxob_simpl [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_obv_false [instance, in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_translate_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_TLBIS2_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_TLBIS1_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA_tob_obv_false [instance, in ArchSemArm.VMUMEquivThm]
VMSA_tob_empty [lemma, in ArchSemArm.VMUMEquivThm]
VMSA22Arm [library]
VMUMEquivThm [library]
VMUM_phase1 [lemma, in ArchSemArm.VMUMEquivThm]
W
W [abbreviation, in ArchSemArm.VMUMEquivThm]W [abbreviation, in ArchSemArm.VMSA22Arm]
W [abbreviation, in ArchSemArm.UMArm]
W [abbreviation, in ArchSemArm.UMSeqArm]
wco [definition, in ArchSemArm.VMSA22Arm]
write_fault_vpre [definition, in ArchSemArm.VMPromising]
write_mem [definition, in ArchSemArm.VMPromising]
write_mem [definition, in ArchSemArm.UMPromising]
WSReg [module, in ArchSemArm.VMPromising]
WSReg.eta [instance, in ArchSemArm.VMPromising]
WSReg.sreg [projection, in ArchSemArm.VMPromising]
WSReg.t [record, in ArchSemArm.VMPromising]
WSReg.to_val_view_if [definition, in ArchSemArm.VMPromising]
WSReg.val [projection, in ArchSemArm.VMPromising]
WSReg.view [projection, in ArchSemArm.VMPromising]
Wx [abbreviation, in ArchSemArm.VMUMEquivThm]
Wx [abbreviation, in ArchSemArm.VMSA22Arm]
Wx [abbreviation, in ArchSemArm.UMArm]
Wx [abbreviation, in ArchSemArm.UMSeqArm]
X
XclItem [module, in ArchSemArm.VMPromising]XclItem [module, in ArchSemArm.UMPromising]
XclItem.addr [projection, in ArchSemArm.UMPromising]
XclItem.size [projection, in ArchSemArm.UMPromising]
XclItem.t [record, in ArchSemArm.UMPromising]
XclItem.time [projection, in ArchSemArm.UMPromising]
XclItem.view [projection, in ArchSemArm.UMPromising]
Notation Index
V
~~ _ (stdpp_scope) [in ArchSemArm.VMSA22Arm]_ ? (stdpp_scope) [in ArchSemArm.VMSA22Arm]
id [in ArchSemArm.VMSA22Arm]
Module Index
A
Arch [in ArchSemArm.ArmInst]ArchExtra [in ArchSemArm.ArmInst]
Arm [in ArchSemArm.ArmInst]
AxArmNames [in ArchSemArm.GenAxiomaticArm]
B
BBM [in ArchSemArm.VMPromising]E
Ev [in ArchSemArm.VMPromising]F
FwdItem [in ArchSemArm.VMPromising]FwdItem [in ArchSemArm.UMPromising]
I
IIS [in ArchSemArm.VMPromising]IIS [in ArchSemArm.UMPromising]
IIS.TransRes [in ArchSemArm.VMPromising]
IMonFromSail [in ArchSemArm.ArmInst]
L
LEv [in ArchSemArm.VMPromising]M
Memory [in ArchSemArm.VMPromising]Memory [in ArchSemArm.UMPromising]
Msg [in ArchSemArm.VMPromising]
Msg [in ArchSemArm.UMPromising]
N
NoCHERI [in ArchSemArm.ArmInst]S
SA [in ArchSemArm.ArmInst]SI [in ArchSemArm.ArmInst]
T
TLB [in ArchSemArm.VMPromising]TLBI [in ArchSemArm.VMPromising]
TLB.Ctxt [in ArchSemArm.VMPromising]
TLB.Entry [in ArchSemArm.VMPromising]
TLB.FE [in ArchSemArm.VMPromising]
TLB.NDCtxt [in ArchSemArm.VMPromising]
TLB.VATLB [in ArchSemArm.VMPromising]
TState [in ArchSemArm.VMPromising]
TState [in ArchSemArm.UMPromising]
U
UM [in ArchSemArm.VMUMEquivThm]V
VATLB [in ArchSemArm.VMPromising]VMSA [in ArchSemArm.VMUMEquivThm]
W
WSReg [in ArchSemArm.VMPromising]X
XclItem [in ArchSemArm.VMPromising]XclItem [in ArchSemArm.UMPromising]
Variable Index
A
AxArmNames.ArmNames.cd [in ArchSemArm.GenAxiomaticArm]AxArmNames.ArmNames.et [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ArmNames.nmth [in ArchSemArm.GenAxiomaticArm]
B
Barriers.et [in ArchSemArm.GenAxiomaticArm]Barriers.nmth [in ArchSemArm.GenAxiomaticArm]
BBM.initmem [in ArchSemArm.VMPromising]
P
Phase1.cd [in ArchSemArm.VMUMEquivThm]Phase1.cd_complete [in ArchSemArm.VMUMEquivThm]
Phase1.cd_wf [in ArchSemArm.VMUMEquivThm]
Phase1.initial_TTW_reads [in ArchSemArm.VMUMEquivThm]
Phase1.nmth [in ArchSemArm.VMUMEquivThm]
Phase1.NoCacheOp_implies_ob1_equal.NoCacheOp [in ArchSemArm.VMUMEquivThm]
Phase1.no_msr [in ArchSemArm.VMUMEquivThm]
Phase1.no_tlbi [in ArchSemArm.VMUMEquivThm]
Phase1.no_tf [in ArchSemArm.VMUMEquivThm]
Phase1.no_exceptions [in ArchSemArm.VMUMEquivThm]
Phase1.regs_whitelist [in ArchSemArm.VMUMEquivThm]
Phase1.TTW_reads_not_delayed [in ArchSemArm.VMUMEquivThm]
R
RunOutcome.initmem [in ArchSemArm.VMPromising]RunOutcome.initmem [in ArchSemArm.UMPromising]
RunOutcome.n_threads [in ArchSemArm.VMPromising]
RunOutcome.tid [in ArchSemArm.VMPromising]
RunOutcome.tid [in ArchSemArm.UMPromising]
U
UMArm.cd [in ArchSemArm.UMArm]UMArm.ms [in ArchSemArm.UMArm]
UMArm.nmth [in ArchSemArm.UMArm]
UMArm.regs_whitelist [in ArchSemArm.UMArm]
UMSeqArm.cd [in ArchSemArm.UMSeqArm]
UMSeqArm.nmth [in ArchSemArm.UMSeqArm]
UMSeqArm.regs_whitelist [in ArchSemArm.UMSeqArm]
V
VMSAArm.cd [in ArchSemArm.VMSA22Arm]VMSAArm.isFault.P [in ArchSemArm.VMSA22Arm]
VMSAArm.isFault.Pdec [in ArchSemArm.VMSA22Arm]
VMSAArm.nmth [in ArchSemArm.VMSA22Arm]
VMSAArm.regs_whitelist [in ArchSemArm.VMSA22Arm]
Library Index
A
ArmInstG
GenAxiomaticArmU
UMArmUMPromising
UMSeqArm
V
VMPromisingVMSA22Arm
VMUMEquivThm
Lemma Index
A
AxArmNames.T_f_in_T [in ArchSemArm.GenAxiomaticArm]C
child_lvl_add_one [in ArchSemArm.VMPromising]P
parent_lvl_sub_one [in ArchSemArm.VMPromising]T
trf_empty [in ArchSemArm.VMUMEquivThm]U
UM_to_VM_speculative [in ArchSemArm.VMUMEquivThm]UM_to_VMSA_bob [in ArchSemArm.VMUMEquivThm]
UM_to_VMSA_dob [in ArchSemArm.VMUMEquivThm]
UM_VMSA_aob [in ArchSemArm.VMUMEquivThm]
UM_VMSA_obs [in ArchSemArm.VMUMEquivThm]
V
VMSA_UM_ob [in ArchSemArm.VMUMEquivThm]VMSA_UM_ob1 [in ArchSemArm.VMUMEquivThm]
VMSA_obETS_empty [in ArchSemArm.VMUMEquivThm]
VMSA_obfault_empty [in ArchSemArm.VMUMEquivThm]
VMSA_Fault_T_empty [in ArchSemArm.VMUMEquivThm]
VMSA_ctxob_simpl [in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_empty [in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_translate_empty [in ArchSemArm.VMUMEquivThm]
VMSA_TLBIS2_empty [in ArchSemArm.VMUMEquivThm]
VMSA_TLBIS1_empty [in ArchSemArm.VMUMEquivThm]
VMSA_tob_empty [in ArchSemArm.VMUMEquivThm]
VMUM_phase1 [in ArchSemArm.VMUMEquivThm]
Constructor Index
B
BBM.Lax [in ArchSemArm.VMPromising]BBM.Off [in ArchSemArm.VMPromising]
BBM.Strict [in ArchSemArm.VMPromising]
E
Ev.Msg [in ArchSemArm.VMPromising]Ev.Tlbi [in ArchSemArm.VMPromising]
L
LEv.Cse [in ArchSemArm.VMPromising]LEv.Wsreg [in ArchSemArm.VMPromising]
T
TLBI_ak_ipa [in ArchSemArm.VMSA22Arm]TLBI_ak_va [in ArchSemArm.VMSA22Arm]
TLBI_ak_no [in ArchSemArm.VMSA22Arm]
TLBI_ak_unsupported [in ArchSemArm.VMSA22Arm]
TLBI.All [in ArchSemArm.VMPromising]
TLBI.Asid [in ArchSemArm.VMPromising]
TLBI.Va [in ArchSemArm.VMPromising]
TLBI.Vaa [in ArchSemArm.VMPromising]
Projection Index
A
atomic [in ArchSemArm.VMSA22Arm]atomic [in ArchSemArm.UMArm]
atomic [in ArchSemArm.UMSeqArm]
AxArmNames.coi_internal [in ArchSemArm.GenAxiomaticArm]
AxArmNames.frfi_internal [in ArchSemArm.GenAxiomaticArm]
AxArmNames.fri_internal [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfi_internal [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfr_internal [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rrf_internal [in ArchSemArm.GenAxiomaticArm]
C
co_contains_TBLI_writes [in ArchSemArm.VMSA22Arm]E
external [in ArchSemArm.VMSA22Arm]external [in ArchSemArm.UMArm]
F
FwdItem.time [in ArchSemArm.UMPromising]FwdItem.view [in ArchSemArm.UMPromising]
FwdItem.xcl_view [in ArchSemArm.UMPromising]
I
IIS.inv_time [in ArchSemArm.VMPromising]IIS.rmw_read [in ArchSemArm.VMPromising]
IIS.rmw_read [in ArchSemArm.UMPromising]
IIS.strict [in ArchSemArm.VMPromising]
IIS.strict [in ArchSemArm.UMPromising]
IIS.TransRes.remaining [in ArchSemArm.VMPromising]
IIS.TransRes.root [in ArchSemArm.VMPromising]
IIS.TransRes.trans_end [in ArchSemArm.VMPromising]
IIS.TransRes.trans_start [in ArchSemArm.VMPromising]
IIS.TransRes.va [in ArchSemArm.VMPromising]
IIS.trs [in ArchSemArm.VMPromising]
initial_reads_not_delayed [in ArchSemArm.VMSA22Arm]
initial_reads [in ArchSemArm.VMSA22Arm]
initial_reads_not_delayed [in ArchSemArm.UMArm]
initial_reads [in ArchSemArm.UMArm]
initial_reads [in ArchSemArm.UMSeqArm]
internal [in ArchSemArm.VMSA22Arm]
internal [in ArchSemArm.UMArm]
is_nms' [in ArchSemArm.VMSA22Arm]
is_nms' [in ArchSemArm.UMArm]
is_nms' [in ArchSemArm.UMSeqArm]
M
memory_events_permitted [in ArchSemArm.VMSA22Arm]memory_events_permitted [in ArchSemArm.UMArm]
memory_events_permitted [in ArchSemArm.UMSeqArm]
Msg.addr [in ArchSemArm.UMPromising]
Msg.size [in ArchSemArm.UMPromising]
Msg.tid [in ArchSemArm.UMPromising]
Msg.val [in ArchSemArm.UMPromising]
N
no_cacheop [in ArchSemArm.VMSA22Arm]no_cacheop [in ArchSemArm.UMArm]
no_exceptions [in ArchSemArm.UMArm]
no_exceptions [in ArchSemArm.UMSeqArm]
R
register_write_permitted [in ArchSemArm.VMSA22Arm]register_write_permitted [in ArchSemArm.UMArm]
register_read_permitted [in ArchSemArm.UMSeqArm]
register_write_permitted [in ArchSemArm.UMSeqArm]
reg_internal' [in ArchSemArm.VMSA22Arm]
reg_internal' [in ArchSemArm.UMArm]
T
TLB.candidate_inv_time [in ArchSemArm.VMPromising]TLB.candidate_end [in ArchSemArm.VMPromising]
TLB.candidate_start [in ArchSemArm.VMPromising]
TLB.candidate_path [in ArchSemArm.VMPromising]
TLB.candidate_ttbr [in ArchSemArm.VMPromising]
TLB.Entry.ptes [in ArchSemArm.VMPromising]
TLB.Entry.val_ttbr [in ArchSemArm.VMPromising]
TLB.NDCtxt.asid [in ArchSemArm.VMPromising]
TLB.NDCtxt.upper [in ArchSemArm.VMPromising]
TLB.NDCtxt.va [in ArchSemArm.VMPromising]
TLB.range_end [in ArchSemArm.VMPromising]
TLB.range_start [in ArchSemArm.VMPromising]
TLB.range_tlb [in ArchSemArm.VMPromising]
TLB.vatlb [in ArchSemArm.VMPromising]
total [in ArchSemArm.UMSeqArm]
translation_internal [in ArchSemArm.VMSA22Arm]
TState.coh [in ArchSemArm.VMPromising]
TState.coh [in ArchSemArm.UMPromising]
TState.fwdb [in ArchSemArm.VMPromising]
TState.fwdb [in ArchSemArm.UMPromising]
TState.levs [in ArchSemArm.VMPromising]
TState.prom [in ArchSemArm.UMPromising]
TState.prom_tlbi [in ArchSemArm.VMPromising]
TState.prom_wr [in ArchSemArm.VMPromising]
TState.regs [in ArchSemArm.VMPromising]
TState.regs [in ArchSemArm.UMPromising]
TState.tcoh [in ArchSemArm.VMPromising]
TState.vacq [in ArchSemArm.VMPromising]
TState.vacq [in ArchSemArm.UMPromising]
TState.vcap [in ArchSemArm.UMPromising]
TState.vcse [in ArchSemArm.VMPromising]
TState.vdmb [in ArchSemArm.VMPromising]
TState.vdmb [in ArchSemArm.UMPromising]
TState.vdmbst [in ArchSemArm.VMPromising]
TState.vdmbst [in ArchSemArm.UMPromising]
TState.vdsb [in ArchSemArm.VMPromising]
TState.visb [in ArchSemArm.UMPromising]
TState.vmsr [in ArchSemArm.VMPromising]
TState.vrd [in ArchSemArm.VMPromising]
TState.vrd [in ArchSemArm.UMPromising]
TState.vrel [in ArchSemArm.VMPromising]
TState.vrel [in ArchSemArm.UMPromising]
TState.vspec [in ArchSemArm.VMPromising]
TState.vtlbi_other [in ArchSemArm.VMPromising]
TState.vtlbi_self [in ArchSemArm.VMPromising]
TState.vwr [in ArchSemArm.VMPromising]
TState.vwr [in ArchSemArm.UMPromising]
TState.xclb [in ArchSemArm.VMPromising]
TState.xclb [in ArchSemArm.UMPromising]
W
WSReg.sreg [in ArchSemArm.VMPromising]WSReg.val [in ArchSemArm.VMPromising]
WSReg.view [in ArchSemArm.VMPromising]
X
XclItem.addr [in ArchSemArm.UMPromising]XclItem.size [in ArchSemArm.UMPromising]
XclItem.time [in ArchSemArm.UMPromising]
XclItem.view [in ArchSemArm.UMPromising]
Inductive Index
B
BBM.param [in ArchSemArm.VMPromising]E
Ev.t [in ArchSemArm.VMPromising]L
LEv.t [in ArchSemArm.VMPromising]T
TLBI_addr_kind [in ArchSemArm.VMSA22Arm]TLBI.t [in ArchSemArm.VMPromising]
Instance Index
A
AxArmNames.exp_internal_dec [in ArchSemArm.GenAxiomaticArm]AxArmNames.is_translation_read_fault_dec [in ArchSemArm.GenAxiomaticArm]
AxArmNames.reg_internal_dec [in ArchSemArm.GenAxiomaticArm]
C
consistent_ok_dec [in ArchSemArm.VMSA22Arm]consistent_dec [in ArchSemArm.VMSA22Arm]
consistent_ok_dec [in ArchSemArm.UMArm]
consistent_dec [in ArchSemArm.UMArm]
consistent_ok_dec [in ArchSemArm.UMSeqArm]
consistent_dec [in ArchSemArm.UMSeqArm]
ContextChange_obv_false [in ArchSemArm.VMUMEquivThm]
C_obv_false [in ArchSemArm.VMUMEquivThm]
D
Decision_has_bbm_violation [in ArchSemArm.VMPromising]Decision_mem_contents_eq [in ArchSemArm.VMPromising]
Decision_is_addr_from_oa [in ArchSemArm.VMPromising]
Decision_allow_write [in ArchSemArm.VMPromising]
Decision_is_global [in ArchSemArm.VMPromising]
Decision_is_tlb_fillable [in ArchSemArm.VMPromising]
Decision_is_accessible_final [in ArchSemArm.VMPromising]
Decision_has_access_flag [in ArchSemArm.VMPromising]
Decision_is_final [in ArchSemArm.VMPromising]
Decision_is_block [in ArchSemArm.VMPromising]
Decision_is_table [in ArchSemArm.VMPromising]
Decision_is_valid [in ArchSemArm.VMPromising]
Decision_match_prefix_at [in ArchSemArm.VMPromising]
Decision_va_in_range [in ArchSemArm.VMPromising]
Decision_is_reg_unknown [in ArchSemArm.VMPromising]
E
ERET_obv_false [in ArchSemArm.VMUMEquivThm]Ev.dec [in ArchSemArm.VMPromising]
Ev.Decision_addr_overlap [in ArchSemArm.VMPromising]
I
IIS.eta [in ArchSemArm.UMPromising]is_faultP_dec [in ArchSemArm.VMSA22Arm]
is_illegal_reg_write_dec [in ArchSemArm.VMSA22Arm]
is_illegal_reg_write_dec [in ArchSemArm.UMArm]
is_illegal_reg_read_dec [in ArchSemArm.UMSeqArm]
is_illegal_reg_write_dec [in ArchSemArm.UMSeqArm]
M
Memory.exclusive_dec [in ArchSemArm.VMPromising]Memory.exclusive_dec [in ArchSemArm.UMPromising]
Msg.eq_dec [in ArchSemArm.UMPromising]
MSR_obv_false [in ArchSemArm.VMUMEquivThm]
N
not_UB_dec [in ArchSemArm.VMSA22Arm]not_UB_dec [in ArchSemArm.UMArm]
not_UB_dec [in ArchSemArm.UMSeqArm]
T
TE_obv_false [in ArchSemArm.VMUMEquivThm]TLBI_obv_false [in ArchSemArm.VMUMEquivThm]
TLBI.dec [in ArchSemArm.VMPromising]
TLB.Decision_is_te_invalidated_by_tlbi [in ArchSemArm.VMPromising]
TLB.Decision_affects [in ArchSemArm.VMPromising]
TLB.Decision_affects_va [in ArchSemArm.VMPromising]
TLB.Decision_affects_asid [in ArchSemArm.VMPromising]
TLB.Decision_is_active_asid [in ArchSemArm.VMPromising]
TLB.Entry.count [in ArchSemArm.VMPromising]
TLB.Entry.eqdep_dec [in ArchSemArm.VMPromising]
TLB.Entry.eq_dec [in ArchSemArm.VMPromising]
TLB.NDCtxt.count [in ArchSemArm.VMPromising]
TLB.NDCtxt.eqdep_dec [in ArchSemArm.VMPromising]
TLB.NDCtxt.eq_dec [in ArchSemArm.VMPromising]
TLB.VATLB.elements [in ArchSemArm.VMPromising]
TLB.VATLB.empty [in ArchSemArm.VMPromising]
TLB.VATLB.filter [in ArchSemArm.VMPromising]
TLB.VATLB.union [in ArchSemArm.VMPromising]
TLB.VATLB.vatlb_dom [in ArchSemArm.VMPromising]
trfe_obv_false [in ArchSemArm.VMUMEquivThm]
trfi_obv_false [in ArchSemArm.VMUMEquivThm]
trf_obv_false [in ArchSemArm.VMUMEquivThm]
TState.Decision_no_write_promises_until [in ArchSemArm.VMPromising]
TState.Decision_no_promises_until [in ArchSemArm.VMPromising]
TState.Decision_tcohs_before_inv_time [in ArchSemArm.VMPromising]
TState.Decision_no_promises_until [in ArchSemArm.UMPromising]
TState.eta [in ArchSemArm.VMPromising]
TState.eta [in ArchSemArm.UMPromising]
T_f_obv_false [in ArchSemArm.VMUMEquivThm]
V
VMSA_obETS_obv_false [in ArchSemArm.VMUMEquivThm]VMSA_obfault_obv_false [in ArchSemArm.VMUMEquivThm]
VMSA_obtlbi_obv_false [in ArchSemArm.VMUMEquivThm]
VMSA_tob_obv_false [in ArchSemArm.VMUMEquivThm]
W
WSReg.eta [in ArchSemArm.VMPromising]Section Index
A
AxArmNames.ArmNames [in ArchSemArm.GenAxiomaticArm]B
Barriers [in ArchSemArm.GenAxiomaticArm]BBM [in ArchSemArm.VMPromising]
P
Phase1 [in ArchSemArm.VMUMEquivThm]Phase1.NoCacheOp_implies_ob1_equal [in ArchSemArm.VMUMEquivThm]
R
RunOutcome [in ArchSemArm.VMPromising]RunOutcome [in ArchSemArm.UMPromising]
U
UMArm [in ArchSemArm.UMArm]UMSeqArm [in ArchSemArm.UMSeqArm]
V
VMSAArm [in ArchSemArm.VMSA22Arm]VMSAArm.isFault [in ArchSemArm.VMSA22Arm]
Abbreviation Index
A
A [in ArchSemArm.VMUMEquivThm]A [in ArchSemArm.VMSA22Arm]
A [in ArchSemArm.UMArm]
A [in ArchSemArm.UMSeqArm]
addr [in ArchSemArm.VMUMEquivThm]
addr [in ArchSemArm.VMSA22Arm]
addr [in ArchSemArm.UMArm]
addr [in ArchSemArm.UMSeqArm]
amo [in ArchSemArm.VMUMEquivThm]
amo [in ArchSemArm.VMSA22Arm]
amo [in ArchSemArm.UMArm]
amo [in ArchSemArm.UMSeqArm]
AxArmNames.A [in ArchSemArm.GenAxiomaticArm]
AxArmNames.amo [in ArchSemArm.GenAxiomaticArm]
AxArmNames.F [in ArchSemArm.GenAxiomaticArm]
AxArmNames.full_instruction_order [in ArchSemArm.GenAxiomaticArm]
AxArmNames.IF [in ArchSemArm.GenAxiomaticArm]
AxArmNames.iio [in ArchSemArm.GenAxiomaticArm]
AxArmNames.instruction_order [in ArchSemArm.GenAxiomaticArm]
AxArmNames.int [in ArchSemArm.GenAxiomaticArm]
AxArmNames.IR [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ISB [in ArchSemArm.GenAxiomaticArm]
AxArmNames.L [in ArchSemArm.GenAxiomaticArm]
AxArmNames.lxsx [in ArchSemArm.GenAxiomaticArm]
AxArmNames.M [in ArchSemArm.GenAxiomaticArm]
AxArmNames.pe [in ArchSemArm.GenAxiomaticArm]
AxArmNames.Q [in ArchSemArm.GenAxiomaticArm]
AxArmNames.R [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfr [in ArchSemArm.GenAxiomaticArm]
AxArmNames.RR [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rrf [in ArchSemArm.GenAxiomaticArm]
AxArmNames.RW [in ArchSemArm.GenAxiomaticArm]
AxArmNames.Rx [in ArchSemArm.GenAxiomaticArm]
AxArmNames.sca [in ArchSemArm.GenAxiomaticArm]
AxArmNames.si [in ArchSemArm.GenAxiomaticArm]
AxArmNames.T [in ArchSemArm.GenAxiomaticArm]
AxArmNames.W [in ArchSemArm.GenAxiomaticArm]
AxArmNames.Wx [in ArchSemArm.GenAxiomaticArm]
C
C [in ArchSemArm.VMUMEquivThm]C [in ArchSemArm.VMSA22Arm]
C [in ArchSemArm.UMArm]
C [in ArchSemArm.UMSeqArm]
co [in ArchSemArm.VMUMEquivThm]
co [in ArchSemArm.VMSA22Arm]
co [in ArchSemArm.UMArm]
co [in ArchSemArm.UMSeqArm]
coe [in ArchSemArm.VMUMEquivThm]
coe [in ArchSemArm.VMSA22Arm]
coe [in ArchSemArm.UMArm]
coe [in ArchSemArm.UMSeqArm]
coi [in ArchSemArm.VMUMEquivThm]
coi [in ArchSemArm.VMSA22Arm]
coi [in ArchSemArm.UMArm]
coi [in ArchSemArm.UMSeqArm]
ctrl [in ArchSemArm.VMUMEquivThm]
ctrl [in ArchSemArm.VMSA22Arm]
ctrl [in ArchSemArm.UMArm]
ctrl [in ArchSemArm.UMSeqArm]
D
data [in ArchSemArm.VMUMEquivThm]data [in ArchSemArm.VMSA22Arm]
data [in ArchSemArm.UMArm]
data [in ArchSemArm.UMSeqArm]
E
ERET [in ArchSemArm.VMUMEquivThm]ERET [in ArchSemArm.VMSA22Arm]
ERET [in ArchSemArm.UMArm]
ERET [in ArchSemArm.UMSeqArm]
Exp [in ArchSemArm.VMUMEquivThm]
Exp [in ArchSemArm.VMSA22Arm]
Exp [in ArchSemArm.UMArm]
Exp [in ArchSemArm.UMSeqArm]
F
F [in ArchSemArm.VMUMEquivThm]F [in ArchSemArm.VMSA22Arm]
F [in ArchSemArm.UMArm]
F [in ArchSemArm.UMSeqArm]
fr [in ArchSemArm.VMUMEquivThm]
fr [in ArchSemArm.VMSA22Arm]
fr [in ArchSemArm.UMArm]
fr [in ArchSemArm.UMSeqArm]
fre [in ArchSemArm.VMUMEquivThm]
fre [in ArchSemArm.VMSA22Arm]
fre [in ArchSemArm.UMArm]
fre [in ArchSemArm.UMSeqArm]
frf [in ArchSemArm.VMUMEquivThm]
frf [in ArchSemArm.VMSA22Arm]
frf [in ArchSemArm.UMArm]
frf [in ArchSemArm.UMSeqArm]
frfi [in ArchSemArm.VMUMEquivThm]
frfi [in ArchSemArm.VMSA22Arm]
frfi [in ArchSemArm.UMArm]
frfi [in ArchSemArm.UMSeqArm]
fri [in ArchSemArm.VMUMEquivThm]
fri [in ArchSemArm.VMSA22Arm]
fri [in ArchSemArm.UMArm]
fri [in ArchSemArm.UMSeqArm]
full_instruction_order [in ArchSemArm.VMUMEquivThm]
full_instruction_order [in ArchSemArm.VMSA22Arm]
full_instruction_order [in ArchSemArm.UMArm]
full_instruction_order [in ArchSemArm.UMSeqArm]
I
ICDC [in ArchSemArm.VMUMEquivThm]ICDC [in ArchSemArm.VMSA22Arm]
ICDC [in ArchSemArm.UMArm]
ICDC [in ArchSemArm.UMSeqArm]
IF [in ArchSemArm.VMUMEquivThm]
IF [in ArchSemArm.VMSA22Arm]
IF [in ArchSemArm.UMArm]
IF [in ArchSemArm.UMSeqArm]
ifr [in ArchSemArm.VMUMEquivThm]
ifr [in ArchSemArm.VMSA22Arm]
ifr [in ArchSemArm.UMArm]
ifr [in ArchSemArm.UMSeqArm]
ifre [in ArchSemArm.VMUMEquivThm]
ifre [in ArchSemArm.VMSA22Arm]
ifre [in ArchSemArm.UMArm]
ifre [in ArchSemArm.UMSeqArm]
ifri [in ArchSemArm.VMUMEquivThm]
ifri [in ArchSemArm.VMSA22Arm]
ifri [in ArchSemArm.UMArm]
ifri [in ArchSemArm.UMSeqArm]
iio [in ArchSemArm.VMUMEquivThm]
iio [in ArchSemArm.VMSA22Arm]
iio [in ArchSemArm.UMArm]
iio [in ArchSemArm.UMSeqArm]
instruction_order [in ArchSemArm.VMUMEquivThm]
instruction_order [in ArchSemArm.VMSA22Arm]
instruction_order [in ArchSemArm.UMArm]
instruction_order [in ArchSemArm.UMSeqArm]
int [in ArchSemArm.VMUMEquivThm]
int [in ArchSemArm.VMSA22Arm]
int [in ArchSemArm.UMArm]
int [in ArchSemArm.UMSeqArm]
IR [in ArchSemArm.VMUMEquivThm]
IR [in ArchSemArm.VMSA22Arm]
IR [in ArchSemArm.UMArm]
IR [in ArchSemArm.UMSeqArm]
irf [in ArchSemArm.VMUMEquivThm]
irf [in ArchSemArm.VMSA22Arm]
irf [in ArchSemArm.UMArm]
irf [in ArchSemArm.UMSeqArm]
irfe [in ArchSemArm.VMUMEquivThm]
irfe [in ArchSemArm.VMSA22Arm]
irfe [in ArchSemArm.UMArm]
irfe [in ArchSemArm.UMSeqArm]
irfi [in ArchSemArm.VMUMEquivThm]
irfi [in ArchSemArm.VMSA22Arm]
irfi [in ArchSemArm.UMArm]
irfi [in ArchSemArm.UMSeqArm]
ISB [in ArchSemArm.VMUMEquivThm]
ISB [in ArchSemArm.VMSA22Arm]
ISB [in ArchSemArm.UMArm]
ISB [in ArchSemArm.UMSeqArm]
is_fault [in ArchSemArm.VMSA22Arm]
L
L [in ArchSemArm.VMUMEquivThm]L [in ArchSemArm.VMSA22Arm]
L [in ArchSemArm.UMArm]
L [in ArchSemArm.UMSeqArm]
lxsx [in ArchSemArm.VMUMEquivThm]
lxsx [in ArchSemArm.VMSA22Arm]
lxsx [in ArchSemArm.UMArm]
lxsx [in ArchSemArm.UMSeqArm]
M
M [in ArchSemArm.VMUMEquivThm]M [in ArchSemArm.VMSA22Arm]
M [in ArchSemArm.UMArm]
M [in ArchSemArm.UMSeqArm]
MRS [in ArchSemArm.VMUMEquivThm]
MRS [in ArchSemArm.VMSA22Arm]
MRS [in ArchSemArm.UMArm]
MRS [in ArchSemArm.UMSeqArm]
MSR [in ArchSemArm.VMUMEquivThm]
MSR [in ArchSemArm.VMSA22Arm]
MSR [in ArchSemArm.UMArm]
MSR [in ArchSemArm.UMSeqArm]
P
pe [in ArchSemArm.VMUMEquivThm]pe [in ArchSemArm.VMSA22Arm]
pe [in ArchSemArm.UMArm]
pe [in ArchSemArm.UMSeqArm]
po [in ArchSemArm.VMUMEquivThm]
po [in ArchSemArm.VMSA22Arm]
po [in ArchSemArm.UMArm]
po [in ArchSemArm.UMSeqArm]
Q
Q [in ArchSemArm.VMUMEquivThm]Q [in ArchSemArm.VMSA22Arm]
Q [in ArchSemArm.UMArm]
Q [in ArchSemArm.UMSeqArm]
R
R [in ArchSemArm.VMUMEquivThm]R [in ArchSemArm.VMSA22Arm]
R [in ArchSemArm.UMArm]
R [in ArchSemArm.UMSeqArm]
RE [in ArchSemArm.VMUMEquivThm]
RE [in ArchSemArm.VMSA22Arm]
RE [in ArchSemArm.UMArm]
RE [in ArchSemArm.UMSeqArm]
rf [in ArchSemArm.VMUMEquivThm]
rf [in ArchSemArm.VMSA22Arm]
rf [in ArchSemArm.UMArm]
rf [in ArchSemArm.UMSeqArm]
rfe [in ArchSemArm.VMUMEquivThm]
rfe [in ArchSemArm.VMSA22Arm]
rfe [in ArchSemArm.UMArm]
rfe [in ArchSemArm.UMSeqArm]
rfi [in ArchSemArm.VMUMEquivThm]
rfi [in ArchSemArm.VMSA22Arm]
rfi [in ArchSemArm.UMArm]
rfi [in ArchSemArm.UMSeqArm]
rfr [in ArchSemArm.VMUMEquivThm]
rfr [in ArchSemArm.VMSA22Arm]
rfr [in ArchSemArm.UMArm]
rfr [in ArchSemArm.UMSeqArm]
rmw [in ArchSemArm.VMUMEquivThm]
rmw [in ArchSemArm.VMSA22Arm]
rmw [in ArchSemArm.UMArm]
rmw [in ArchSemArm.UMSeqArm]
RR [in ArchSemArm.VMUMEquivThm]
RR [in ArchSemArm.VMSA22Arm]
RR [in ArchSemArm.UMArm]
RR [in ArchSemArm.UMSeqArm]
rrf [in ArchSemArm.VMUMEquivThm]
rrf [in ArchSemArm.VMSA22Arm]
rrf [in ArchSemArm.UMArm]
rrf [in ArchSemArm.UMSeqArm]
RW [in ArchSemArm.VMUMEquivThm]
RW [in ArchSemArm.VMSA22Arm]
RW [in ArchSemArm.UMArm]
RW [in ArchSemArm.UMSeqArm]
Rx [in ArchSemArm.VMUMEquivThm]
Rx [in ArchSemArm.VMSA22Arm]
Rx [in ArchSemArm.UMArm]
Rx [in ArchSemArm.UMSeqArm]
S
sca [in ArchSemArm.VMUMEquivThm]sca [in ArchSemArm.VMSA22Arm]
sca [in ArchSemArm.UMArm]
sca [in ArchSemArm.UMSeqArm]
si [in ArchSemArm.VMUMEquivThm]
si [in ArchSemArm.VMSA22Arm]
si [in ArchSemArm.UMArm]
si [in ArchSemArm.UMSeqArm]
T
T [in ArchSemArm.VMUMEquivThm]T [in ArchSemArm.VMSA22Arm]
T [in ArchSemArm.UMArm]
T [in ArchSemArm.UMSeqArm]
TE [in ArchSemArm.VMUMEquivThm]
TE [in ArchSemArm.VMSA22Arm]
TE [in ArchSemArm.UMArm]
TE [in ArchSemArm.UMSeqArm]
tfr [in ArchSemArm.VMUMEquivThm]
tfr [in ArchSemArm.VMSA22Arm]
tfr [in ArchSemArm.UMArm]
tfr [in ArchSemArm.UMSeqArm]
tfre [in ArchSemArm.VMUMEquivThm]
tfre [in ArchSemArm.VMSA22Arm]
tfre [in ArchSemArm.UMArm]
tfre [in ArchSemArm.UMSeqArm]
tfri [in ArchSemArm.VMUMEquivThm]
tfri [in ArchSemArm.VMSA22Arm]
tfri [in ArchSemArm.UMArm]
tfri [in ArchSemArm.UMSeqArm]
TLBI [in ArchSemArm.VMUMEquivThm]
TLBI [in ArchSemArm.VMSA22Arm]
TLBI [in ArchSemArm.UMArm]
TLBI [in ArchSemArm.UMSeqArm]
trf [in ArchSemArm.VMUMEquivThm]
trf [in ArchSemArm.VMSA22Arm]
trf [in ArchSemArm.UMArm]
trf [in ArchSemArm.UMSeqArm]
trfe [in ArchSemArm.VMUMEquivThm]
trfe [in ArchSemArm.VMSA22Arm]
trfe [in ArchSemArm.UMArm]
trfe [in ArchSemArm.UMSeqArm]
trfi [in ArchSemArm.VMUMEquivThm]
trfi [in ArchSemArm.VMSA22Arm]
trfi [in ArchSemArm.UMArm]
trfi [in ArchSemArm.UMSeqArm]
T_f [in ArchSemArm.VMUMEquivThm]
T_f [in ArchSemArm.VMSA22Arm]
W
W [in ArchSemArm.VMUMEquivThm]W [in ArchSemArm.VMSA22Arm]
W [in ArchSemArm.UMArm]
W [in ArchSemArm.UMSeqArm]
Wx [in ArchSemArm.VMUMEquivThm]
Wx [in ArchSemArm.VMSA22Arm]
Wx [in ArchSemArm.UMArm]
Wx [in ArchSemArm.UMSeqArm]
Record Index
A
AxArmNames.exp_internal [in ArchSemArm.GenAxiomaticArm]AxArmNames.reg_internal [in ArchSemArm.GenAxiomaticArm]
C
consistent [in ArchSemArm.VMSA22Arm]consistent [in ArchSemArm.UMArm]
consistent [in ArchSemArm.UMSeqArm]
F
FwdItem.t [in ArchSemArm.UMPromising]I
IIS.t [in ArchSemArm.VMPromising]IIS.t [in ArchSemArm.UMPromising]
IIS.TransRes.t [in ArchSemArm.VMPromising]
M
Msg.t [in ArchSemArm.UMPromising]N
not_UB [in ArchSemArm.VMSA22Arm]not_UB [in ArchSemArm.UMArm]
not_UB [in ArchSemArm.UMSeqArm]
T
TLB.Entry.t [in ArchSemArm.VMPromising]TLB.NDCtxt.t [in ArchSemArm.VMPromising]
TLB.snapshot_range [in ArchSemArm.VMPromising]
TLB.t [in ArchSemArm.VMPromising]
TLB.trans_candidate [in ArchSemArm.VMPromising]
TState.t [in ArchSemArm.VMPromising]
TState.t [in ArchSemArm.UMPromising]
W
WSReg.t [in ArchSemArm.VMPromising]X
XclItem.t [in ArchSemArm.UMPromising]Definition Index
A
allow_write [in ArchSemArm.VMPromising]aob [in ArchSemArm.VMSA22Arm]
aob [in ArchSemArm.UMArm]
ArchExtra.pc_reg [in ArchSemArm.ArmInst]
ArchExtra.reg_type_to_gen [in ArchSemArm.ArmInst]
ArchExtra.reg_type_of_gen [in ArchSemArm.ArmInst]
ArchExtra.reg_of_string [in ArchSemArm.ArmInst]
archmodel [in ArchSemArm.VMSA22Arm]
archmodel [in ArchSemArm.UMArm]
archmodel [in ArchSemArm.UMSeqArm]
asid_ttbr [in ArchSemArm.VMPromising]
asid_ttbr_of_root_ttbr [in ArchSemArm.VMPromising]
attr_idx [in ArchSemArm.VMPromising]
AxArmNames.C [in ArchSemArm.GenAxiomaticArm]
AxArmNames.co [in ArchSemArm.GenAxiomaticArm]
AxArmNames.coe [in ArchSemArm.GenAxiomaticArm]
AxArmNames.coi [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ERET [in ArchSemArm.GenAxiomaticArm]
AxArmNames.Exp [in ArchSemArm.GenAxiomaticArm]
AxArmNames.fr [in ArchSemArm.GenAxiomaticArm]
AxArmNames.fre [in ArchSemArm.GenAxiomaticArm]
AxArmNames.frf [in ArchSemArm.GenAxiomaticArm]
AxArmNames.frfi [in ArchSemArm.GenAxiomaticArm]
AxArmNames.fri [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ICDC [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifr [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifre [in ArchSemArm.GenAxiomaticArm]
AxArmNames.ifri [in ArchSemArm.GenAxiomaticArm]
AxArmNames.irf [in ArchSemArm.GenAxiomaticArm]
AxArmNames.irfe [in ArchSemArm.GenAxiomaticArm]
AxArmNames.irfi [in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_translation_read_fault [in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_mrs [in ArchSemArm.GenAxiomaticArm]
AxArmNames.is_msr [in ArchSemArm.GenAxiomaticArm]
AxArmNames.MRS [in ArchSemArm.GenAxiomaticArm]
AxArmNames.MSR [in ArchSemArm.GenAxiomaticArm]
AxArmNames.po [in ArchSemArm.GenAxiomaticArm]
AxArmNames.RE [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rf [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfe [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rfi [in ArchSemArm.GenAxiomaticArm]
AxArmNames.rmw [in ArchSemArm.GenAxiomaticArm]
AxArmNames.TE [in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfr [in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfre [in ArchSemArm.GenAxiomaticArm]
AxArmNames.tfri [in ArchSemArm.GenAxiomaticArm]
AxArmNames.TLBI [in ArchSemArm.GenAxiomaticArm]
AxArmNames.trf [in ArchSemArm.GenAxiomaticArm]
AxArmNames.trfe [in ArchSemArm.GenAxiomaticArm]
AxArmNames.trfi [in ArchSemArm.GenAxiomaticArm]
AxArmNames.T_f [in ArchSemArm.GenAxiomaticArm]
axmodel [in ArchSemArm.VMSA22Arm]
axmodel [in ArchSemArm.UMArm]
axmodel [in ArchSemArm.UMSeqArm]
B
BBM.check [in ArchSemArm.VMPromising]BBM.param_sind [in ArchSemArm.VMPromising]
BBM.param_rec [in ArchSemArm.VMPromising]
BBM.param_ind [in ArchSemArm.VMPromising]
BBM.param_rect [in ArchSemArm.VMPromising]
bob [in ArchSemArm.VMSA22Arm]
bob [in ArchSemArm.UMArm]
C
check_bbm_violation [in ArchSemArm.VMPromising]child_lvl [in ArchSemArm.VMPromising]
consistent_ok [in ArchSemArm.VMSA22Arm]
consistent_ok [in ArchSemArm.UMArm]
consistent_ok [in ArchSemArm.UMSeqArm]
ContextChange [in ArchSemArm.VMSA22Arm]
CSE [in ArchSemArm.VMSA22Arm]
ctxob [in ArchSemArm.VMSA22Arm]
D
dmb [in ArchSemArm.GenAxiomaticArm]dmbld [in ArchSemArm.GenAxiomaticArm]
dmbnsh [in ArchSemArm.GenAxiomaticArm]
dmbnshld [in ArchSemArm.GenAxiomaticArm]
dmbnshst [in ArchSemArm.GenAxiomaticArm]
dmbnshsy [in ArchSemArm.GenAxiomaticArm]
dmbst [in ArchSemArm.GenAxiomaticArm]
dmbsy [in ArchSemArm.GenAxiomaticArm]
dmb_store [in ArchSemArm.GenAxiomaticArm]
dmb_load [in ArchSemArm.GenAxiomaticArm]
dmb_full [in ArchSemArm.GenAxiomaticArm]
dob [in ArchSemArm.VMSA22Arm]
dob [in ArchSemArm.UMArm]
dsb [in ArchSemArm.GenAxiomaticArm]
dsbld [in ArchSemArm.GenAxiomaticArm]
dsbnsh [in ArchSemArm.GenAxiomaticArm]
dsbnshld [in ArchSemArm.GenAxiomaticArm]
dsbnshst [in ArchSemArm.GenAxiomaticArm]
dsbnshsy [in ArchSemArm.GenAxiomaticArm]
dsbst [in ArchSemArm.GenAxiomaticArm]
dsbsy [in ArchSemArm.GenAxiomaticArm]
dsb_store [in ArchSemArm.GenAxiomaticArm]
dsb_load [in ArchSemArm.GenAxiomaticArm]
dsb_full [in ArchSemArm.GenAxiomaticArm]
E
EL [in ArchSemArm.VMPromising]ELp [in ArchSemArm.VMPromising]
ELp_to_EL [in ArchSemArm.VMPromising]
emit_promise' [in ArchSemArm.VMPromising]
ets2 [in ArchSemArm.VMPromising]
ets3 [in ArchSemArm.VMPromising]
Ev.addr_overlap [in ArchSemArm.VMPromising]
Ev.get_tlbi_recipient [in ArchSemArm.VMPromising]
Ev.get_tlbi [in ArchSemArm.VMPromising]
Ev.get_msg [in ArchSemArm.VMPromising]
Ev.tid [in ArchSemArm.VMPromising]
Ev.t_sind [in ArchSemArm.VMPromising]
Ev.t_rec [in ArchSemArm.VMPromising]
Ev.t_ind [in ArchSemArm.VMPromising]
Ev.t_rect [in ArchSemArm.VMPromising]
F
Fault [in ArchSemArm.VMSA22Arm]FaultFromAquireR [in ArchSemArm.VMSA22Arm]
FaultFromR [in ArchSemArm.VMSA22Arm]
FaultFromReleaseW [in ArchSemArm.VMSA22Arm]
FaultFromW [in ArchSemArm.VMSA22Arm]
Fault_P [in ArchSemArm.VMSA22Arm]
Fault_T [in ArchSemArm.VMSA22Arm]
filter_tlbi_promises [in ArchSemArm.VMPromising]
find_latest_snapshot_before [in ArchSemArm.VMPromising]
FwdItem.init [in ArchSemArm.UMPromising]
FwdItem.read_fwd_view [in ArchSemArm.UMPromising]
G
get_ipa_page [in ArchSemArm.VMSA22Arm]get_va_page [in ArchSemArm.VMSA22Arm]
get_TLBI_addr_kind [in ArchSemArm.VMSA22Arm]
get_asid [in ArchSemArm.VMSA22Arm]
get_vmid [in ArchSemArm.VMSA22Arm]
get_translation_start [in ArchSemArm.VMSA22Arm]
H
has_bbm_violation [in ArchSemArm.VMPromising]has_access_flag [in ArchSemArm.VMPromising]
has_tlbi_shareability [in ArchSemArm.VMSA22Arm]
has_tlbi_regime [in ArchSemArm.VMSA22Arm]
has_tlbi_op [in ArchSemArm.VMSA22Arm]
higher_level [in ArchSemArm.VMPromising]
I
IIS.add [in ArchSemArm.VMPromising]IIS.add [in ArchSemArm.UMPromising]
IIS.init [in ArchSemArm.VMPromising]
IIS.init [in ArchSemArm.UMPromising]
IIS.set_inv_time [in ArchSemArm.VMPromising]
IIS.set_trs [in ArchSemArm.VMPromising]
IIS.TransRes.pop [in ArchSemArm.VMPromising]
Illegal_RW [in ArchSemArm.VMSA22Arm]
Illegal_RW [in ArchSemArm.UMArm]
Illegal_RR [in ArchSemArm.UMSeqArm]
Illegal_RW [in ArchSemArm.UMSeqArm]
index_to_offset [in ArchSemArm.VMPromising]
ipa_page_overlap [in ArchSemArm.VMSA22Arm]
isb [in ArchSemArm.GenAxiomaticArm]
is_dmbnshT [in ArchSemArm.GenAxiomaticArm]
is_dmbnsh [in ArchSemArm.GenAxiomaticArm]
is_dmbnshP [in ArchSemArm.GenAxiomaticArm]
is_dmbT [in ArchSemArm.GenAxiomaticArm]
is_dmb [in ArchSemArm.GenAxiomaticArm]
is_dmbP [in ArchSemArm.GenAxiomaticArm]
is_dsbnshT [in ArchSemArm.GenAxiomaticArm]
is_dsbnsh [in ArchSemArm.GenAxiomaticArm]
is_dsbnshP [in ArchSemArm.GenAxiomaticArm]
is_dsbT [in ArchSemArm.GenAxiomaticArm]
is_dsb [in ArchSemArm.GenAxiomaticArm]
is_dsbP [in ArchSemArm.GenAxiomaticArm]
is_isb [in ArchSemArm.GenAxiomaticArm]
is_bbm_violation [in ArchSemArm.VMPromising]
is_addr_from_oa [in ArchSemArm.VMPromising]
is_mmu_enabled [in ArchSemArm.VMPromising]
is_contiguous [in ArchSemArm.VMPromising]
is_non_global [in ArchSemArm.VMPromising]
is_global [in ArchSemArm.VMPromising]
is_tlb_fillable [in ArchSemArm.VMPromising]
is_accessible_final [in ArchSemArm.VMPromising]
is_final [in ArchSemArm.VMPromising]
is_block [in ArchSemArm.VMPromising]
is_table [in ArchSemArm.VMPromising]
is_valid [in ArchSemArm.VMPromising]
is_upper_va [in ArchSemArm.VMPromising]
is_reg_unknown [in ArchSemArm.VMPromising]
is_faultP_spec [in ArchSemArm.VMSA22Arm]
is_faultP [in ArchSemArm.VMSA22Arm]
is_tlbi_shareability [in ArchSemArm.VMSA22Arm]
is_tlbi_regime [in ArchSemArm.VMSA22Arm]
is_tlbi_op [in ArchSemArm.VMSA22Arm]
is_illegal_reg_write [in ArchSemArm.VMSA22Arm]
is_illegal_reg_write [in ArchSemArm.UMArm]
is_illegal_reg_read [in ArchSemArm.UMSeqArm]
is_illegal_reg_write [in ArchSemArm.UMSeqArm]
L
leaf_lvl [in ArchSemArm.VMPromising]Level [in ArchSemArm.VMPromising]
level_index [in ArchSemArm.VMPromising]
level_prefix [in ArchSemArm.VMPromising]
level_length [in ArchSemArm.VMPromising]
LEv.get_wsreg [in ArchSemArm.VMPromising]
LEv.get_cse [in ArchSemArm.VMPromising]
LEv.t_sind [in ArchSemArm.VMPromising]
LEv.t_rec [in ArchSemArm.VMPromising]
LEv.t_ind [in ArchSemArm.VMPromising]
LEv.t_rect [in ArchSemArm.VMPromising]
M
match_prefix_at [in ArchSemArm.VMPromising]materialize_tlbi_for_recipient [in ArchSemArm.VMPromising]
maybe_TLB_cached [in ArchSemArm.VMSA22Arm]
Memory.cut_before [in ArchSemArm.VMPromising]
Memory.cut_after [in ArchSemArm.VMPromising]
Memory.cut_before [in ArchSemArm.UMPromising]
Memory.cut_after [in ArchSemArm.UMPromising]
Memory.exclusive [in ArchSemArm.VMPromising]
Memory.exclusive [in ArchSemArm.UMPromising]
Memory.fulfill [in ArchSemArm.VMPromising]
Memory.fulfill [in ArchSemArm.UMPromising]
Memory.promise [in ArchSemArm.VMPromising]
Memory.promise [in ArchSemArm.UMPromising]
Memory.read_word [in ArchSemArm.VMPromising]
Memory.read_byte [in ArchSemArm.VMPromising]
Memory.read_from [in ArchSemArm.VMPromising]
Memory.read_initial [in ArchSemArm.VMPromising]
Memory.read_last [in ArchSemArm.VMPromising]
Memory.read_from [in ArchSemArm.UMPromising]
Memory.read_initial [in ArchSemArm.UMPromising]
Memory.read_last [in ArchSemArm.UMPromising]
Memory.t [in ArchSemArm.VMPromising]
Memory.t [in ArchSemArm.UMPromising]
Memory.to_memMap [in ArchSemArm.VMPromising]
Memory.to_memMap [in ArchSemArm.UMPromising]
mem_contents_eq [in ArchSemArm.VMPromising]
Msg.read_byte [in ArchSemArm.UMPromising]
N
next_entry_addr [in ArchSemArm.VMPromising]NoCHERI.no_cheri [in ArchSemArm.ArmInst]
O
ob [in ArchSemArm.VMSA22Arm]ob [in ArchSemArm.UMArm]
obETS [in ArchSemArm.VMSA22Arm]
obETS2 [in ArchSemArm.VMSA22Arm]
obfault [in ArchSemArm.VMSA22Arm]
obs [in ArchSemArm.VMSA22Arm]
obs [in ArchSemArm.UMArm]
obtlbi [in ArchSemArm.VMSA22Arm]
obtlbi_translate [in ArchSemArm.VMSA22Arm]
ob1 [in ArchSemArm.VMSA22Arm]
ob1 [in ArchSemArm.UMArm]
offset_size [in ArchSemArm.VMPromising]
output_addr [in ArchSemArm.VMPromising]
output_addr_size [in ArchSemArm.VMPromising]
P
page_of_addr [in ArchSemArm.VMSA22Arm]parent_lvl [in ArchSemArm.VMPromising]
prefix [in ArchSemArm.VMPromising]
prefix_to_va [in ArchSemArm.VMPromising]
R
read_fault_vpre [in ArchSemArm.VMPromising]read_pte [in ArchSemArm.VMPromising]
read_mem_explicit [in ArchSemArm.VMPromising]
read_fwd [in ArchSemArm.VMPromising]
read_candidates [in ArchSemArm.VMPromising]
read_imem [in ArchSemArm.VMPromising]
read_mem [in ArchSemArm.UMPromising]
read_fwd [in ArchSemArm.UMPromising]
read_candidates [in ArchSemArm.UMPromising]
read_imem [in ArchSemArm.UMPromising]
regval_to_val [in ArchSemArm.VMPromising]
relaxed_regs [in ArchSemArm.VMPromising]
root_ttbr [in ArchSemArm.VMPromising]
root_lvl [in ArchSemArm.VMPromising]
run_outcome' [in ArchSemArm.VMPromising]
run_outcome [in ArchSemArm.VMPromising]
run_take_exception [in ArchSemArm.VMPromising]
run_trans_end [in ArchSemArm.VMPromising]
run_trans_start [in ArchSemArm.VMPromising]
run_tlbi [in ArchSemArm.VMPromising]
run_barrier [in ArchSemArm.VMPromising]
run_cse [in ArchSemArm.VMPromising]
run_reg_write [in ArchSemArm.VMPromising]
run_reg_read [in ArchSemArm.VMPromising]
run_reg_trans_read [in ArchSemArm.VMPromising]
run_reg_general_read [in ArchSemArm.VMPromising]
run_outcome' [in ArchSemArm.UMPromising]
run_outcome [in ArchSemArm.UMPromising]
S
sail_tiny_arm_sem [in ArchSemArm.ArmInst]same_asid [in ArchSemArm.VMSA22Arm]
same_vmid [in ArchSemArm.VMSA22Arm]
same_translation [in ArchSemArm.VMSA22Arm]
shareability [in ArchSemArm.VMPromising]
speculative [in ArchSemArm.VMSA22Arm]
speculative [in ArchSemArm.UMArm]
Stage1 [in ArchSemArm.VMSA22Arm]
Stage2 [in ArchSemArm.VMSA22Arm]
strict_regs [in ArchSemArm.VMPromising]
T
tlbi_translate_same_ipa_page [in ArchSemArm.VMSA22Arm]tlbi_translate_same_va_page [in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_sind [in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_rec [in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_ind [in ArchSemArm.VMSA22Arm]
TLBI_addr_kind_rect [in ArchSemArm.VMSA22Arm]
tlbi_translate_same_vmid [in ArchSemArm.VMSA22Arm]
tlbi_translate_same_asid [in ArchSemArm.VMSA22Arm]
TLBI_IS [in ArchSemArm.VMSA22Arm]
TLBI_EL2 [in ArchSemArm.VMSA22Arm]
TLBI_EL1 [in ArchSemArm.VMSA22Arm]
TLBI_IPA [in ArchSemArm.VMSA22Arm]
TLBI_VA [in ArchSemArm.VMSA22Arm]
TLBI_VMID [in ArchSemArm.VMSA22Arm]
TLBI_S2 [in ArchSemArm.VMSA22Arm]
TLBI_S1 [in ArchSemArm.VMSA22Arm]
TLBI_ASID [in ArchSemArm.VMSA22Arm]
TLBI.asid [in ArchSemArm.VMPromising]
TLBI.asid_opt [in ArchSemArm.VMPromising]
TLBI.last [in ArchSemArm.VMPromising]
TLBI.last_opt [in ArchSemArm.VMPromising]
TLBI.tid [in ArchSemArm.VMPromising]
TLBI.t_sind [in ArchSemArm.VMPromising]
TLBI.t_rec [in ArchSemArm.VMPromising]
TLBI.t_ind [in ArchSemArm.VMPromising]
TLBI.t_rect [in ArchSemArm.VMPromising]
TLBI.upper_opt [in ArchSemArm.VMPromising]
TLBI.va [in ArchSemArm.VMPromising]
TLBI.va_opt [in ArchSemArm.VMPromising]
tlb_barriered [in ArchSemArm.VMSA22Arm]
tlb_affects [in ArchSemArm.VMSA22Arm]
tlb_might_affect [in ArchSemArm.VMSA22Arm]
TLB.affects [in ArchSemArm.VMPromising]
TLB.affects_va [in ArchSemArm.VMPromising]
TLB.affects_asid [in ArchSemArm.VMPromising]
TLB.apply_tlbi_for_tid [in ArchSemArm.VMPromising]
TLB.Ctxt.asid [in ArchSemArm.VMPromising]
TLB.Ctxt.lvl [in ArchSemArm.VMPromising]
TLB.Ctxt.nd [in ArchSemArm.VMPromising]
TLB.Ctxt.t [in ArchSemArm.VMPromising]
TLB.Ctxt.upper [in ArchSemArm.VMPromising]
TLB.Ctxt.va [in ArchSemArm.VMPromising]
TLB.Entry.append [in ArchSemArm.VMPromising]
TLB.Entry.pte [in ArchSemArm.VMPromising]
TLB.FE.asid [in ArchSemArm.VMPromising]
TLB.FE.ctxt [in ArchSemArm.VMPromising]
TLB.FE.lvl [in ArchSemArm.VMPromising]
TLB.FE.pte [in ArchSemArm.VMPromising]
TLB.FE.ptes [in ArchSemArm.VMPromising]
TLB.FE.t [in ArchSemArm.VMPromising]
TLB.FE.va [in ArchSemArm.VMPromising]
TLB.get_invalid_entries_from_snapshots [in ArchSemArm.VMPromising]
TLB.get_invalid_entries_from_range [in ArchSemArm.VMPromising]
TLB.get_valid_entries_from_snapshots [in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time [in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time_by_lvl [in ArchSemArm.VMPromising]
TLB.get_invalid_ptes_with_inv_time_by_lvl_asid [in ArchSemArm.VMPromising]
TLB.get_leaf_ptes_with_inv_time [in ArchSemArm.VMPromising]
TLB.get_leaf_ptes_with_inv_time_by_ctxt [in ArchSemArm.VMPromising]
TLB.init [in ArchSemArm.VMPromising]
TLB.invalidation_time [in ArchSemArm.VMPromising]
TLB.invalidation_time_from_evs [in ArchSemArm.VMPromising]
TLB.is_te_invalidated_by_tlbi [in ArchSemArm.VMPromising]
TLB.is_upper_ttbr [in ArchSemArm.VMPromising]
TLB.is_active_asid [in ArchSemArm.VMPromising]
TLB.lookup [in ArchSemArm.VMPromising]
TLB.next_va [in ArchSemArm.VMPromising]
TLB.snapshots_from_until [in ArchSemArm.VMPromising]
TLB.snapshots_from [in ArchSemArm.VMPromising]
TLB.tlbi_apply [in ArchSemArm.VMPromising]
TLB.traverse [in ArchSemArm.VMPromising]
TLB.traverse_lvl [in ArchSemArm.VMPromising]
TLB.traverse_root [in ArchSemArm.VMPromising]
TLB.ttbr_asid_roots_at [in ArchSemArm.VMPromising]
TLB.ttbr_asids_at [in ArchSemArm.VMPromising]
TLB.ttbr_values_at [in ArchSemArm.VMPromising]
TLB.unique_snapshots_until [in ArchSemArm.VMPromising]
TLB.unique_snapshots_between [in ArchSemArm.VMPromising]
TLB.unique_snapshots_va [in ArchSemArm.VMPromising]
TLB.unique_snapshots_va_until [in ArchSemArm.VMPromising]
TLB.unique_snapshots_va_between [in ArchSemArm.VMPromising]
TLB.update [in ArchSemArm.VMPromising]
TLB.update_all [in ArchSemArm.VMPromising]
TLB.VATLB.final_entries [in ArchSemArm.VMPromising]
TLB.VATLB.get [in ArchSemArm.VMPromising]
TLB.VATLB.getFE [in ArchSemArm.VMPromising]
TLB.VATLB.init [in ArchSemArm.VMPromising]
TLB.VATLB.insert [in ArchSemArm.VMPromising]
TLB.VATLB.setFEs [in ArchSemArm.VMPromising]
TLB.VATLB.singleton [in ArchSemArm.VMPromising]
TLB.VATLB.t [in ArchSemArm.VMPromising]
TLB.VATLB.T [in ArchSemArm.VMPromising]
TLB.va_fill [in ArchSemArm.VMPromising]
TLB.va_fill_lvl [in ArchSemArm.VMPromising]
TLB.va_fill_root [in ArchSemArm.VMPromising]
tob [in ArchSemArm.VMSA22Arm]
TState.add_wsreg [in ArchSemArm.VMPromising]
TState.clear_xclb [in ArchSemArm.VMPromising]
TState.clear_xclb [in ArchSemArm.UMPromising]
TState.cse [in ArchSemArm.VMPromising]
TState.cse_candidates [in ArchSemArm.VMPromising]
TState.cse_position [in ArchSemArm.VMPromising]
TState.filter_cse [in ArchSemArm.VMPromising]
TState.filter_wsreg [in ArchSemArm.VMPromising]
TState.get_tcoh [in ArchSemArm.VMPromising]
TState.init [in ArchSemArm.VMPromising]
TState.init [in ArchSemArm.UMPromising]
TState.lev_cur [in ArchSemArm.VMPromising]
TState.max_cohs [in ArchSemArm.VMPromising]
TState.min_promise [in ArchSemArm.VMPromising]
TState.no_write_promises_until [in ArchSemArm.VMPromising]
TState.no_promises_until [in ArchSemArm.VMPromising]
TState.no_promises_until [in ArchSemArm.UMPromising]
TState.promise [in ArchSemArm.UMPromising]
TState.promise_tlbi [in ArchSemArm.VMPromising]
TState.promise_write [in ArchSemArm.VMPromising]
TState.read_reg [in ArchSemArm.VMPromising]
TState.read_sreg_at [in ArchSemArm.VMPromising]
TState.read_sreg_indirect [in ArchSemArm.VMPromising]
TState.read_sreg_direct [in ArchSemArm.VMPromising]
TState.read_sreg_by_cse [in ArchSemArm.VMPromising]
TState.read_sreg_last [in ArchSemArm.VMPromising]
TState.reg_map [in ArchSemArm.VMPromising]
TState.reg_map [in ArchSemArm.UMPromising]
TState.set_xclb [in ArchSemArm.VMPromising]
TState.set_fwdbs [in ArchSemArm.VMPromising]
TState.set_fwdb [in ArchSemArm.VMPromising]
TState.set_coh [in ArchSemArm.VMPromising]
TState.set_reg [in ArchSemArm.VMPromising]
TState.set_xclb [in ArchSemArm.UMPromising]
TState.set_fwdbs [in ArchSemArm.UMPromising]
TState.set_fwdb [in ArchSemArm.UMPromising]
TState.set_coh [in ArchSemArm.UMPromising]
TState.set_reg [in ArchSemArm.UMPromising]
TState.tcohs_before_inv_time [in ArchSemArm.VMPromising]
TState.update [in ArchSemArm.VMPromising]
TState.update [in ArchSemArm.UMPromising]
TState.update_tcohs [in ArchSemArm.VMPromising]
TState.update_tcoh [in ArchSemArm.VMPromising]
TState.update_cohs [in ArchSemArm.VMPromising]
TState.update_coh [in ArchSemArm.VMPromising]
TState.update_cohs [in ArchSemArm.UMPromising]
TState.update_coh [in ArchSemArm.UMPromising]
TState.update2 [in ArchSemArm.VMPromising]
TState.update2 [in ArchSemArm.UMPromising]
TState.va_page_offsets [in ArchSemArm.VMPromising]
ttbrs [in ArchSemArm.VMPromising]
U
UMPromising [in ArchSemArm.UMPromising]UMPromising_opmodel_pf [in ArchSemArm.UMPromising]
UMPromising_opmodel [in ArchSemArm.UMPromising]
UMPromising_pf [in ArchSemArm.UMPromising]
UMPromising_exe [in ArchSemArm.UMPromising]
UMPromising_cert [in ArchSemArm.UMPromising]
UMPromising_nocert [in ArchSemArm.UMPromising]
V
valid_eids_compl [in ArchSemArm.VMSA22Arm]valid_eids_rc [in ArchSemArm.VMSA22Arm]
val_to_regval [in ArchSemArm.VMPromising]
val_to_addr [in ArchSemArm.VMPromising]
va_ranges_overlap [in ArchSemArm.VMPromising]
va_to_vpn [in ArchSemArm.VMPromising]
va_in_range [in ArchSemArm.VMPromising]
va_page_overlap [in ArchSemArm.VMSA22Arm]
view [in ArchSemArm.VMPromising]
view [in ArchSemArm.UMPromising]
view_if [in ArchSemArm.VMPromising]
view_if [in ArchSemArm.UMPromising]
VMPromising [in ArchSemArm.VMPromising]
VMPromising_opmodel_pf [in ArchSemArm.VMPromising]
VMPromising_opmodel [in ArchSemArm.VMPromising]
VMPromising_pf [in ArchSemArm.VMPromising]
VMPromising_exe [in ArchSemArm.VMPromising]
VMPromising_cert [in ArchSemArm.VMPromising]
VMPromising_nocert [in ArchSemArm.VMPromising]
W
wco [in ArchSemArm.VMSA22Arm]write_fault_vpre [in ArchSemArm.VMPromising]
write_mem [in ArchSemArm.VMPromising]
write_mem [in ArchSemArm.UMPromising]
WSReg.to_val_view_if [in ArchSemArm.VMPromising]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1076 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (109 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (76 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (11 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (281 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (455 entries) |
This page has been generated by coqdoc