Files

 main

/

theories

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

Aina Linn Georges

and

Aina Linn Georges

fixed load paths

Jul 7, 2020

c225fe6 · Jul 7, 2020

History

History

/

theories

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
attic		attic	delete some dead (not useful) files, modified lse such that it compil…	Jul 6, 2020
examples		examples	fixed load paths	Jul 7, 2020
ftlr		ftlr	Move parameters over encoding/decoding to a typeclass, + a bunch of r…	Jul 1, 2020
rules		rules	Move lemmas from the adequacy proof to auxiliary files	Jul 6, 2020
addr_reg.v		addr_reg.v	Cleanup & move lemmas around	Jul 6, 2020
cap_lang.v		cap_lang.v	Fully concrete scenario, with a concrete adversarial code: it runs!	Jul 2, 2020
fundamental.v		fundamental.v	Move lemmas from the adequacy proof to auxiliary files	Jul 6, 2020
iris_extra.v		iris_extra.v	Cleanup & move lemmas around	Jul 6, 2020
logrel.v		logrel.v	Move parameters over encoding/decoding to a typeclass, + a bunch of r…	Jul 1, 2020
machine_base.v		machine_base.v	Fully concrete scenario, with a concrete adversarial code: it runs!	Jul 2, 2020
machine_parameters.v		machine_parameters.v	Version of the adequacy theorem with a concrete machine & layout	Jul 2, 2020
machine_run.v		machine_run.v	Fully concrete scenario, with a concrete adversarial code: it runs!	Jul 2, 2020
mono_ref.v		mono_ref.v	replaced memory points to predicates with capability predicates, usin…	Sep 2, 2019
monocmra.v		monocmra.v	work towards an scall spec	Jan 31, 2020
monotone.v		monotone.v	moved lemmas into appropriate files	Jul 6, 2020
multiple_updates.v		multiple_updates.v	Remove old commented code	Jul 6, 2020
region.v		region.v	Cleanup & move lemmas around	Jul 6, 2020
region_invariants.v		region_invariants.v	Cleanup & move lemmas around	Jul 6, 2020
region_invariants_allocation.v		region_invariants_allocation.v	Move lemmas from the adequacy proof to auxiliary files	Jul 6, 2020
region_invariants_revocation.v		region_invariants_revocation.v	Cleanup & move lemmas around	Jul 6, 2020
region_invariants_static.v		region_invariants_static.v	Cleanup & move lemmas around	Jul 6, 2020
region_invariants_uninitialized.v		region_invariants_uninitialized.v	Move lemmas from the adequacy proof to auxiliary files	Jul 6, 2020
stdpp_extra.v		stdpp_extra.v	Cleanup & move lemmas around	Jul 6, 2020
sts.v		sts.v	Cleanup & move lemmas around	Jul 6, 2020
View all files