-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy path_CoqProject
More file actions
135 lines (120 loc) · 4.47 KB
/
Copy path_CoqProject
File metadata and controls
135 lines (120 loc) · 4.47 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
-Q theories/ cap_machine
-Q machine_utils/theories/ machine_utils
-arg -w -arg -convert_concl_no_check
-arg -w -arg -several-object-files
-arg -w -arg -ssr-search-moved
-arg -w -arg -deprecated-instance-without-locality
# Machine utils
machine_utils/theories/finz.v
machine_utils/theories/finz_base.v
machine_utils/theories/finz_interval.v
machine_utils/theories/finz_lemmas.v
machine_utils/theories/solve_finz.v
machine_utils/theories/classes.v
machine_utils/theories/class_instances.v
machine_utils/theories/solve_pure.v
machine_utils/theories/tactics.v
# Extras
theories/utils/iris_extra.v
theories/utils/stdpp_extra.v
theories/utils/machine_utils_extra.v
theories/utils/map_simpl.v
theories/utils/NamedProp.v
# Capability Machine Model
theories/opsem/addr_reg.v
theories/proofmode/solve_addr.v
theories/opsem/machine_base.v
theories/opsem/machine_parameters.v
theories/opsem/cap_lang.v
# Program logic: Logical layer
theories/program_logic/logical_mapsto.v
# Misc for automation and notations
theories/proofmode/classes.v
theories/proofmode/class_instances.v
theories/proofmode/solve_addr_extra.v
theories/proofmode/region.v
theories/proofmode/register_tactics.v
# Program logic: Unary WP rules
theories/program_logic/transiently.v
theories/program_logic/wp_opt.v
theories/program_logic/base_logic.v
theories/program_logic/rules_base.v
theories/program_logic/rules_fail.v
theories/program_logic/rules/rules_Get.v
theories/program_logic/rules/rules_Load.v
theories/program_logic/rules/rules_Store.v
theories/program_logic/rules/rules_AddSubLt.v
theories/program_logic/rules/rules_Lea.v
theories/program_logic/rules/rules_Mov.v
theories/program_logic/rules/rules_Restrict.v
theories/program_logic/rules/rules_Jmp.v
theories/program_logic/rules/rules_Jnz.v
theories/program_logic/rules/rules_Subseg.v
theories/program_logic/rules/rules_Seal.v
theories/program_logic/rules/rules_UnSeal.v
theories/program_logic/rules/rules_EInit.v
theories/program_logic/rules/rules_EDeInit.v
theories/program_logic/rules/rules_EStoreId.v
theories/program_logic/rules/rules_IsUnique.v
theories/program_logic/rules/rules_Hash.v
theories/program_logic/rules.v
# Cerise Proofmode
theories/proofmode/contiguous.v
theories/proofmode/tactics_helpers.v
theories/proofmode/solve_pure.v
theories/proofmode/proofmode_instr_rules.v
theories/proofmode/proofmode.v
# Unary Logical Relation
theories/logrel/seal_store.v
theories/logrel/logrel.v
theories/logrel/ftlr/ftlr_base.v
theories/logrel/ftlr/interp_weakening.v
theories/logrel/ftlr/Get.v
theories/logrel/ftlr/Hash.v
theories/logrel/ftlr/Load.v
theories/logrel/ftlr/Store.v
theories/logrel/ftlr/AddSubLt.v
theories/logrel/ftlr/Lea.v
theories/logrel/ftlr/Mov.v
theories/logrel/ftlr/Restrict.v
theories/logrel/ftlr/Jmp.v
theories/logrel/ftlr/Jnz.v
theories/logrel/ftlr/Subseg.v
theories/logrel/ftlr/Seal.v
theories/logrel/ftlr/UnSeal.v
theories/logrel/ftlr/IsUnique.v
theories/logrel/ftlr/EInit.v
theories/logrel/ftlr/EDeInit.v
theories/logrel/ftlr/EStoreId.v
theories/logrel/fundamental.v
# Misc for examples
theories/case_studies/macros/addr_reg_sample.v
theories/proofmode/disjoint_regions_tactics.v
theories/proofmode/mkregion_helpers.v
# Common Cerise (assembly) macros
theories/case_studies/macros/malloc.v
theories/case_studies/macros/assert.v
theories/case_studies/macros/hash_cap.v
theories/case_studies/macros/macros.v
# Template Adequacy
theories/case_studies/template_adequacy_attestation.v
# Secure Outsources Computation (SOC) example
theories/case_studies/soc/soc_code.v
theories/case_studies/soc/soc_enclave_spec.v
theories/case_studies/soc/soc_spec.v
theories/case_studies/soc/soc_adequacy.v
# Trusted Memory Readout example
theories/case_studies/memory_readout/trusted_memory_readout_code.v
theories/case_studies/memory_readout/trusted_memory_readout_spec.v
theories/case_studies/memory_readout/trusted_memory_readout_enclaves_spec.v
theories/case_studies/memory_readout/trusted_memory_readout_client_spec.v
theories/case_studies/memory_readout/trusted_memory_readout_sensor_spec.v
theories/case_studies/memory_readout/trusted_memory_readout_main_spec.v
theories/case_studies/memory_readout/trusted_memory_readout_adequacy.v
# Mutual Attestation example
theories/case_studies/mutual_attestation/mutual_attestation_code.v
theories/case_studies/mutual_attestation/mutual_attestation_A_spec.v
theories/case_studies/mutual_attestation/mutual_attestation_B_spec.v
theories/case_studies/mutual_attestation/mutual_attestation_spec.v
theories/case_studies/mutual_attestation/mutual_attestation_adequacy.v
theories/assumptions.v