secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-L4.verified/lib
History
Gerwin Klein 49f0c84c6e lib: stronger version of mapM_x_commute for True guard 
mapM_x_commute requires "distinct" even if the operations in the mapM
don't require any guards. Add a separate version without distinct when
guard is \top.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2024-10-24 15:33:46 +11:00
..
Basics lib: README.md files for the new sessions 2023-01-25 11:49:59 +11:00
CorresK lib+refine: rename Corres_Method to CorresK_Method 2023-06-30 10:56:47 +10:00
EVTutorial lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Eisbach_Tools lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
Hoare_Sep_Tactics lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
ML_Utils lib: README.md files for the new sessions 2023-01-25 11:49:59 +11:00
Monads lib/monads: resync trace monad with nondet 2024-07-17 13:37:45 +10:00
Word_Lib word_lib: shiftr is always less than max word 2024-09-24 22:24:08 +02:00
clib clib: add ccorres_assert2_abs 2024-07-11 13:36:28 +09:30
concurrency lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
sep_algebra lib+proof+sys-init: more updates for monad changes 2024-07-09 11:24:17 +10:00
test lib: Requalify_Test: add example of requalify-hide-requalify 2024-08-28 15:17:03 +10:00
AddUpdSimps.thy lib AddUpdSimps: cleanup + remove old debugging code 2020-05-04 17:02:58 +08:00
BCorres_UL.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Bisim_UL.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
CorresK_Method.thy lib+proof+sys-init: update for more changed monad lemmas 2024-07-09 11:24:17 +10:00
Corres_Adjust_Preconds.thy lib+proofs+sys-init+tools: proof updates for Fun_Pred_Syntax 2023-01-09 14:54:11 +11:00
Corres_Cases.thy lib+refine: rename Corres_Method to CorresK_Method 2023-06-30 10:56:47 +10:00
Corres_Method.thy lib: factor out is_safe_wp method 2023-08-30 21:59:37 +02:00
Corres_UL.thy lib+proof: move corres_add_noop_rhs and corres_add_noop_rhs2 to Lib 2024-07-11 13:36:28 +09:30
Crunch.ML lib+proof: rename crunches to crunch 2024-07-08 23:02:12 +10:00
Crunch.thy lib+proof: rename crunches to crunch 2024-07-08 23:02:12 +10:00
Crunch_Instances_NonDet.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Crunch_Instances_Trace.thy lib/concurrency: update for changed RG rules 2024-03-27 10:23:40 +11:00
CutMon.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
DataMap.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Defs.thy lib: update old-style "defs" to Isabelle2024 2024-06-12 13:25:18 +10:00
DetWPLib.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Distinct_Cmd.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
EquivValid.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
Eval_Bool.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
ExtraCorres.thy lib: adjust corres_symb_exec_r_conj_ex_abs_forwards 2024-07-15 19:27:16 +09:30
Extract_Conjunct.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
FP_Eval.thy lib: always prefer Main to HOL.HOL import 2023-01-25 11:48:38 +11:00
FastMap.thy isabelle2021-1 lib: update Lib session, retire wpx 2022-03-29 08:38:25 +11:00
Find_Names.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
GenericLib.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
GenericTag.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Guess_ExI.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
HaskellLemmaBucket.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
HaskellLib_H.thy monads/reader_option: add ostate_assert 2024-07-11 13:36:28 +09:30
Heap_List.thy lib: add heap_ls_neighbour_in_set 2024-04-08 21:11:09 +09:30
Injection_Handler.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Insulin.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
LemmaBucket.thy lib: add filter_hd_equals_tl to LemmaBucket 2024-04-08 21:11:09 +09:30
LexordList.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Lib.thy lib: add variation on mod_less_eq_dividend 2024-07-05 18:02:52 +10:00
ListLibLemmas.thy lib: add list lemmas to Lib and ListLibLemmas 2024-02-26 21:23:09 +10:30
List_Lib.thy lib: add defn of list_insert_before, and some lemmas 2024-01-15 18:08:12 +10:30
Locale_Abbrev.thy isabelle-2021: Lib update 2021-09-30 16:53:17 +10:00
ML_Goal.thy lib: Isabelle2023 update 2023-10-06 14:29:15 +11:00
ML_Goal_Test.thy lib+tools: MLUtils -> ML_Utils for consistency 2023-01-20 13:43:39 +11:00
Match_Abbreviation.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
Monad_Commute.thy lib: stronger version of mapM_x_commute for True guard 2024-10-24 15:33:46 +11:00
Monad_Lists.thy lib+proof+sys-init: update for more changed monad lemmas 2024-07-09 11:24:17 +10:00
MonadicRewrite.thy lib: generic monadic_rewrite_state_assert/stateAssert 2024-03-25 13:36:09 +01:00
More_Numeral_Type.thy isabelle-2021: ad-hoc adjustions to preview 2021-09-30 16:53:17 +10:00
NICTATools.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Named_Eta.thy lib: add named_eta and no_name_eta methods 2022-09-06 02:50:23 +10:00
NonDetMonadLemmaBucket.thy lib+spec+proof+tools: update for reader_option refactor 2024-03-01 12:03:30 +11:00
None_Top_Bot.thy lib: consistent naming in None_Top_Bot 2024-03-16 09:36:40 +01:00
Oblivious.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Qualify.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
ROOT lib: migrate Requalify tests into test/ 2024-07-23 16:47:33 +10:00
RangeMap.thy lib: make ML_Utils a separate session 2023-01-20 13:43:39 +11:00
Repeat_Attribute.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
Requalify.thy lib: Requalify: better document annotation 2024-08-28 15:17:03 +10:00
Rules_Tac.thy lib: add rules_tac and related multi-thm instantiators 2022-09-10 06:29:19 +10:00
ShowTypes.thy cleanup: reduce warnings 2021-09-30 16:53:17 +10:00
SimpStrategy.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
Simulation.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Solves_Tac.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
SpecValid_R.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
SplitRule.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
StateMonad.thy lib: factor out and generalise bool syntax for functions 2023-01-09 14:54:06 +11:00
SubMonadLib.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
Time_Methods_Cmd.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Try_Attribute.thy lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
Try_Methods.thy lib: theory import fixes for new sessions 2023-01-24 11:30:05 +11:00
Value_Abbreviation.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Value_Type.thy lib: produce _def and _val thms in value_type 2024-04-10 19:30:04 +10:00
crunch-cmd.ML lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 2024-06-12 13:25:18 +10:00
defs.ML lib: update old-style "defs" to Isabelle2024 2024-06-12 13:25:18 +10:00
set.ML licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
tests.xml lib: A tutorial and some 'modify' monad rules for Lib.EquivValid 2020-11-17 06:06:03 +11:00