Skip to content

Issues: seL4/l4v

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

40 Open 48 Closed
40 Open 48 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Investigate further use of none_top/none_bot in the proofs enhancement proof engineering nicer, shorter, more maintainable etc proofs
#751 opened May 1, 2024 by michaelmcinerney
Decide on style for [def]rule_tac ... [and ...] in ... proof engineering nicer, shorter, more maintainable etc proofs
#746 opened Mar 28, 2024 by Xaphiosis
2
Some way of blocking simp from unifying schematics proof engineering nicer, shorter, more maintainable etc proofs proof tools convenience, automation, productivity tools
#730 opened Mar 7, 2024 by Xaphiosis
1
Have wp warn when resulting in a goal with a schematic assumption. proof engineering nicer, shorter, more maintainable etc proofs proof tools convenience, automation, productivity tools
#729 opened Mar 7, 2024 by Xaphiosis
15
Sub-term to free variable lifting tactic proof engineering nicer, shorter, more maintainable etc proofs proof tools convenience, automation, productivity tools
#727 opened Mar 1, 2024 by Xaphiosis
Safer vcg in CRefine enhancement proof engineering nicer, shorter, more maintainable etc proofs
#726 opened Mar 1, 2024 by Xaphiosis
Methods such as monadic_rewrite_symb_exec_r should warn that discharging side-conditions failed enhancement proof engineering nicer, shorter, more maintainable etc proofs
#715 opened Feb 15, 2024 by Xaphiosis
SIMPL: don't print _'proc C-parser anything about the C/Simpl parser enhancement
#710 opened Jan 23, 2024 by lsf37
Document mysterious useful comments for ctac and ceqv cleanup docs Documentation, READMEs, etc
#692 opened Oct 27, 2023 by Xaphiosis
@Xaphiosis
Cleanup post-x64 comments cleanup proof engineering nicer, shorter, more maintainable etc proofs
#691 opened Oct 27, 2023 by Xaphiosis
Cleanup CRefine Wellformed_C cleanup proof engineering nicer, shorter, more maintainable etc proofs
#690 opened Oct 27, 2023 by Xaphiosis
Remove instances of UNIV <\inter> from CRefine cleanup proof engineering nicer, shorter, more maintainable etc proofs
#688 opened Oct 25, 2023 by Xaphiosis
Investigate adding projectKOs to the simp set
#687 opened Oct 23, 2023 by michaelmcinerney
1
should corres_cases also do case distinction on if? proof engineering nicer, shorter, more maintainable etc proofs proof tools convenience, automation, productivity tools question
#652 opened Jun 26, 2023 by lsf37
does ccorres need a corres_cases equivalent? proof engineering nicer, shorter, more maintainable etc proofs proof tools convenience, automation, productivity tools question
#651 opened Jun 26, 2023 by lsf37
investigate parallelising the haskell translator proof tools convenience, automation, productivity tools
#635 opened May 24, 2023 by lsf37
Investigate greater use of heap projections in Invariants_H.thy
#633 opened May 16, 2023 by michaelmcinerney
Move lemmas to CParser C-parser anything about the C/Simpl parser cleanup proof engineering nicer, shorter, more maintainable etc proofs
#631 opened May 1, 2023 by michaelmcinerney
restyle Platform.thy for all architectures cleanup proof engineering nicer, shorter, more maintainable etc proofs
#620 opened Mar 28, 2023 by lsf37
rename kernel_base to pptrBase cleanup proof engineering nicer, shorter, more maintainable etc proofs
#619 opened Mar 28, 2023 by lsf37
our bit_simps shadows Word_Lib bit_simps cleanup
#600 opened Mar 8, 2023 by lsf37
abs_typ_at_lifts should have an arch variant proof engineering nicer, shorter, more maintainable etc proofs
#599 opened Mar 8, 2023 by lsf37
1
Make if_1_0_0 lemmas consistent cleanup
#579 opened Feb 14, 2023 by corlewis
2
factor out more VCPU lemmas Aarch64 AArch64-specific proofs, specs, etc cleanup
#571 opened Feb 5, 2023 by lsf37
should corres_underlying imply failure preservation? cleanup proof engineering nicer, shorter, more maintainable etc proofs
#528 opened Oct 17, 2022 by lsf37
ProTip! Exclude everything labeled bug with -label:bug.