-
Notifications
You must be signed in to change notification settings - Fork 123
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
Have only one Arch_assms per architecture, use it and new tech to bypass Arch interpretation during instantiation.
arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependentStatus: Open.#1044 In seL4/l4v;Adjust lemmas named Arch_ in Refine
arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependentStatus: Open.#1042 In seL4/l4v;The
wpsmethod should include awp_prestepproof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofsStatus: Open.#1019 In seL4/l4v;hoare_vcg_prop (in default wp set) throws away non-throw information
proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofsproof toolsconvenience, automation, productivity toolsconvenience, automation, productivity toolsStatus: Open.#1007 In seL4/l4v;detect and handle attribute
packedC-parseranything about the C/Simpl parseranything about the C/Simpl parserStatus: Open.#994 In seL4/l4v;- Status: Open.#990 In seL4/l4v;
- Status: Open.#988 In seL4/l4v;
A place for folded machine_word_len lemmas
arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependentproof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofsStatus: Open.#984 In seL4/l4v;- Status: Open.#955 In seL4/l4v;
- Status: Open.#954 In seL4/l4v;
crunch bundles
proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofsproof toolsconvenience, automation, productivity toolsconvenience, automation, productivity toolsStatus: Open.Intelligently create a bundle that hides word lemmas which expose LENGTH('a)
arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependentStatus: Open.#929 In seL4/l4v;