@@ -91,37 +91,37 @@ theories/ftlr/EStoreId.v
9191theories/fundamental.v
9292
9393# Misc for examples
94- theories/examples/addr_reg_sample.v
94+ theories/examples/macros/ addr_reg_sample.v
9595theories/proofmode/disjoint_regions_tactics.v
9696theories/proofmode/mkregion_helpers.v
9797
9898# Common Cerise (assembly) macros
99- theories/examples/malloc.v
100- theories/examples/assert.v
101- theories/examples/hash_cap.v
102- theories/examples/macros.v
99+ theories/examples/macros/ malloc.v
100+ theories/examples/macros/ assert.v
101+ theories/examples/macros/ hash_cap.v
102+ theories/examples/macros/macros .v
103103
104104# Template Adequacy
105- theories/examples/enclaves/ template_adequacy_attestation.v
105+ theories/examples/template_adequacy_attestation.v
106106
107107# Trusted Compute example
108- theories/examples/enclaves /trusted_compute_code.v
109- theories/examples/enclaves /trusted_compute_enclave_spec.v
110- theories/examples/enclaves /trusted_compute_spec.v
111- theories/examples/enclaves /trusted_compute_adequacy.v
108+ theories/examples/soc /trusted_compute_code.v
109+ theories/examples/soc /trusted_compute_enclave_spec.v
110+ theories/examples/soc /trusted_compute_spec.v
111+ theories/examples/soc /trusted_compute_adequacy.v
112112
113113# Trusted Memory Readout example
114- theories/examples/enclaves /trusted_memory_readout_code.v
115- theories/examples/enclaves /trusted_memory_readout_spec.v
116- theories/examples/enclaves /trusted_memory_readout_enclaves_spec.v
117- theories/examples/enclaves /trusted_memory_readout_client_spec.v
118- theories/examples/enclaves /trusted_memory_readout_sensor_spec.v
119- theories/examples/enclaves /trusted_memory_readout_main_spec.v
120- theories/examples/enclaves /trusted_memory_readout_adequacy.v
114+ theories/examples/memory_readout /trusted_memory_readout_code.v
115+ theories/examples/memory_readout /trusted_memory_readout_spec.v
116+ theories/examples/memory_readout /trusted_memory_readout_enclaves_spec.v
117+ theories/examples/memory_readout /trusted_memory_readout_client_spec.v
118+ theories/examples/memory_readout /trusted_memory_readout_sensor_spec.v
119+ theories/examples/memory_readout /trusted_memory_readout_main_spec.v
120+ theories/examples/memory_readout /trusted_memory_readout_adequacy.v
121121
122122# Mutual attestation example
123- theories/examples/enclaves /mutual_attestation_code.v
124- theories/examples/enclaves /mutual_attestation_A_spec.v
125- theories/examples/enclaves /mutual_attestation_B_spec.v
126- theories/examples/enclaves /mutual_attestation_spec.v
127- theories/examples/enclaves /mutual_attestation_adequacy.v
123+ theories/examples/mutual_attestation /mutual_attestation_code.v
124+ theories/examples/mutual_attestation /mutual_attestation_A_spec.v
125+ theories/examples/mutual_attestation /mutual_attestation_B_spec.v
126+ theories/examples/mutual_attestation /mutual_attestation_spec.v
127+ theories/examples/mutual_attestation /mutual_attestation_adequacy.v
0 commit comments