| 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 | (821 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 | (38 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 | (58 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) |
| Axiom 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 | (52 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 | (60 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 | (27 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 | (75 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 | (6 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 | (74 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 | (28 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 | (37 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 | (337 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 | (18 entries) |
Global Index
A
Arch [module, in ArchSem.Interface]ArchExtra [module, in ArchSem.FromSail]
ArchExtra.pc_reg [axiom, in ArchSem.FromSail]
ArchExtra.reg_type_to_gen [axiom, in ArchSem.FromSail]
ArchExtra.reg_type_of_gen [axiom, in ArchSem.FromSail]
ArchExtra.reg_of_string [axiom, in ArchSem.FromSail]
ArchFromSail [module, in ArchSem.FromSail]
ArchFromSailT [module, in ArchSem.FromSail]
ArchFromSail.abort [definition, in ArchSem.FromSail]
ArchFromSail.addr_space_countable [definition, in ArchSem.FromSail]
ArchFromSail.addr_space_eq [definition, in ArchSem.FromSail]
ArchFromSail.addr_space [definition, in ArchSem.FromSail]
ArchFromSail.addr_size [definition, in ArchSem.FromSail]
ArchFromSail.barrier [definition, in ArchSem.FromSail]
ArchFromSail.barrier_eq [definition, in ArchSem.FromSail]
ArchFromSail.cache_op_eq [definition, in ArchSem.FromSail]
ArchFromSail.cache_op [definition, in ArchSem.FromSail]
ArchFromSail.cap_size_log [definition, in ArchSem.FromSail]
ArchFromSail.CHERI [definition, in ArchSem.FromSail]
ArchFromSail.ctrans_reg_type_simpl [instance, in ArchSem.FromSail]
ArchFromSail.ctrans_reg_type [instance, in ArchSem.FromSail]
ArchFromSail.exn [definition, in ArchSem.FromSail]
ArchFromSail.exn_eq [definition, in ArchSem.FromSail]
ArchFromSail.is_atomic_rmw [definition, in ArchSem.FromSail]
ArchFromSail.is_exclusive [definition, in ArchSem.FromSail]
ArchFromSail.is_standalone [definition, in ArchSem.FromSail]
ArchFromSail.is_rel_acq_rcsc [definition, in ArchSem.FromSail]
ArchFromSail.is_rel_acq_rcpc [definition, in ArchSem.FromSail]
ArchFromSail.is_relaxed [definition, in ArchSem.FromSail]
ArchFromSail.is_ttw [definition, in ArchSem.FromSail]
ArchFromSail.is_ifetch [definition, in ArchSem.FromSail]
ArchFromSail.is_explicit [definition, in ArchSem.FromSail]
ArchFromSail.mem_acc_eq [definition, in ArchSem.FromSail]
ArchFromSail.mem_acc [definition, in ArchSem.FromSail]
ArchFromSail.pc_reg [definition, in ArchSem.FromSail]
ArchFromSail.pretty_reg [definition, in ArchSem.FromSail]
ArchFromSail.reg [definition, in ArchSem.FromSail]
ArchFromSail.reg_acc_eq [definition, in ArchSem.FromSail]
ArchFromSail.reg_acc [definition, in ArchSem.FromSail]
ArchFromSail.reg_type_to_gen [definition, in ArchSem.FromSail]
ArchFromSail.reg_type_of_gen [definition, in ArchSem.FromSail]
ArchFromSail.reg_type_eq_dep_dec [instance, in ArchSem.FromSail]
ArchFromSail.reg_type_inhabited [definition, in ArchSem.FromSail]
ArchFromSail.reg_type_countable [definition, in ArchSem.FromSail]
ArchFromSail.reg_type_eq [definition, in ArchSem.FromSail]
ArchFromSail.reg_type [definition, in ArchSem.FromSail]
ArchFromSail.reg_of_string [definition, in ArchSem.FromSail]
ArchFromSail.reg_countable [definition, in ArchSem.FromSail]
ArchFromSail.reg_eq [definition, in ArchSem.FromSail]
ArchFromSail.tlbi [definition, in ArchSem.FromSail]
ArchFromSail.tlbi_eq [definition, in ArchSem.FromSail]
ArchFromSail.trans_end_eq [definition, in ArchSem.FromSail]
ArchFromSail.trans_end [definition, in ArchSem.FromSail]
ArchFromSail.trans_start_eq [definition, in ArchSem.FromSail]
ArchFromSail.trans_start [definition, in ArchSem.FromSail]
ArchInst [module, in ArchSem.ArchInst]
ArchInst [library]
ArchInst.Cand [module, in ArchSem.ArchInst]
ArchInst.GenPro [module, in ArchSem.ArchInst]
ArchInst.Interface [module, in ArchSem.ArchInst]
ArchInst.ISAManip [module, in ArchSem.ArchInst]
ArchInst.SeqModel [module, in ArchSem.ArchInst]
ArchInst.TM [module, in ArchSem.ArchInst]
Arch.abort [axiom, in ArchSem.Interface]
Arch.addr_space_countable [axiom, in ArchSem.Interface]
Arch.addr_space_eq [axiom, in ArchSem.Interface]
Arch.addr_space [axiom, in ArchSem.Interface]
Arch.addr_size [axiom, in ArchSem.Interface]
Arch.barrier [axiom, in ArchSem.Interface]
Arch.barrier_eq [axiom, in ArchSem.Interface]
Arch.cache_op_eq [axiom, in ArchSem.Interface]
Arch.cache_op [axiom, in ArchSem.Interface]
Arch.cap_size_log [axiom, in ArchSem.Interface]
Arch.CHERI [axiom, in ArchSem.Interface]
Arch.ctrans_reg_type_simpl [axiom, in ArchSem.Interface]
Arch.ctrans_reg_type [axiom, in ArchSem.Interface]
Arch.exn [axiom, in ArchSem.Interface]
Arch.exn_eq [axiom, in ArchSem.Interface]
Arch.is_atomic_rmw [axiom, in ArchSem.Interface]
Arch.is_exclusive [axiom, in ArchSem.Interface]
Arch.is_standalone [axiom, in ArchSem.Interface]
Arch.is_rel_acq_rcpc [axiom, in ArchSem.Interface]
Arch.is_rel_acq_rcsc [axiom, in ArchSem.Interface]
Arch.is_relaxed [axiom, in ArchSem.Interface]
Arch.is_ttw [axiom, in ArchSem.Interface]
Arch.is_ifetch [axiom, in ArchSem.Interface]
Arch.is_explicit [axiom, in ArchSem.Interface]
Arch.mem_acc_eq [axiom, in ArchSem.Interface]
Arch.mem_acc [axiom, in ArchSem.Interface]
Arch.pc_reg [axiom, in ArchSem.Interface]
Arch.pretty_reg [axiom, in ArchSem.Interface]
Arch.reg [axiom, in ArchSem.Interface]
Arch.reg_acc_eq [axiom, in ArchSem.Interface]
Arch.reg_acc [axiom, in ArchSem.Interface]
Arch.reg_type_to_gen [axiom, in ArchSem.Interface]
Arch.reg_type_of_gen [axiom, in ArchSem.Interface]
Arch.reg_type_eq_dep_dec [axiom, in ArchSem.Interface]
Arch.reg_type_inhabited [axiom, in ArchSem.Interface]
Arch.reg_type_countable [axiom, in ArchSem.Interface]
Arch.reg_type_eq [axiom, in ArchSem.Interface]
Arch.reg_type [axiom, in ArchSem.Interface]
Arch.reg_of_string [axiom, in ArchSem.Interface]
Arch.reg_countable [axiom, in ArchSem.Interface]
Arch.reg_eq [axiom, in ArchSem.Interface]
Arch.tlbi [axiom, in ArchSem.Interface]
Arch.tlbi_eq [axiom, in ArchSem.Interface]
Arch.trans_end_eq [axiom, in ArchSem.Interface]
Arch.trans_end [axiom, in ArchSem.Interface]
Arch.trans_start_eq [axiom, in ArchSem.Interface]
Arch.trans_start [axiom, in ArchSem.Interface]
B
bitU_finite [instance, in ArchSem.FromSail]C
CandidateExecutions [module, in ArchSem.CandidateExecutions]CandidateExecutions [library]
CandidateExecutions.Ax [module, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Allowed [constructor, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.archres [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Ax [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.axres [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Ax.et [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Ax.flag [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior [inductive, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_sind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_rec [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_ind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_rect [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.cand [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.cand [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_Model [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_is_ok [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_wider' [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_wider [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_weaker [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Flagged [constructor, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.model [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Rejected [constructor, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res [module, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.archres [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.axres [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.cand [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_is_ok [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_wider' [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_wider [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_weaker [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.Res [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.Res.et [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.Res.flag [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.to_archModel [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.weaker [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.wider [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.wider_weaker [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.t [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.t [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.to_archModel_nc [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.weaker [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.weaker_Model [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider_Model [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider_weaker [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate [module, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr_space_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr_space_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr_space_wf [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_update [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_rmw_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_rmw_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.barriers [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.bytes_per_event_NoDup [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.bytes_per_event [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.cacheops [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand.et [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand.nmth [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.cd_to_archState [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.coherence [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.coherence_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.coherence_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.coherence_wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.collect_all [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.convert_to_EID_rel [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_contains_overlapping_writes [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_irreflexive [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_transitive [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ctrl [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.data [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.cd [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.et [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.n [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_event_ids [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_iEvent_NoDup [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_iEvent [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.eta [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.events [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.events' [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_map_match [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_map [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_NoDup [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_NoDup1 [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_match [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exclusive_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exclusive_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_sind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_rec [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_ind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_rect [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type [inductive, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.explicit_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.explicit_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_mem_map [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_write_per_addr [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_reg_map [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_reg_map_tid [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.footprint_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.footprint_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.footprint_wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.from_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.full_instruction_order [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.gather_by_key_None [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.gather_by_key [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.get_addr_footprint [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iEvent_list_match [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iEvent_list [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ifetch_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ifetch_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iio [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iio_addr [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.initial_reg_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init_mem_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init' [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_order [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_list_match [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_list [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match_use [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete_use [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_failed_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_failed [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_rf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_rf [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_mem_read_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_mem_read [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_cdestr [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_spec [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_nms_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_nms [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_sym_iff [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_sym [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_eid_candidate [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_is_Some_gather_by_key [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_total_unfold_gather_by_key [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_unfold_event_map [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_eid_pre [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_iEvent [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_instruction [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_same_pa [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_instruction_order [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_to_writes [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_from_reads [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_footprint_valid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_atomic_rmw [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_exclusive [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_standalone [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_rel_acq_rcpc [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_rel_acq_rcsc [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_relaxed [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_ttw [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_ifetch [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_explicit [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_by_kind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_events_union [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_events [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_reqs_union [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_aborts [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_reqs [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_addr_announces [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_reqs_union [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_aborts [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_reqs [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.MS [constructor, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.NMS [constructor, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_po_loc [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_po [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_gen [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.overlapping [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.overlapping_sym [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_reads_from [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.possible_initial_reg_reads_ok [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.possible_initial_reg_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre_exec [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre_eta [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind [section, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind.P [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind.Pdec [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.et [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.nmth [variable, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_by_kind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf' [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_footprint_valid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_data [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_from_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.relaxed_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.relaxed_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcpc_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcpc_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcsc_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcsc_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_valid_initial [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_valid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_functional [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_to_reads [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_from_writes [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_reg_reads_decomp [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_same_reg [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_irreflexive [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_initial_valid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_same_reg_val [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_functional [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_to_reads [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_from_writes [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg_val_same_reg [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg_val [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_mem_value_size [lemma, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_mem_value [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_footprint [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_size [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_addr [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_access [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_instruction_instance [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_thread [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_key [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_instruction_order [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_iio [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_access [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_instruction_instance [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_thread [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_key [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_gather_by_key_lookup [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_valid_eids [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_collect_all [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_unfold_elem_of_event_list [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.standalone_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.standalone_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.t [abbreviation, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.t [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.tlbis [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ttw_writes [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ttw_reads [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.UnfoldEidRels [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.unsupported_event [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.valid_eids [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.wf [record, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.wf_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.writes_by_kind [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.EID [module, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.byte [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.cdestr_rec_inj [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.countable [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.eq_dec [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.eta [instance, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.full_po_lt [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.ieid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.iid [projection, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.iio_lt [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.po_lt [definition, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.t [record, in ArchSem.CandidateExecutions]
CandidateExecutions.EID.tid [projection, in ArchSem.CandidateExecutions]
_ <â‚šâ‚Šáµ¢ _ (eid_scope) [notation, in ArchSem.CandidateExecutions]
_ <áµ¢ _ (eid_scope) [notation, in ArchSem.CandidateExecutions]
_ <â‚š _ (eid_scope) [notation, in ArchSem.CandidateExecutions]
F
FromSail [library]G
GenPromising [module, in ArchSem.GenPromising]GenPromising [library]
GenPromisingT [module, in ArchSem.GenPromising]
GenPromising.CPState [module, in ArchSem.GenPromising]
GenPromising.CPState.cpromise_tid [definition, in ArchSem.GenPromising]
GenPromising.CPState.CPS [section, in ArchSem.GenPromising]
GenPromising.CPState.CPS.isem [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.mEvent_eq_dec [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.n [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.prom [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps [section, in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult [section, in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult.initmem [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult.tid [variable, in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.term [variable, in ArchSem.GenPromising]
GenPromising.CPState.enumerate_results [definition, in ArchSem.GenPromising]
GenPromising.CPState.EnumerationResult [record, in ArchSem.GenPromising]
GenPromising.CPState.errors [projection, in ArchSem.GenPromising]
GenPromising.CPState.final [definition, in ArchSem.GenPromising]
GenPromising.CPState.final_states [projection, in ArchSem.GenPromising]
GenPromising.CPState.iis [abbreviation, in ArchSem.GenPromising]
GenPromising.CPState.make_final [definition, in ArchSem.GenPromising]
GenPromising.CPState.mEvent [abbreviation, in ArchSem.GenPromising]
GenPromising.CPState.opmodel [definition, in ArchSem.GenPromising]
GenPromising.CPState.opmodel_pf [definition, in ArchSem.GenPromising]
GenPromising.CPState.out_of_fuel [projection, in ArchSem.GenPromising]
GenPromising.CPState.promises [projection, in ArchSem.GenPromising]
GenPromising.CPState.promise_select_tid [definition, in ArchSem.GenPromising]
GenPromising.CPState.run_transition_promise_first [definition, in ArchSem.GenPromising]
GenPromising.CPState.run_transition [definition, in ArchSem.GenPromising]
GenPromising.CPState.run_step [definition, in ArchSem.GenPromising]
GenPromising.CPState.run_to_termination [definition, in ArchSem.GenPromising]
GenPromising.CPState.run_outcome_with_promise [definition, in ArchSem.GenPromising]
GenPromising.CPState.t [abbreviation, in ArchSem.GenPromising]
GenPromising.CPState.to_final_archState [definition, in ArchSem.GenPromising]
GenPromising.CPState.tState [abbreviation, in ArchSem.GenPromising]
GenPromising.CPState.validate_final [definition, in ArchSem.GenPromising]
GenPromising.Promising [module, in ArchSem.GenPromising]
GenPromising.Promising_to_Modelc_pf [definition, in ArchSem.GenPromising]
GenPromising.Promising_to_Modelc [definition, in ArchSem.GenPromising]
GenPromising.Promising_to_Modelnc [definition, in ArchSem.GenPromising]
GenPromising.Promising.address_space [projection, in ArchSem.GenPromising]
GenPromising.Promising.check_valid_end [projection, in ArchSem.GenPromising]
GenPromising.Promising.emit_promise [projection, in ArchSem.GenPromising]
GenPromising.Promising.filter_promises [projection, in ArchSem.GenPromising]
GenPromising.Promising.handle_outcome [projection, in ArchSem.GenPromising]
GenPromising.Promising.iis [projection, in ArchSem.GenPromising]
GenPromising.Promising.iis_init [projection, in ArchSem.GenPromising]
GenPromising.Promising.memory_snapshot [projection, in ArchSem.GenPromising]
GenPromising.Promising.mEvent [projection, in ArchSem.GenPromising]
GenPromising.Promising.mEvent_tid [projection, in ArchSem.GenPromising]
GenPromising.Promising.mEvent_eq_dec [projection, in ArchSem.GenPromising]
GenPromising.Promising.Model [record, in ArchSem.GenPromising]
GenPromising.Promising.tState [projection, in ArchSem.GenPromising]
GenPromising.Promising.tState_nopromises [projection, in ArchSem.GenPromising]
GenPromising.Promising.tState_regs [projection, in ArchSem.GenPromising]
GenPromising.Promising.tState_init [projection, in ArchSem.GenPromising]
GenPromising.PState [module, in ArchSem.GenPromising]
GenPromising.PState.allowed_promises_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.check_valid_end [definition, in ArchSem.GenPromising]
GenPromising.PState.check_valid_end_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.events [projection, in ArchSem.GenPromising]
GenPromising.PState.from_archState [definition, in ArchSem.GenPromising]
GenPromising.PState.initmem [projection, in ArchSem.GenPromising]
GenPromising.PState.mEvent [abbreviation, in ArchSem.GenPromising]
GenPromising.PState.nopromises [definition, in ArchSem.GenPromising]
GenPromising.PState.nopromises_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.promise_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.PS [section, in ArchSem.GenPromising]
GenPromising.PState.PSProm [section, in ArchSem.GenPromising]
GenPromising.PState.PSProm.isem [variable, in ArchSem.GenPromising]
GenPromising.PState.PSProm.n [variable, in ArchSem.GenPromising]
GenPromising.PState.PSProm.prom [variable, in ArchSem.GenPromising]
GenPromising.PState.PState_PPState_set [instance, in ArchSem.GenPromising]
GenPromising.PState.PState_PPState [definition, in ArchSem.GenPromising]
GenPromising.PState.PS.mEvent [variable, in ArchSem.GenPromising]
GenPromising.PState.PS.n [variable, in ArchSem.GenPromising]
GenPromising.PState.PS.tState [variable, in ArchSem.GenPromising]
GenPromising.PState.run_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.seq_step [definition, in ArchSem.GenPromising]
GenPromising.PState.set_t [instance, in ArchSem.GenPromising]
GenPromising.PState.SPromise [constructor, in ArchSem.GenPromising]
GenPromising.PState.SRun [constructor, in ArchSem.GenPromising]
GenPromising.PState.step [inductive, in ArchSem.GenPromising]
GenPromising.PState.step_promise [lemma, in ArchSem.GenPromising]
GenPromising.PState.step_sind [definition, in ArchSem.GenPromising]
GenPromising.PState.step_ind [definition, in ArchSem.GenPromising]
GenPromising.PState.t [abbreviation, in ArchSem.GenPromising]
GenPromising.PState.t [record, in ArchSem.GenPromising]
GenPromising.PState.terminated [definition, in ArchSem.GenPromising]
GenPromising.PState.terminated_tid [definition, in ArchSem.GenPromising]
GenPromising.PState.to_archState [definition, in ArchSem.GenPromising]
GenPromising.PState.tState [abbreviation, in ArchSem.GenPromising]
GenPromising.PState.tstate [definition, in ArchSem.GenPromising]
GenPromising.PState.tstates [projection, in ArchSem.GenPromising]
I
IMonFromSail [module, in ArchSem.FromSail]IMonFromSail.iMon_from_Sail [definition, in ArchSem.FromSail]
IMonFromSail.MemReq_from_sail [definition, in ArchSem.FromSail]
IMonFromSail.Sail_outcome_interp [definition, in ArchSem.FromSail]
IMonFromSail.Sail_nochoose [definition, in ArchSem.FromSail]
IMonFromSail.Sail_choose [definition, in ArchSem.FromSail]
Interface [module, in ArchSem.Interface]
Interface [library]
InterfaceT [module, in ArchSem.Interface]
Interface.address [definition, in ArchSem.Interface]
Interface.addr_overlap_sym_iff [lemma, in ArchSem.Interface]
Interface.addr_overlap_sym [lemma, in ArchSem.Interface]
Interface.addr_overlap_refl [lemma, in ArchSem.Interface]
Interface.addr_overlap_spec [lemma, in ArchSem.Interface]
Interface.addr_overlap [definition, in ArchSem.Interface]
Interface.addr_in_range_spec [lemma, in ArchSem.Interface]
Interface.addr_in_range_dec [instance, in ArchSem.Interface]
Interface.addr_in_range [definition, in ArchSem.Interface]
Interface.addr_range_length [lemma, in ArchSem.Interface]
Interface.addr_range [definition, in ArchSem.Interface]
Interface.addr_addN_zero [lemma, in ArchSem.Interface]
Interface.addr_addN_assoc [lemma, in ArchSem.Interface]
Interface.addr_addN [definition, in ArchSem.Interface]
Interface.Barrier [constructor, in ArchSem.Interface]
Interface.CacheOp [constructor, in ArchSem.Interface]
Interface.f_equal_addr_addN [definition, in ArchSem.Interface]
Interface.GenericFail [constructor, in ArchSem.Interface]
Interface.get_trans_end [definition, in ArchSem.Interface]
Interface.get_trans_start [definition, in ArchSem.Interface]
Interface.get_exn [definition, in ArchSem.Interface]
Interface.get_tlbi [definition, in ArchSem.Interface]
Interface.get_cacheop [definition, in ArchSem.Interface]
Interface.get_barrier [definition, in ArchSem.Interface]
Interface.get_mem_value_size [lemma, in ArchSem.Interface]
Interface.get_mem_value [definition, in ArchSem.Interface]
Interface.get_access_kind [definition, in ArchSem.Interface]
Interface.get_size [definition, in ArchSem.Interface]
Interface.get_addr_space [definition, in ArchSem.Interface]
Interface.get_addr [definition, in ArchSem.Interface]
Interface.get_mem_req [definition, in ArchSem.Interface]
Interface.get_rec_acc [definition, in ArchSem.Interface]
Interface.get_reg_val_get_reg [lemma, in ArchSem.Interface]
Interface.get_reg_val [definition, in ArchSem.Interface]
Interface.get_reg [definition, in ArchSem.Interface]
Interface.iEvent [definition, in ArchSem.Interface]
Interface.iMon [definition, in ArchSem.Interface]
Interface.iMon_throw [instance, in ArchSem.Interface]
Interface.isBarrier [section, in ArchSem.Interface]
Interface.isBarrier.P [variable, in ArchSem.Interface]
Interface.isBarrier.Pdec [variable, in ArchSem.Interface]
Interface.isCacheop [section, in ArchSem.Interface]
Interface.isCacheop.P [variable, in ArchSem.Interface]
Interface.isCacheop.Pdec [variable, in ArchSem.Interface]
Interface.IsMemRead [section, in ArchSem.Interface]
Interface.isMemReadReq [section, in ArchSem.Interface]
Interface.isMemReadReq.P [variable, in ArchSem.Interface]
Interface.isMemReadReq.Pdec [variable, in ArchSem.Interface]
Interface.IsMemRead.P [variable, in ArchSem.Interface]
Interface.IsMemRead.Pdec [variable, in ArchSem.Interface]
Interface.isMemWrite [section, in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce [section, in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce.P [variable, in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce.Pdec [variable, in ArchSem.Interface]
Interface.isMemWriteReq [section, in ArchSem.Interface]
Interface.isMemWriteReq.P [variable, in ArchSem.Interface]
Interface.isMemWriteReq.Pdec [variable, in ArchSem.Interface]
Interface.isMemWrite.P [variable, in ArchSem.Interface]
Interface.isMemWrite.Pdec [variable, in ArchSem.Interface]
Interface.isReg [section, in ArchSem.Interface]
Interface.isReg.P [variable, in ArchSem.Interface]
Interface.isReg.Pdec [variable, in ArchSem.Interface]
Interface.isTakeException [section, in ArchSem.Interface]
Interface.isTakeException.P [variable, in ArchSem.Interface]
Interface.isTakeException.Pdec [variable, in ArchSem.Interface]
Interface.isTlbop [section, in ArchSem.Interface]
Interface.isTlbop.P [variable, in ArchSem.Interface]
Interface.isTlbop.Pdec [variable, in ArchSem.Interface]
Interface.is_return_exception_dec [instance, in ArchSem.Interface]
Interface.is_return_exception [definition, in ArchSem.Interface]
Interface.is_take_exception [abbreviation, in ArchSem.Interface]
Interface.is_take_exceptionP_dec [instance, in ArchSem.Interface]
Interface.is_take_exceptionP_spec [definition, in ArchSem.Interface]
Interface.is_take_exceptionP [definition, in ArchSem.Interface]
Interface.is_tlbop [abbreviation, in ArchSem.Interface]
Interface.is_tlbopP_dec [instance, in ArchSem.Interface]
Interface.is_tlbopP_spec [definition, in ArchSem.Interface]
Interface.is_tlbopP [definition, in ArchSem.Interface]
Interface.is_cacheop [abbreviation, in ArchSem.Interface]
Interface.is_cacheopP_dec [instance, in ArchSem.Interface]
Interface.is_cacheopP_spec [definition, in ArchSem.Interface]
Interface.is_cacheopP [definition, in ArchSem.Interface]
Interface.is_barrier [abbreviation, in ArchSem.Interface]
Interface.is_barrierP_dec [instance, in ArchSem.Interface]
Interface.is_barrierP_spec [definition, in ArchSem.Interface]
Interface.is_barrierP [definition, in ArchSem.Interface]
Interface.is_mem_event_kindP_dec [instance, in ArchSem.Interface]
Interface.is_mem_event_kindP [definition, in ArchSem.Interface]
Interface.is_mem_write_kindP [definition, in ArchSem.Interface]
Interface.is_mem_read_kindP [definition, in ArchSem.Interface]
Interface.is_mem_event [definition, in ArchSem.Interface]
Interface.is_mem_write [abbreviation, in ArchSem.Interface]
Interface.is_mem_writeP_dec [instance, in ArchSem.Interface]
Interface.is_mem_writeP_cdestr [definition, in ArchSem.Interface]
Interface.is_mem_writeP_spec [definition, in ArchSem.Interface]
Interface.is_mem_writeP [definition, in ArchSem.Interface]
Interface.is_mem_write_req [abbreviation, in ArchSem.Interface]
Interface.is_mem_write_reqP_dec [instance, in ArchSem.Interface]
Interface.is_mem_write_reqP_cdestr [definition, in ArchSem.Interface]
Interface.is_mem_write_reqP_spec [definition, in ArchSem.Interface]
Interface.is_mem_write_reqP [definition, in ArchSem.Interface]
Interface.is_mem_write_addr_announce [abbreviation, in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_dec [instance, in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_cdestr [definition, in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_spec [definition, in ArchSem.Interface]
Interface.is_mem_write_addr_announceP [definition, in ArchSem.Interface]
Interface.is_mem_read [abbreviation, in ArchSem.Interface]
Interface.is_mem_readP_dec [instance, in ArchSem.Interface]
Interface.is_mem_readP_cdestr [definition, in ArchSem.Interface]
Interface.is_mem_readP_spec [definition, in ArchSem.Interface]
Interface.is_mem_readP [definition, in ArchSem.Interface]
Interface.is_mem_read_req [abbreviation, in ArchSem.Interface]
Interface.is_mem_read_reqP_dec [instance, in ArchSem.Interface]
Interface.is_mem_read_reqP_cdestr [definition, in ArchSem.Interface]
Interface.is_mem_read_reqP_spec [definition, in ArchSem.Interface]
Interface.is_mem_read_reqP [definition, in ArchSem.Interface]
Interface.is_reg_event [abbreviation, in ArchSem.Interface]
Interface.is_reg_write [abbreviation, in ArchSem.Interface]
Interface.is_reg_read [abbreviation, in ArchSem.Interface]
Interface.is_reg_eventP_dec [instance, in ArchSem.Interface]
Interface.is_reg_eventP_cdestr [definition, in ArchSem.Interface]
Interface.is_reg_eventP_spec [definition, in ArchSem.Interface]
Interface.is_reg_eventP [definition, in ArchSem.Interface]
Interface.is_reg_writeP_dec [instance, in ArchSem.Interface]
Interface.is_reg_writeP_cdestr [definition, in ArchSem.Interface]
Interface.is_reg_writeP_spec [definition, in ArchSem.Interface]
Interface.is_reg_writeP [definition, in ArchSem.Interface]
Interface.is_reg_readP_dec [instance, in ArchSem.Interface]
Interface.is_reg_readP_cdestr [definition, in ArchSem.Interface]
Interface.is_reg_readP_spec [definition, in ArchSem.Interface]
Interface.is_reg_readP [definition, in ArchSem.Interface]
Interface.is_rel_acq [definition, in ArchSem.Interface]
Interface.iTrace [definition, in ArchSem.Interface]
Interface.MemEventByKind [section, in ArchSem.Interface]
Interface.MemEventByKind.P [variable, in ArchSem.Interface]
Interface.MemEventByKind.Pdec [variable, in ArchSem.Interface]
Interface.MemRead [constructor, in ArchSem.Interface]
Interface.MemReq [module, in ArchSem.Interface]
Interface.MemReq.access_kind [projection, in ArchSem.Interface]
Interface.MemReq.address [projection, in ArchSem.Interface]
Interface.MemReq.address_space [projection, in ArchSem.Interface]
Interface.MemReq.eq_dec [instance, in ArchSem.Interface]
Interface.MemReq.eta [instance, in ArchSem.Interface]
Interface.MemReq.num_tag [projection, in ArchSem.Interface]
Interface.MemReq.range [definition, in ArchSem.Interface]
Interface.MemReq.size [projection, in ArchSem.Interface]
Interface.MemReq.t [record, in ArchSem.Interface]
Interface.MemWrite [constructor, in ArchSem.Interface]
Interface.MemWriteAddrAnnounce [constructor, in ArchSem.Interface]
Interface.outcome [inductive, in ArchSem.Interface]
Interface.outcome_EffCTransSimpl [instance, in ArchSem.Interface]
Interface.outcome_EffCTrans [instance, in ArchSem.Interface]
Interface.outcome_eq_dec [instance, in ArchSem.Interface]
Interface.outcome_wf [instance, in ArchSem.Interface]
Interface.outcome_ret [instance, in ArchSem.Interface]
Interface.outcome_sind [definition, in ArchSem.Interface]
Interface.outcome_rec [definition, in ArchSem.Interface]
Interface.outcome_ind [definition, in ArchSem.Interface]
Interface.outcome_rect [definition, in ArchSem.Interface]
Interface.RegRead [constructor, in ArchSem.Interface]
Interface.RegWrite [constructor, in ArchSem.Interface]
Interface.ReturnException [constructor, in ArchSem.Interface]
Interface.TakeException [constructor, in ArchSem.Interface]
Interface.TlbOp [constructor, in ArchSem.Interface]
Interface.TranslationEnd [constructor, in ArchSem.Interface]
Interface.TranslationStart [constructor, in ArchSem.Interface]
ISAManip [module, in ArchSem.ISAManip]
ISAManip [library]
ISAManip.GlobalVars [section, in ArchSem.ISAManip]
ISAManip.GlobalVars.global_vars [variable, in ArchSem.ISAManip]
ISAManip.global_vars_consistent_dec [instance, in ArchSem.ISAManip]
ISAManip.global_vars_consistent [definition, in ArchSem.ISAManip]
ISAManip.global_vars_consistent_aux_dec [instance, in ArchSem.ISAManip]
ISAManip.global_vars_consistent_aux [definition, in ArchSem.ISAManip]
ISAManip.remove_global_vars_equiv [lemma, in ArchSem.ISAManip]
ISAManip.remove_global_vars_traces [definition, in ArchSem.ISAManip]
ISAManip.remove_global_vars_trace_end [definition, in ArchSem.ISAManip]
ISAManip.remove_global_vars [definition, in ArchSem.ISAManip]
ISAManip.remove_global_vars_handler [definition, in ArchSem.ISAManip]
N
NoCHERI [module, in ArchSem.Interface]NoCHERI.no_cheri [axiom, in ArchSem.Interface]
P
PPState [module, in ArchSem.GenPromising]PPState.eta [instance, in ArchSem.GenPromising]
PPState.iis [projection, in ArchSem.GenPromising]
PPState.mem [projection, in ArchSem.GenPromising]
PPState.PPS [section, in ArchSem.GenPromising]
PPState.PPS.iis_t [variable, in ArchSem.GenPromising]
PPState.PPS.mEvent [variable, in ArchSem.GenPromising]
PPState.PPS.tState [variable, in ArchSem.GenPromising]
PPState.state [projection, in ArchSem.GenPromising]
PPState.t [record, in ArchSem.GenPromising]
PromMemory [module, in ArchSem.GenPromising]
PromMemory.attach_timestamps [definition, in ArchSem.GenPromising]
PromMemory.cut_after_with_timestamps [definition, in ArchSem.GenPromising]
PromMemory.cut_after [definition, in ArchSem.GenPromising]
PromMemory.cut_before [definition, in ArchSem.GenPromising]
PromMemory.lookup_inst [instance, in ArchSem.GenPromising]
PromMemory.PM [section, in ArchSem.GenPromising]
PromMemory.PM.ev [variable, in ArchSem.GenPromising]
PromMemory.t [definition, in ArchSem.GenPromising]
R
reg_gen_val_sind [definition, in ArchSem.Interface]reg_gen_val_rec [definition, in ArchSem.Interface]
reg_gen_val_ind [definition, in ArchSem.Interface]
reg_gen_val_rect [definition, in ArchSem.Interface]
reg_gen_val [inductive, in ArchSem.Interface]
RVArray [constructor, in ArchSem.Interface]
RVNumber [constructor, in ArchSem.Interface]
RVString [constructor, in ArchSem.Interface]
RVStruct [constructor, in ArchSem.Interface]
S
SailArch [module, in ArchSem.FromSail]SailInterfaceT [module, in ArchSem.FromSail]
SeqModel [library]
SequentialModel [module, in ArchSem.SeqModel]
SequentialModel.check_address_space [definition, in ArchSem.SeqModel]
SequentialModel.mem_was_written [definition, in ArchSem.SeqModel]
SequentialModel.read_mem_seq_state [definition, in ArchSem.SeqModel]
SequentialModel.read_byte_seq_state [definition, in ArchSem.SeqModel]
SequentialModel.read_reg_seq_state [definition, in ArchSem.SeqModel]
SequentialModel.Seq [section, in ArchSem.SeqModel]
SequentialModel.seqmon [abbreviation, in ArchSem.SeqModel]
SequentialModel.sequential_modelc [definition, in ArchSem.SeqModel]
SequentialModel.sequential_opmodel [definition, in ArchSem.SeqModel]
SequentialModel.sequential_model_outcome [definition, in ArchSem.SeqModel]
SequentialModel.seq_state [record, in ArchSem.SeqModel]
SequentialModel.Seq.regs_whitelist [variable, in ArchSem.SeqModel]
SequentialModel.sst [projection, in ArchSem.SeqModel]
SequentialModel.write_mem_seq_state [definition, in ArchSem.SeqModel]
SequentialModel.write_reg_seq_state [definition, in ArchSem.SeqModel]
SequentialModel.written [projection, in ArchSem.SeqModel]
T
TermModels [module, in ArchSem.TermModels]TermModels [library]
TermModelsT [module, in ArchSem.TermModels]
TermModels.archModel [module, in ArchSem.TermModels]
TermModels.archModel.c [abbreviation, in ArchSem.TermModels]
TermModels.archModel.equiv [instance, in ArchSem.TermModels]
TermModels.archModel.equiv_errors [lemma, in ArchSem.TermModels]
TermModels.archModel.equiv_wider' [lemma, in ArchSem.TermModels]
TermModels.archModel.equiv_wider [lemma, in ArchSem.TermModels]
TermModels.archModel.equiv_weaker [lemma, in ArchSem.TermModels]
TermModels.archModel.map_set [definition, in ArchSem.TermModels]
TermModels.archModel.Model [section, in ArchSem.TermModels]
TermModels.archModel.Model.flag [variable, in ArchSem.TermModels]
TermModels.archModel.nc [abbreviation, in ArchSem.TermModels]
TermModels.archModel.res [abbreviation, in ArchSem.TermModels]
TermModels.archModel.Res [module, in ArchSem.TermModels]
TermModels.archModel.Res.AMR [section, in ArchSem.TermModels]
TermModels.archModel.Res.AMR.flag [variable, in ArchSem.TermModels]
TermModels.archModel.Res.AMR.n [variable, in ArchSem.TermModels]
TermModels.archModel.Res.AMR.termCond [variable, in ArchSem.TermModels]
TermModels.archModel.Res.equiv [definition, in ArchSem.TermModels]
TermModels.archModel.Res.equiv_errors [lemma, in ArchSem.TermModels]
TermModels.archModel.Res.equiv_wider' [lemma, in ArchSem.TermModels]
TermModels.archModel.Res.equiv_wider [lemma, in ArchSem.TermModels]
TermModels.archModel.Res.Error [constructor, in ArchSem.TermModels]
TermModels.archModel.Res.errors [definition, in ArchSem.TermModels]
TermModels.archModel.Res.FinalState [constructor, in ArchSem.TermModels]
TermModels.archModel.Res.finalStates [definition, in ArchSem.TermModels]
TermModels.archModel.Res.Flagged [constructor, in ArchSem.TermModels]
TermModels.archModel.Res.flags [definition, in ArchSem.TermModels]
TermModels.archModel.Res.from_exec [definition, in ArchSem.TermModels]
TermModels.archModel.Res.from_result [definition, in ArchSem.TermModels]
TermModels.archModel.Res.no_error [definition, in ArchSem.TermModels]
TermModels.archModel.Res.set_unfold_elem_of_errors [instance, in ArchSem.TermModels]
TermModels.archModel.Res.set_unfold_elem_of_finalStates [instance, in ArchSem.TermModels]
TermModels.archModel.Res.set_unfold_elem_of_flagifieds [instance, in ArchSem.TermModels]
TermModels.archModel.Res.t [inductive, in ArchSem.TermModels]
TermModels.archModel.Res.t_sind [definition, in ArchSem.TermModels]
TermModels.archModel.Res.t_rec [definition, in ArchSem.TermModels]
TermModels.archModel.Res.t_ind [definition, in ArchSem.TermModels]
TermModels.archModel.Res.t_rect [definition, in ArchSem.TermModels]
TermModels.archModel.Res.weaker [definition, in ArchSem.TermModels]
TermModels.archModel.Res.wider [definition, in ArchSem.TermModels]
TermModels.archModel.Res.wider_weaker [lemma, in ArchSem.TermModels]
TermModels.archModel.t [definition, in ArchSem.TermModels]
TermModels.archModel.to_nc [definition, in ArchSem.TermModels]
TermModels.archModel.weaker [definition, in ArchSem.TermModels]
TermModels.archModel.wider [definition, in ArchSem.TermModels]
TermModels.archModel.wider_weaker [lemma, in ArchSem.TermModels]
TermModels.archState [abbreviation, in ArchSem.TermModels]
TermModels.archState [module, in ArchSem.TermModels]
TermModels.archState.address_space [projection, in ArchSem.TermModels]
TermModels.archState.is_terminated_dec [instance, in ArchSem.TermModels]
TermModels.archState.is_terminated [definition, in ArchSem.TermModels]
TermModels.archState.memory [projection, in ArchSem.TermModels]
TermModels.archState.regs [projection, in ArchSem.TermModels]
TermModels.archState.t [record, in ArchSem.TermModels]
TermModels.memoryMap [definition, in ArchSem.TermModels]
TermModels.mem_delete [definition, in ArchSem.TermModels]
TermModels.mem_insert [definition, in ArchSem.TermModels]
TermModels.mem_insert_bv [definition, in ArchSem.TermModels]
TermModels.mem_insert_bytes [definition, in ArchSem.TermModels]
TermModels.mem_insert_byte [definition, in ArchSem.TermModels]
TermModels.mem_present [definition, in ArchSem.TermModels]
TermModels.mem_present_nat [definition, in ArchSem.TermModels]
TermModels.mem_lookup [definition, in ArchSem.TermModels]
TermModels.mem_lookup_bytes [definition, in ArchSem.TermModels]
TermModels.mem_lookup_byte [definition, in ArchSem.TermModels]
TermModels.opModel [abbreviation, in ArchSem.TermModels]
TermModels.opModel [module, in ArchSem.TermModels]
TermModels.opModel.init [projection, in ArchSem.TermModels]
TermModels.opModel.run [definition, in ArchSem.TermModels]
TermModels.opModel.state [projection, in ArchSem.TermModels]
TermModels.opModel.step [projection, in ArchSem.TermModels]
TermModels.opModel.t [record, in ArchSem.TermModels]
TermModels.opModel.to_archModel1 [definition, in ArchSem.TermModels]
TermModels.opModel.to_archModel [definition, in ArchSem.TermModels]
TermModels.registerMap [definition, in ArchSem.TermModels]
TermModels.reg_delete [definition, in ArchSem.TermModels]
TermModels.reg_insert [definition, in ArchSem.TermModels]
TermModels.reg_lookup [definition, in ArchSem.TermModels]
TermModels.terminationCondition [definition, in ArchSem.TermModels]
Notation Index
C
_ <â‚šâ‚Šáµ¢ _ (eid_scope) [in ArchSem.CandidateExecutions]_ <áµ¢ _ (eid_scope) [in ArchSem.CandidateExecutions]
_ <â‚š _ (eid_scope) [in ArchSem.CandidateExecutions]
Module Index
A
Arch [in ArchSem.Interface]ArchExtra [in ArchSem.FromSail]
ArchFromSail [in ArchSem.FromSail]
ArchFromSailT [in ArchSem.FromSail]
ArchInst [in ArchSem.ArchInst]
ArchInst.Cand [in ArchSem.ArchInst]
ArchInst.GenPro [in ArchSem.ArchInst]
ArchInst.Interface [in ArchSem.ArchInst]
ArchInst.ISAManip [in ArchSem.ArchInst]
ArchInst.SeqModel [in ArchSem.ArchInst]
ArchInst.TM [in ArchSem.ArchInst]
C
CandidateExecutions [in ArchSem.CandidateExecutions]CandidateExecutions.Ax [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate [in ArchSem.CandidateExecutions]
CandidateExecutions.EID [in ArchSem.CandidateExecutions]
G
GenPromising [in ArchSem.GenPromising]GenPromisingT [in ArchSem.GenPromising]
GenPromising.CPState [in ArchSem.GenPromising]
GenPromising.Promising [in ArchSem.GenPromising]
GenPromising.PState [in ArchSem.GenPromising]
I
IMonFromSail [in ArchSem.FromSail]Interface [in ArchSem.Interface]
InterfaceT [in ArchSem.Interface]
Interface.MemReq [in ArchSem.Interface]
ISAManip [in ArchSem.ISAManip]
N
NoCHERI [in ArchSem.Interface]P
PPState [in ArchSem.GenPromising]PromMemory [in ArchSem.GenPromising]
S
SailArch [in ArchSem.FromSail]SailInterfaceT [in ArchSem.FromSail]
SequentialModel [in ArchSem.SeqModel]
T
TermModels [in ArchSem.TermModels]TermModelsT [in ArchSem.TermModels]
TermModels.archModel [in ArchSem.TermModels]
TermModels.archModel.Res [in ArchSem.TermModels]
TermModels.archState [in ArchSem.TermModels]
TermModels.opModel [in ArchSem.TermModels]
Variable Index
C
CandidateExecutions.Ax.Ax.et [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.Ax.flag [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.Res.et [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.Res.flag [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand.et [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand.nmth [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.cd [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.et [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps.n [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind.P [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind.Pdec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.et [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.nmth [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.CPS.isem [in ArchSem.GenPromising]GenPromising.CPState.CPS.mEvent_eq_dec [in ArchSem.GenPromising]
GenPromising.CPState.CPS.n [in ArchSem.GenPromising]
GenPromising.CPState.CPS.prom [in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult.initmem [in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult.tid [in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.term [in ArchSem.GenPromising]
GenPromising.PState.PSProm.isem [in ArchSem.GenPromising]
GenPromising.PState.PSProm.n [in ArchSem.GenPromising]
GenPromising.PState.PSProm.prom [in ArchSem.GenPromising]
GenPromising.PState.PS.mEvent [in ArchSem.GenPromising]
GenPromising.PState.PS.n [in ArchSem.GenPromising]
GenPromising.PState.PS.tState [in ArchSem.GenPromising]
I
Interface.isBarrier.P [in ArchSem.Interface]Interface.isBarrier.Pdec [in ArchSem.Interface]
Interface.isCacheop.P [in ArchSem.Interface]
Interface.isCacheop.Pdec [in ArchSem.Interface]
Interface.isMemReadReq.P [in ArchSem.Interface]
Interface.isMemReadReq.Pdec [in ArchSem.Interface]
Interface.IsMemRead.P [in ArchSem.Interface]
Interface.IsMemRead.Pdec [in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce.P [in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce.Pdec [in ArchSem.Interface]
Interface.isMemWriteReq.P [in ArchSem.Interface]
Interface.isMemWriteReq.Pdec [in ArchSem.Interface]
Interface.isMemWrite.P [in ArchSem.Interface]
Interface.isMemWrite.Pdec [in ArchSem.Interface]
Interface.isReg.P [in ArchSem.Interface]
Interface.isReg.Pdec [in ArchSem.Interface]
Interface.isTakeException.P [in ArchSem.Interface]
Interface.isTakeException.Pdec [in ArchSem.Interface]
Interface.isTlbop.P [in ArchSem.Interface]
Interface.isTlbop.Pdec [in ArchSem.Interface]
Interface.MemEventByKind.P [in ArchSem.Interface]
Interface.MemEventByKind.Pdec [in ArchSem.Interface]
ISAManip.GlobalVars.global_vars [in ArchSem.ISAManip]
P
PPState.PPS.iis_t [in ArchSem.GenPromising]PPState.PPS.mEvent [in ArchSem.GenPromising]
PPState.PPS.tState [in ArchSem.GenPromising]
PromMemory.PM.ev [in ArchSem.GenPromising]
S
SequentialModel.Seq.regs_whitelist [in ArchSem.SeqModel]T
TermModels.archModel.Model.flag [in ArchSem.TermModels]TermModels.archModel.Res.AMR.flag [in ArchSem.TermModels]
TermModels.archModel.Res.AMR.n [in ArchSem.TermModels]
TermModels.archModel.Res.AMR.termCond [in ArchSem.TermModels]
Library Index
A
ArchInstC
CandidateExecutionsF
FromSailG
GenPromisingI
InterfaceISAManip
S
SeqModelT
TermModelsAxiom Index
A
ArchExtra.pc_reg [in ArchSem.FromSail]ArchExtra.reg_type_to_gen [in ArchSem.FromSail]
ArchExtra.reg_type_of_gen [in ArchSem.FromSail]
ArchExtra.reg_of_string [in ArchSem.FromSail]
Arch.abort [in ArchSem.Interface]
Arch.addr_space_countable [in ArchSem.Interface]
Arch.addr_space_eq [in ArchSem.Interface]
Arch.addr_space [in ArchSem.Interface]
Arch.addr_size [in ArchSem.Interface]
Arch.barrier [in ArchSem.Interface]
Arch.barrier_eq [in ArchSem.Interface]
Arch.cache_op_eq [in ArchSem.Interface]
Arch.cache_op [in ArchSem.Interface]
Arch.cap_size_log [in ArchSem.Interface]
Arch.CHERI [in ArchSem.Interface]
Arch.ctrans_reg_type_simpl [in ArchSem.Interface]
Arch.ctrans_reg_type [in ArchSem.Interface]
Arch.exn [in ArchSem.Interface]
Arch.exn_eq [in ArchSem.Interface]
Arch.is_atomic_rmw [in ArchSem.Interface]
Arch.is_exclusive [in ArchSem.Interface]
Arch.is_standalone [in ArchSem.Interface]
Arch.is_rel_acq_rcpc [in ArchSem.Interface]
Arch.is_rel_acq_rcsc [in ArchSem.Interface]
Arch.is_relaxed [in ArchSem.Interface]
Arch.is_ttw [in ArchSem.Interface]
Arch.is_ifetch [in ArchSem.Interface]
Arch.is_explicit [in ArchSem.Interface]
Arch.mem_acc_eq [in ArchSem.Interface]
Arch.mem_acc [in ArchSem.Interface]
Arch.pc_reg [in ArchSem.Interface]
Arch.pretty_reg [in ArchSem.Interface]
Arch.reg [in ArchSem.Interface]
Arch.reg_acc_eq [in ArchSem.Interface]
Arch.reg_acc [in ArchSem.Interface]
Arch.reg_type_to_gen [in ArchSem.Interface]
Arch.reg_type_of_gen [in ArchSem.Interface]
Arch.reg_type_eq_dep_dec [in ArchSem.Interface]
Arch.reg_type_inhabited [in ArchSem.Interface]
Arch.reg_type_countable [in ArchSem.Interface]
Arch.reg_type_eq [in ArchSem.Interface]
Arch.reg_type [in ArchSem.Interface]
Arch.reg_of_string [in ArchSem.Interface]
Arch.reg_countable [in ArchSem.Interface]
Arch.reg_eq [in ArchSem.Interface]
Arch.tlbi [in ArchSem.Interface]
Arch.tlbi_eq [in ArchSem.Interface]
Arch.trans_end_eq [in ArchSem.Interface]
Arch.trans_end [in ArchSem.Interface]
Arch.trans_start_eq [in ArchSem.Interface]
Arch.trans_start [in ArchSem.Interface]
N
NoCHERI.no_cheri [in ArchSem.Interface]Lemma Index
C
CandidateExecutions.Ax.equiv_Model [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.equiv_is_ok [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_wider' [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_wider [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv_weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_is_ok [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_wider' [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_wider [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv_weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.wider_weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.weaker_Model [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider_Model [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider_weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.bytes_per_event_NoDup [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_iEvent_NoDup [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_map_match [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_NoDup [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_NoDup1 [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list_match [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.gather_by_key_None [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iEvent_list_match [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_list_match [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match_use [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete_use [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_sym_iff [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_sym [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_is_Some_gather_by_key [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_events_union [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_reqs_union [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_reqs_union [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_po [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_gen [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.overlapping_sym [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.possible_initial_reg_reads_ok [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_reg_reads_decomp [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_same_reg [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_irreflexive [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg_val_same_reg [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_mem_value_size [in ArchSem.CandidateExecutions]
G
GenPromising.PState.step_promise [in ArchSem.GenPromising]I
Interface.addr_overlap_sym_iff [in ArchSem.Interface]Interface.addr_overlap_sym [in ArchSem.Interface]
Interface.addr_overlap_refl [in ArchSem.Interface]
Interface.addr_overlap_spec [in ArchSem.Interface]
Interface.addr_in_range_spec [in ArchSem.Interface]
Interface.addr_range_length [in ArchSem.Interface]
Interface.addr_addN_zero [in ArchSem.Interface]
Interface.addr_addN_assoc [in ArchSem.Interface]
Interface.get_mem_value_size [in ArchSem.Interface]
Interface.get_reg_val_get_reg [in ArchSem.Interface]
ISAManip.remove_global_vars_equiv [in ArchSem.ISAManip]
T
TermModels.archModel.equiv_errors [in ArchSem.TermModels]TermModels.archModel.equiv_wider' [in ArchSem.TermModels]
TermModels.archModel.equiv_wider [in ArchSem.TermModels]
TermModels.archModel.equiv_weaker [in ArchSem.TermModels]
TermModels.archModel.Res.equiv_errors [in ArchSem.TermModels]
TermModels.archModel.Res.equiv_wider' [in ArchSem.TermModels]
TermModels.archModel.Res.equiv_wider [in ArchSem.TermModels]
TermModels.archModel.Res.wider_weaker [in ArchSem.TermModels]
TermModels.archModel.wider_weaker [in ArchSem.TermModels]
Constructor Index
C
CandidateExecutions.Ax.Allowed [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.Flagged [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Rejected [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.MS [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.NMS [in ArchSem.CandidateExecutions]
G
GenPromising.PState.SPromise [in ArchSem.GenPromising]GenPromising.PState.SRun [in ArchSem.GenPromising]
I
Interface.Barrier [in ArchSem.Interface]Interface.CacheOp [in ArchSem.Interface]
Interface.GenericFail [in ArchSem.Interface]
Interface.MemRead [in ArchSem.Interface]
Interface.MemWrite [in ArchSem.Interface]
Interface.MemWriteAddrAnnounce [in ArchSem.Interface]
Interface.RegRead [in ArchSem.Interface]
Interface.RegWrite [in ArchSem.Interface]
Interface.ReturnException [in ArchSem.Interface]
Interface.TakeException [in ArchSem.Interface]
Interface.TlbOp [in ArchSem.Interface]
Interface.TranslationEnd [in ArchSem.Interface]
Interface.TranslationStart [in ArchSem.Interface]
R
RVArray [in ArchSem.Interface]RVNumber [in ArchSem.Interface]
RVString [in ArchSem.Interface]
RVStruct [in ArchSem.Interface]
T
TermModels.archModel.Res.Error [in ArchSem.TermModels]TermModels.archModel.Res.FinalState [in ArchSem.TermModels]
TermModels.archModel.Res.Flagged [in ArchSem.TermModels]
Projection Index
C
CandidateExecutions.Candidate.addr_space_wf' [in ArchSem.CandidateExecutions]CandidateExecutions.Candidate.coherence [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.coherence_wf' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_contains_overlapping_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_irreflexive [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.co_transitive [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.events [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.footprint_wf' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_same_pa [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_instruction_order [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_to_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_from_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_footprint_valid [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre_exec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_footprint_valid [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_valid_initial [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_valid [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_functional [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_to_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rf_from_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_initial_valid [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_same_reg_val [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_functional [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_to_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rrf_from_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.byte [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.ieid [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.iid [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.tid [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.errors [in ArchSem.GenPromising]GenPromising.CPState.final_states [in ArchSem.GenPromising]
GenPromising.CPState.out_of_fuel [in ArchSem.GenPromising]
GenPromising.CPState.promises [in ArchSem.GenPromising]
GenPromising.Promising.address_space [in ArchSem.GenPromising]
GenPromising.Promising.check_valid_end [in ArchSem.GenPromising]
GenPromising.Promising.emit_promise [in ArchSem.GenPromising]
GenPromising.Promising.filter_promises [in ArchSem.GenPromising]
GenPromising.Promising.handle_outcome [in ArchSem.GenPromising]
GenPromising.Promising.iis [in ArchSem.GenPromising]
GenPromising.Promising.iis_init [in ArchSem.GenPromising]
GenPromising.Promising.memory_snapshot [in ArchSem.GenPromising]
GenPromising.Promising.mEvent [in ArchSem.GenPromising]
GenPromising.Promising.mEvent_tid [in ArchSem.GenPromising]
GenPromising.Promising.mEvent_eq_dec [in ArchSem.GenPromising]
GenPromising.Promising.tState [in ArchSem.GenPromising]
GenPromising.Promising.tState_nopromises [in ArchSem.GenPromising]
GenPromising.Promising.tState_regs [in ArchSem.GenPromising]
GenPromising.Promising.tState_init [in ArchSem.GenPromising]
GenPromising.PState.events [in ArchSem.GenPromising]
GenPromising.PState.initmem [in ArchSem.GenPromising]
GenPromising.PState.tstates [in ArchSem.GenPromising]
I
Interface.MemReq.access_kind [in ArchSem.Interface]Interface.MemReq.address [in ArchSem.Interface]
Interface.MemReq.address_space [in ArchSem.Interface]
Interface.MemReq.num_tag [in ArchSem.Interface]
Interface.MemReq.size [in ArchSem.Interface]
P
PPState.iis [in ArchSem.GenPromising]PPState.mem [in ArchSem.GenPromising]
PPState.state [in ArchSem.GenPromising]
S
SequentialModel.sst [in ArchSem.SeqModel]SequentialModel.written [in ArchSem.SeqModel]
T
TermModels.archState.address_space [in ArchSem.TermModels]TermModels.archState.memory [in ArchSem.TermModels]
TermModels.archState.regs [in ArchSem.TermModels]
TermModels.opModel.init [in ArchSem.TermModels]
TermModels.opModel.state [in ArchSem.TermModels]
TermModels.opModel.step [in ArchSem.TermModels]
Inductive Index
C
CandidateExecutions.Ax.behavior [in ArchSem.CandidateExecutions]CandidateExecutions.Candidate.exec_type [in ArchSem.CandidateExecutions]
G
GenPromising.PState.step [in ArchSem.GenPromising]I
Interface.outcome [in ArchSem.Interface]R
reg_gen_val [in ArchSem.Interface]T
TermModels.archModel.Res.t [in ArchSem.TermModels]Instance Index
A
ArchFromSail.ctrans_reg_type_simpl [in ArchSem.FromSail]ArchFromSail.ctrans_reg_type [in ArchSem.FromSail]
ArchFromSail.reg_type_eq_dep_dec [in ArchSem.FromSail]
B
bitU_finite [in ArchSem.FromSail]C
CandidateExecutions.Candidate.addr_space_wf_dec [in ArchSem.CandidateExecutions]CandidateExecutions.Candidate.coherence_wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.eta [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.footprint_wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_failed_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_rf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_mem_read_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_nms_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_eid_candidate [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_total_unfold_gather_by_key [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_unfold_event_map [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_eid_pre [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre_eta [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_instruction_order [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_iio [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_access [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_instruction_instance [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_thread [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_same_key [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_gather_by_key_lookup [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_valid_eids [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_elem_of_collect_all [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.set_unfold_elem_of_event_list [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.wf_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.cdestr_rec_inj [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.countable [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.eq_dec [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.eta [in ArchSem.CandidateExecutions]
G
GenPromising.PState.PState_PPState_set [in ArchSem.GenPromising]GenPromising.PState.set_t [in ArchSem.GenPromising]
I
Interface.addr_in_range_dec [in ArchSem.Interface]Interface.iMon_throw [in ArchSem.Interface]
Interface.is_return_exception_dec [in ArchSem.Interface]
Interface.is_take_exceptionP_dec [in ArchSem.Interface]
Interface.is_tlbopP_dec [in ArchSem.Interface]
Interface.is_cacheopP_dec [in ArchSem.Interface]
Interface.is_barrierP_dec [in ArchSem.Interface]
Interface.is_mem_event_kindP_dec [in ArchSem.Interface]
Interface.is_mem_writeP_dec [in ArchSem.Interface]
Interface.is_mem_write_reqP_dec [in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_dec [in ArchSem.Interface]
Interface.is_mem_readP_dec [in ArchSem.Interface]
Interface.is_mem_read_reqP_dec [in ArchSem.Interface]
Interface.is_reg_eventP_dec [in ArchSem.Interface]
Interface.is_reg_writeP_dec [in ArchSem.Interface]
Interface.is_reg_readP_dec [in ArchSem.Interface]
Interface.MemReq.eq_dec [in ArchSem.Interface]
Interface.MemReq.eta [in ArchSem.Interface]
Interface.outcome_EffCTransSimpl [in ArchSem.Interface]
Interface.outcome_EffCTrans [in ArchSem.Interface]
Interface.outcome_eq_dec [in ArchSem.Interface]
Interface.outcome_wf [in ArchSem.Interface]
Interface.outcome_ret [in ArchSem.Interface]
ISAManip.global_vars_consistent_dec [in ArchSem.ISAManip]
ISAManip.global_vars_consistent_aux_dec [in ArchSem.ISAManip]
P
PPState.eta [in ArchSem.GenPromising]PromMemory.lookup_inst [in ArchSem.GenPromising]
T
TermModels.archModel.equiv [in ArchSem.TermModels]TermModels.archModel.Res.set_unfold_elem_of_errors [in ArchSem.TermModels]
TermModels.archModel.Res.set_unfold_elem_of_finalStates [in ArchSem.TermModels]
TermModels.archModel.Res.set_unfold_elem_of_flagifieds [in ArchSem.TermModels]
TermModels.archState.is_terminated_dec [in ArchSem.TermModels]
Section Index
C
CandidateExecutions.Ax.Ax [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.Res.Res [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Cand [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Deps [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.Pre.ByKind [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.CPS [in ArchSem.GenPromising]GenPromising.CPState.CPS.Steps [in ArchSem.GenPromising]
GenPromising.CPState.CPS.Steps.EnumerateResult [in ArchSem.GenPromising]
GenPromising.PState.PS [in ArchSem.GenPromising]
GenPromising.PState.PSProm [in ArchSem.GenPromising]
I
Interface.isBarrier [in ArchSem.Interface]Interface.isCacheop [in ArchSem.Interface]
Interface.IsMemRead [in ArchSem.Interface]
Interface.isMemReadReq [in ArchSem.Interface]
Interface.isMemWrite [in ArchSem.Interface]
Interface.isMemWriteAddrAnnounce [in ArchSem.Interface]
Interface.isMemWriteReq [in ArchSem.Interface]
Interface.isReg [in ArchSem.Interface]
Interface.isTakeException [in ArchSem.Interface]
Interface.isTlbop [in ArchSem.Interface]
Interface.MemEventByKind [in ArchSem.Interface]
ISAManip.GlobalVars [in ArchSem.ISAManip]
P
PPState.PPS [in ArchSem.GenPromising]PromMemory.PM [in ArchSem.GenPromising]
S
SequentialModel.Seq [in ArchSem.SeqModel]T
TermModels.archModel.Model [in ArchSem.TermModels]TermModels.archModel.Res.AMR [in ArchSem.TermModels]
Abbreviation Index
C
CandidateExecutions.Ax.archres [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.axres [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.cand [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.cand [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.model [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.archres [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.axres [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.cand [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.t [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.events' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init' [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.t [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.iis [in ArchSem.GenPromising]GenPromising.CPState.mEvent [in ArchSem.GenPromising]
GenPromising.CPState.t [in ArchSem.GenPromising]
GenPromising.CPState.tState [in ArchSem.GenPromising]
GenPromising.PState.mEvent [in ArchSem.GenPromising]
GenPromising.PState.t [in ArchSem.GenPromising]
GenPromising.PState.tState [in ArchSem.GenPromising]
I
Interface.is_take_exception [in ArchSem.Interface]Interface.is_tlbop [in ArchSem.Interface]
Interface.is_cacheop [in ArchSem.Interface]
Interface.is_barrier [in ArchSem.Interface]
Interface.is_mem_write [in ArchSem.Interface]
Interface.is_mem_write_req [in ArchSem.Interface]
Interface.is_mem_write_addr_announce [in ArchSem.Interface]
Interface.is_mem_read [in ArchSem.Interface]
Interface.is_mem_read_req [in ArchSem.Interface]
Interface.is_reg_event [in ArchSem.Interface]
Interface.is_reg_write [in ArchSem.Interface]
Interface.is_reg_read [in ArchSem.Interface]
S
SequentialModel.seqmon [in ArchSem.SeqModel]T
TermModels.archModel.c [in ArchSem.TermModels]TermModels.archModel.nc [in ArchSem.TermModels]
TermModels.archModel.res [in ArchSem.TermModels]
TermModels.archState [in ArchSem.TermModels]
TermModels.opModel [in ArchSem.TermModels]
Definition Index
A
ArchFromSail.abort [in ArchSem.FromSail]ArchFromSail.addr_space_countable [in ArchSem.FromSail]
ArchFromSail.addr_space_eq [in ArchSem.FromSail]
ArchFromSail.addr_space [in ArchSem.FromSail]
ArchFromSail.addr_size [in ArchSem.FromSail]
ArchFromSail.barrier [in ArchSem.FromSail]
ArchFromSail.barrier_eq [in ArchSem.FromSail]
ArchFromSail.cache_op_eq [in ArchSem.FromSail]
ArchFromSail.cache_op [in ArchSem.FromSail]
ArchFromSail.cap_size_log [in ArchSem.FromSail]
ArchFromSail.CHERI [in ArchSem.FromSail]
ArchFromSail.exn [in ArchSem.FromSail]
ArchFromSail.exn_eq [in ArchSem.FromSail]
ArchFromSail.is_atomic_rmw [in ArchSem.FromSail]
ArchFromSail.is_exclusive [in ArchSem.FromSail]
ArchFromSail.is_standalone [in ArchSem.FromSail]
ArchFromSail.is_rel_acq_rcsc [in ArchSem.FromSail]
ArchFromSail.is_rel_acq_rcpc [in ArchSem.FromSail]
ArchFromSail.is_relaxed [in ArchSem.FromSail]
ArchFromSail.is_ttw [in ArchSem.FromSail]
ArchFromSail.is_ifetch [in ArchSem.FromSail]
ArchFromSail.is_explicit [in ArchSem.FromSail]
ArchFromSail.mem_acc_eq [in ArchSem.FromSail]
ArchFromSail.mem_acc [in ArchSem.FromSail]
ArchFromSail.pc_reg [in ArchSem.FromSail]
ArchFromSail.pretty_reg [in ArchSem.FromSail]
ArchFromSail.reg [in ArchSem.FromSail]
ArchFromSail.reg_acc_eq [in ArchSem.FromSail]
ArchFromSail.reg_acc [in ArchSem.FromSail]
ArchFromSail.reg_type_to_gen [in ArchSem.FromSail]
ArchFromSail.reg_type_of_gen [in ArchSem.FromSail]
ArchFromSail.reg_type_inhabited [in ArchSem.FromSail]
ArchFromSail.reg_type_countable [in ArchSem.FromSail]
ArchFromSail.reg_type_eq [in ArchSem.FromSail]
ArchFromSail.reg_type [in ArchSem.FromSail]
ArchFromSail.reg_of_string [in ArchSem.FromSail]
ArchFromSail.reg_countable [in ArchSem.FromSail]
ArchFromSail.reg_eq [in ArchSem.FromSail]
ArchFromSail.tlbi [in ArchSem.FromSail]
ArchFromSail.tlbi_eq [in ArchSem.FromSail]
ArchFromSail.trans_end_eq [in ArchSem.FromSail]
ArchFromSail.trans_end [in ArchSem.FromSail]
ArchFromSail.trans_start_eq [in ArchSem.FromSail]
ArchFromSail.trans_start [in ArchSem.FromSail]
C
CandidateExecutions.Ax.behavior_sind [in ArchSem.CandidateExecutions]CandidateExecutions.Ax.behavior_rec [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_ind [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.behavior_rect [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.equiv [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.equiv [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.to_archModel [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.Res.wider [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.t [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.to_archModel_nc [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.weaker [in ArchSem.CandidateExecutions]
CandidateExecutions.Ax.wider [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.addr_space_wf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_update [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_rmw_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.atomic_rmw_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.barriers [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.bytes_per_event [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.cacheops [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.cd_to_archState [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.collect_all [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.convert_to_EID_rel [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ctrl [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.data [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_event_ids [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.EID_list_from_iEvent [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_map [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.event_list [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exclusive_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exclusive_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_sind [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_rec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_ind [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.exec_type_rect [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.explicit_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.explicit_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_mem_map [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_write_per_addr [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_reg_map [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.final_reg_map_tid [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.from_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.full_instruction_order [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.gather_by_key [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.get_addr_footprint [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.has_only_supported_events [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iEvent_list [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ifetch_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ifetch_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iio [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.iio_addr [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.initial_reg_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.init_mem_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_order [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.instruction_list [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_failed [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_complete [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ISA_match [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_rf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_mem_read [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_cdestr [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read_spec [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_valid_init_reg_read [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_nms [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.is_overlapping [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_iEvent [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lookup_instruction [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_atomic_rmw [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_exclusive [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_standalone [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_rel_acq_rcpc [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_rel_acq_rcsc [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_relaxed [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_ttw [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_ifetch [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_explicit [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_by_kind [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_events [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_aborts [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_reqs [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_write_addr_announces [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_aborts [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_read_reqs [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.mem_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after_spec_po_loc [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.not_after [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.overlapping [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_reads_from [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pc_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.possible_initial_reg_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_by_kind [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_data [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_from_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.relaxed_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.relaxed_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcpc_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcpc_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcsc_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.rel_acq_rcsc_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg_val [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_reg [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_mem_value [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_footprint [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_size [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_addr [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_access [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_instruction_instance [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_thread [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.same_key [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.standalone_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.standalone_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.tlbis [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ttw_writes [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.ttw_reads [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.unsupported_event [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.valid_eids [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.writes_by_kind [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.full_po_lt [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.iio_lt [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.po_lt [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.cpromise_tid [in ArchSem.GenPromising]GenPromising.CPState.enumerate_results [in ArchSem.GenPromising]
GenPromising.CPState.final [in ArchSem.GenPromising]
GenPromising.CPState.make_final [in ArchSem.GenPromising]
GenPromising.CPState.opmodel [in ArchSem.GenPromising]
GenPromising.CPState.opmodel_pf [in ArchSem.GenPromising]
GenPromising.CPState.promise_select_tid [in ArchSem.GenPromising]
GenPromising.CPState.run_transition_promise_first [in ArchSem.GenPromising]
GenPromising.CPState.run_transition [in ArchSem.GenPromising]
GenPromising.CPState.run_step [in ArchSem.GenPromising]
GenPromising.CPState.run_to_termination [in ArchSem.GenPromising]
GenPromising.CPState.run_outcome_with_promise [in ArchSem.GenPromising]
GenPromising.CPState.to_final_archState [in ArchSem.GenPromising]
GenPromising.CPState.validate_final [in ArchSem.GenPromising]
GenPromising.Promising_to_Modelc_pf [in ArchSem.GenPromising]
GenPromising.Promising_to_Modelc [in ArchSem.GenPromising]
GenPromising.Promising_to_Modelnc [in ArchSem.GenPromising]
GenPromising.PState.allowed_promises_tid [in ArchSem.GenPromising]
GenPromising.PState.check_valid_end [in ArchSem.GenPromising]
GenPromising.PState.check_valid_end_tid [in ArchSem.GenPromising]
GenPromising.PState.from_archState [in ArchSem.GenPromising]
GenPromising.PState.nopromises [in ArchSem.GenPromising]
GenPromising.PState.nopromises_tid [in ArchSem.GenPromising]
GenPromising.PState.promise_tid [in ArchSem.GenPromising]
GenPromising.PState.PState_PPState [in ArchSem.GenPromising]
GenPromising.PState.run_tid [in ArchSem.GenPromising]
GenPromising.PState.seq_step [in ArchSem.GenPromising]
GenPromising.PState.step_sind [in ArchSem.GenPromising]
GenPromising.PState.step_ind [in ArchSem.GenPromising]
GenPromising.PState.terminated [in ArchSem.GenPromising]
GenPromising.PState.terminated_tid [in ArchSem.GenPromising]
GenPromising.PState.to_archState [in ArchSem.GenPromising]
GenPromising.PState.tstate [in ArchSem.GenPromising]
I
IMonFromSail.iMon_from_Sail [in ArchSem.FromSail]IMonFromSail.MemReq_from_sail [in ArchSem.FromSail]
IMonFromSail.Sail_outcome_interp [in ArchSem.FromSail]
IMonFromSail.Sail_nochoose [in ArchSem.FromSail]
IMonFromSail.Sail_choose [in ArchSem.FromSail]
Interface.address [in ArchSem.Interface]
Interface.addr_overlap [in ArchSem.Interface]
Interface.addr_in_range [in ArchSem.Interface]
Interface.addr_range [in ArchSem.Interface]
Interface.addr_addN [in ArchSem.Interface]
Interface.f_equal_addr_addN [in ArchSem.Interface]
Interface.get_trans_end [in ArchSem.Interface]
Interface.get_trans_start [in ArchSem.Interface]
Interface.get_exn [in ArchSem.Interface]
Interface.get_tlbi [in ArchSem.Interface]
Interface.get_cacheop [in ArchSem.Interface]
Interface.get_barrier [in ArchSem.Interface]
Interface.get_mem_value [in ArchSem.Interface]
Interface.get_access_kind [in ArchSem.Interface]
Interface.get_size [in ArchSem.Interface]
Interface.get_addr_space [in ArchSem.Interface]
Interface.get_addr [in ArchSem.Interface]
Interface.get_mem_req [in ArchSem.Interface]
Interface.get_rec_acc [in ArchSem.Interface]
Interface.get_reg_val [in ArchSem.Interface]
Interface.get_reg [in ArchSem.Interface]
Interface.iEvent [in ArchSem.Interface]
Interface.iMon [in ArchSem.Interface]
Interface.is_return_exception [in ArchSem.Interface]
Interface.is_take_exceptionP_spec [in ArchSem.Interface]
Interface.is_take_exceptionP [in ArchSem.Interface]
Interface.is_tlbopP_spec [in ArchSem.Interface]
Interface.is_tlbopP [in ArchSem.Interface]
Interface.is_cacheopP_spec [in ArchSem.Interface]
Interface.is_cacheopP [in ArchSem.Interface]
Interface.is_barrierP_spec [in ArchSem.Interface]
Interface.is_barrierP [in ArchSem.Interface]
Interface.is_mem_event_kindP [in ArchSem.Interface]
Interface.is_mem_write_kindP [in ArchSem.Interface]
Interface.is_mem_read_kindP [in ArchSem.Interface]
Interface.is_mem_event [in ArchSem.Interface]
Interface.is_mem_writeP_cdestr [in ArchSem.Interface]
Interface.is_mem_writeP_spec [in ArchSem.Interface]
Interface.is_mem_writeP [in ArchSem.Interface]
Interface.is_mem_write_reqP_cdestr [in ArchSem.Interface]
Interface.is_mem_write_reqP_spec [in ArchSem.Interface]
Interface.is_mem_write_reqP [in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_cdestr [in ArchSem.Interface]
Interface.is_mem_write_addr_announceP_spec [in ArchSem.Interface]
Interface.is_mem_write_addr_announceP [in ArchSem.Interface]
Interface.is_mem_readP_cdestr [in ArchSem.Interface]
Interface.is_mem_readP_spec [in ArchSem.Interface]
Interface.is_mem_readP [in ArchSem.Interface]
Interface.is_mem_read_reqP_cdestr [in ArchSem.Interface]
Interface.is_mem_read_reqP_spec [in ArchSem.Interface]
Interface.is_mem_read_reqP [in ArchSem.Interface]
Interface.is_reg_eventP_cdestr [in ArchSem.Interface]
Interface.is_reg_eventP_spec [in ArchSem.Interface]
Interface.is_reg_eventP [in ArchSem.Interface]
Interface.is_reg_writeP_cdestr [in ArchSem.Interface]
Interface.is_reg_writeP_spec [in ArchSem.Interface]
Interface.is_reg_writeP [in ArchSem.Interface]
Interface.is_reg_readP_cdestr [in ArchSem.Interface]
Interface.is_reg_readP_spec [in ArchSem.Interface]
Interface.is_reg_readP [in ArchSem.Interface]
Interface.is_rel_acq [in ArchSem.Interface]
Interface.iTrace [in ArchSem.Interface]
Interface.MemReq.range [in ArchSem.Interface]
Interface.outcome_sind [in ArchSem.Interface]
Interface.outcome_rec [in ArchSem.Interface]
Interface.outcome_ind [in ArchSem.Interface]
Interface.outcome_rect [in ArchSem.Interface]
ISAManip.global_vars_consistent [in ArchSem.ISAManip]
ISAManip.global_vars_consistent_aux [in ArchSem.ISAManip]
ISAManip.remove_global_vars_traces [in ArchSem.ISAManip]
ISAManip.remove_global_vars_trace_end [in ArchSem.ISAManip]
ISAManip.remove_global_vars [in ArchSem.ISAManip]
ISAManip.remove_global_vars_handler [in ArchSem.ISAManip]
P
PromMemory.attach_timestamps [in ArchSem.GenPromising]PromMemory.cut_after_with_timestamps [in ArchSem.GenPromising]
PromMemory.cut_after [in ArchSem.GenPromising]
PromMemory.cut_before [in ArchSem.GenPromising]
PromMemory.t [in ArchSem.GenPromising]
R
reg_gen_val_sind [in ArchSem.Interface]reg_gen_val_rec [in ArchSem.Interface]
reg_gen_val_ind [in ArchSem.Interface]
reg_gen_val_rect [in ArchSem.Interface]
S
SequentialModel.check_address_space [in ArchSem.SeqModel]SequentialModel.mem_was_written [in ArchSem.SeqModel]
SequentialModel.read_mem_seq_state [in ArchSem.SeqModel]
SequentialModel.read_byte_seq_state [in ArchSem.SeqModel]
SequentialModel.read_reg_seq_state [in ArchSem.SeqModel]
SequentialModel.sequential_modelc [in ArchSem.SeqModel]
SequentialModel.sequential_opmodel [in ArchSem.SeqModel]
SequentialModel.sequential_model_outcome [in ArchSem.SeqModel]
SequentialModel.write_mem_seq_state [in ArchSem.SeqModel]
SequentialModel.write_reg_seq_state [in ArchSem.SeqModel]
T
TermModels.archModel.map_set [in ArchSem.TermModels]TermModels.archModel.Res.equiv [in ArchSem.TermModels]
TermModels.archModel.Res.errors [in ArchSem.TermModels]
TermModels.archModel.Res.finalStates [in ArchSem.TermModels]
TermModels.archModel.Res.flags [in ArchSem.TermModels]
TermModels.archModel.Res.from_exec [in ArchSem.TermModels]
TermModels.archModel.Res.from_result [in ArchSem.TermModels]
TermModels.archModel.Res.no_error [in ArchSem.TermModels]
TermModels.archModel.Res.t_sind [in ArchSem.TermModels]
TermModels.archModel.Res.t_rec [in ArchSem.TermModels]
TermModels.archModel.Res.t_ind [in ArchSem.TermModels]
TermModels.archModel.Res.t_rect [in ArchSem.TermModels]
TermModels.archModel.Res.weaker [in ArchSem.TermModels]
TermModels.archModel.Res.wider [in ArchSem.TermModels]
TermModels.archModel.t [in ArchSem.TermModels]
TermModels.archModel.to_nc [in ArchSem.TermModels]
TermModels.archModel.weaker [in ArchSem.TermModels]
TermModels.archModel.wider [in ArchSem.TermModels]
TermModels.archState.is_terminated [in ArchSem.TermModels]
TermModels.memoryMap [in ArchSem.TermModels]
TermModels.mem_delete [in ArchSem.TermModels]
TermModels.mem_insert [in ArchSem.TermModels]
TermModels.mem_insert_bv [in ArchSem.TermModels]
TermModels.mem_insert_bytes [in ArchSem.TermModels]
TermModels.mem_insert_byte [in ArchSem.TermModels]
TermModels.mem_present [in ArchSem.TermModels]
TermModels.mem_present_nat [in ArchSem.TermModels]
TermModels.mem_lookup [in ArchSem.TermModels]
TermModels.mem_lookup_bytes [in ArchSem.TermModels]
TermModels.mem_lookup_byte [in ArchSem.TermModels]
TermModels.opModel.run [in ArchSem.TermModels]
TermModels.opModel.to_archModel1 [in ArchSem.TermModels]
TermModels.opModel.to_archModel [in ArchSem.TermModels]
TermModels.registerMap [in ArchSem.TermModels]
TermModels.reg_delete [in ArchSem.TermModels]
TermModels.reg_insert [in ArchSem.TermModels]
TermModels.reg_lookup [in ArchSem.TermModels]
TermModels.terminationCondition [in ArchSem.TermModels]
Record Index
C
CandidateExecutions.Candidate.coherence_wf [in ArchSem.CandidateExecutions]CandidateExecutions.Candidate.footprint_wf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.lxsx_wf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.pre [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reads_from_wf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.reg_reads_from_wf [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.t [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.UnfoldEidRels [in ArchSem.CandidateExecutions]
CandidateExecutions.Candidate.wf [in ArchSem.CandidateExecutions]
CandidateExecutions.EID.t [in ArchSem.CandidateExecutions]
G
GenPromising.CPState.EnumerationResult [in ArchSem.GenPromising]GenPromising.Promising.Model [in ArchSem.GenPromising]
GenPromising.PState.t [in ArchSem.GenPromising]
I
Interface.MemReq.t [in ArchSem.Interface]P
PPState.t [in ArchSem.GenPromising]S
SequentialModel.seq_state [in ArchSem.SeqModel]T
TermModels.archState.t [in ArchSem.TermModels]TermModels.opModel.t [in ArchSem.TermModels]
| 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 | (821 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 | (38 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 | (58 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) |
| Axiom 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 | (52 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 | (60 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 | (27 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 | (75 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 | (6 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 | (74 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 | (28 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 | (37 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 | (337 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 | (18 entries) |
This page has been generated by coqdoc