Skip to content
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.

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

MCS: merge master into rt #680

Merged
merged 207 commits into from
Oct 13, 2023
Merged
Changes from 1 commit
Commits
Show all changes
207 commits
Select commit Hold shift + click to select a range
2545aa0
github: add manual triggers for testing
lsf37 Mar 30, 2023
59bf9d9
docs: style: right- vs left-wrapping of operators
Xaphiosis Jan 20, 2023
0794e0a
run_tests: enable BaseRefine for AARCH64
Xaphiosis May 3, 2023
1483554
aarch64 refine: first attempt at Invariants_H
Xaphiosis May 5, 2023
01575f2
aarch64 refine: copy InvariantUpdates_H from RISCV64
Xaphiosis May 5, 2023
1404b9c
aarch64 refine: add StateRelation
Xaphiosis May 8, 2023
96851e8
aarch64 ainvs: fix typo
lsf37 May 8, 2023
44fc3ec
aarch64 refine: copy LevityCatch from RISCV64
lsf37 May 8, 2023
0b0b3b3
aarch64 refine: iteration on Invariants_H
lsf37 May 8, 2023
394f74b
aarch64 aspec: sync vmid bit width with Haskell+C
lsf37 May 10, 2023
9f25a4e
aarch64 haskell: use ppn concept for PageTablePTEs
lsf37 May 10, 2023
55a01f1
aarch64 refine: complete StateRelation
lsf37 May 10, 2023
61bce83
aarch64 refine: copy Corres.thy from RISCV64
lsf37 May 10, 2023
bf3929b
aarch64 refine: adjust Bits_R from RISCV64
lsf37 May 10, 2023
7cdb85f
aarch64 refine: copy EmptyFail from RISCV64
lsf37 May 10, 2023
555bff6
aarch64 refine: copy SubMonad_R from RISCV64
lsf37 May 10, 2023
b882216
aarch64 refine: copy Machine_R from RISCV64
lsf37 May 10, 2023
38a65fd
aarch64 refine: adjust KHeap_R from RISCV64
lsf37 May 10, 2023
b426654
aarch64 refine: use ptTranslationBits for indices
lsf37 May 11, 2023
3b5a983
aarch64 refine: first pass through ArchAcc_R
lsf37 May 11, 2023
e0114ee
aarch64 refine: add CSpace_I and CSpace1_R
Xaphiosis May 15, 2023
a93a626
aarch64 refine: copy RAB_FN from RISCV64
Xaphiosis May 16, 2023
18d76ef
aarch64 refine: add vcpuBits_def to objBits_defs
Xaphiosis May 16, 2023
2b543da
aarch64 refine: add CSpace_R
Xaphiosis May 16, 2023
cb03631
aarch64 refine: add TcbAcc_R and ArchMove_R
Xaphiosis May 16, 2023
059afc8
aarch64 refine: add InterruptAcc_R
Xaphiosis May 16, 2023
97ebd07
aarch64 refine: start on VSpace_R
Xaphiosis May 16, 2023
0f11a7a
aarch64 refine: progress in ArchAcc
lsf37 May 16, 2023
a79e06f
aarch64 refine: first run through VSpace_R
Xaphiosis May 17, 2023
9040568
aarch64 refine: add state_hyp_refs_of' to valid_state'
Xaphiosis May 18, 2023
044a97e
aarch64 refine: first run through Schedule_R
Xaphiosis May 18, 2023
3a77d09
aarch64 refine: first pass through IpcCancel_R
Xaphiosis May 18, 2023
e508693
aarch64 refine: first pass through Retype_R
Xaphiosis May 18, 2023
a4536a1
aarch64 refine: first pass through Detype_R
Xaphiosis May 18, 2023
5601abc
aarch64 refine: fill in VSpaceObject cases in Retype_R
lsf37 May 19, 2023
f4c12a6
aarch64 refine: remove kernel_mappings in Retype/Detype
lsf37 May 19, 2023
0a7eaec
aarch64 refine: copy over Invocations_R from RISCV64
lsf37 May 19, 2023
be22c7b
aarch64 refine: set up Untyped_R from RISCV64, add hyp/vcpu
lsf37 May 19, 2023
4dfb6f8
aarch64 refine: first pass through Finalise_R
Xaphiosis May 19, 2023
865facf
aarch64 refine: first pass through Ipc_R
lsf37 May 19, 2023
835d82c
aarch64 refine: first pass through Interrupt_R
lsf37 May 19, 2023
4834c25
aarch64 refine: first pass through CNodeInv_R
lsf37 May 19, 2023
f3bbd47
aarch64 haskell: prefer fail over error
lsf37 May 19, 2023
a88bf41
aarch64 refine: remove 1 sorry
lsf37 May 19, 2023
20fad5b
aarch64 refine: update vmattributes_map for devices
Xaphiosis May 21, 2023
8de1430
aarch64 refine: first pass through Tcb_R
lsf37 May 22, 2023
7cea1dc
aarch64 aspec: attribs_from_word used wrong bits
Xaphiosis May 22, 2023
7ed8476
aarch64 haskell: update decodeARMASIDPoolInvocation
Xaphiosis May 22, 2023
226c2f6
aarch64 refine: first pass through Arch_R
Xaphiosis May 21, 2023
59d303b
aarch64 refine: first pass through Syscall_R
lsf37 May 22, 2023
ee346ba
aarch64 refine: first pass though Init_R
Xaphiosis May 23, 2023
72dfb53
aarch64 refine: copy IncKernelLemmas+InitLemmas from RISCV64
Xaphiosis May 23, 2023
c58c007
aarch64 refine: copy KernelInit_R from RISCV64
Xaphiosis May 24, 2023
a4f944d
aarch64 refine: copy PageTableDuplicates from RISCV64
lsf37 May 22, 2023
e0ae44a
aarch64 haskell+design: record PT types in ghost state
lsf37 May 24, 2023
064d102
aarch64 ainvs+refine: proof updates for PT type ghost state
lsf37 May 24, 2023
d24d2f8
aarch64 refine: first pass through ADT_H
lsf37 May 24, 2023
aa2eb9a
design: fix ExecSpec for other architectures
lsf37 May 24, 2023
9298456
refine: update other architectures for ghost state change
lsf37 May 25, 2023
c4dee68
aarch64: update Init_R+PageTableDuplicates for PT ghost state
Xaphiosis May 25, 2023
7154cc9
aarch64 refine: remove final mention of vs_valid_duplicates'
Xaphiosis May 25, 2023
81d382e
aarch64 refine: first pass through Refine (sorry-free)
Xaphiosis May 25, 2023
2f3e333
aarch64 refine: first pass through EmptyFail_H (sorry-free)
Xaphiosis May 25, 2023
7b73a18
run_tests: enable Refine (quick_and_dirty) for AARCH64
Xaphiosis May 25, 2023
496f70f
run_tests: fix QUICK_AND_DIRTY handling
Xaphiosis May 25, 2023
7cdd203
aarch64 refine: first run through Orphanage
Xaphiosis May 25, 2023
381ad05
run_tests: enable RefineOrphanage for AARCH64
Xaphiosis May 25, 2023
1e61943
proof/ROOT: RefineOrphanage: add quick and dirty option
Xaphiosis May 25, 2023
971be5f
haskell: constrain run_tests to current L4V_ARCH
lsf37 May 31, 2023
7c422d7
cspec: introduce L4V_PLAT
lsf37 Jun 2, 2023
c4d673b
cspec: Use L4V_PLAT in build export script
mbrcknl Jun 2, 2023
fc44f65
aspec+haskell: add accessor names for scheduler_action datatype
michaelmcinerney Mar 21, 2023
6da2d97
run_tests: echo L4V_FEATURES and L4V_PLAT
lsf37 Jun 6, 2023
290b7c7
run_tests: update outdated comment
lsf37 Jun 6, 2023
9752444
run_tests: REFINE_QUICK_AND_DIRTY already set in Makefile
lsf37 Jun 6, 2023
443706f
github: distinguish proof PR checks from deployment run
lsf37 Jun 6, 2023
9fe1676
github: auto-rebase platform branches
lsf37 Jun 5, 2023
6f2ea86
github: push to -rebased branch first
lsf37 Jun 6, 2023
ea62a6c
lib: docs + 2nd predicate-type guard for wpc
lsf37 Jun 13, 2023
0e30162
lib+proof: proof updates for wpc change
lsf37 Jun 13, 2023
29873da
lib: split out WP_Pre.pre_tac for wp_pre
lsf37 Jun 9, 2023
f75a348
lib+refine+crefine: disambiguate corres_pre
lsf37 Jun 9, 2023
db44def
arm-hyp crefine: use monadic_rewrite_pre
lsf37 Jun 15, 2023
f72702f
lib: monadic rewrite: improve bound name retention
Xaphiosis Jun 13, 2023
ec907bf
lib: add test for monadic rewrite
Xaphiosis Jun 13, 2023
18cbdae
infoflow: update for monadic rewrite changes
Xaphiosis Jun 13, 2023
460d99b
haskell: upgrade to lts-20.25 and ghc 9.2.8
lsf37 Jun 18, 2023
dc093ca
github: use explicit token to enable push triggers
lsf37 Jun 21, 2023
722cd25
github: use correct secret
lsf37 Jun 21, 2023
5abb456
lib: add corres_cases method
lsf37 Jun 22, 2023
168d3aa
crefine: remove obsolete corres wpc setup
lsf37 Jun 22, 2023
59759ed
arm refine: deploy corres_cases in some examples
lsf37 Jun 23, 2023
163b9fe
crefine: remove some duplicated lemmas
corlewis Jun 26, 2023
0edd68f
lib: cong rules for ccorres_underlying
corlewis Jun 19, 2023
1f06802
crefine: update for new ccorres cong rules
corlewis Jun 19, 2023
c1fe4ad
lib+refine: rename Corres_Method to CorresK_Method
lsf37 Jun 26, 2023
865df55
lib: add new corres method
lsf37 Jun 26, 2023
445a8e4
lib: cleanup in Corres_UL and around liftM in Monads
lsf37 Jun 27, 2023
691c9e2
lib: some remarks on corres_mapM*
lsf37 Jun 29, 2023
fad4b70
refine: make corres method available in Refine
lsf37 Jun 26, 2023
01a4216
riscv refine: example corres method use
lsf37 Jun 29, 2023
a0be68c
clib+crefine: add no_name_eta to crefine tactics
corlewis Jun 30, 2023
d87f5e1
crefine: update for no_name_eta
corlewis Jun 30, 2023
fa484da
monads: synchronise with rt branch
corlewis Jul 4, 2023
c9dc6d2
docs/setup: add step for installing cabal
corlewis Jul 18, 2023
26f41e1
lib/monads: rename OptionMonad to Reader_Option_Monad
corlewis Jul 7, 2023
9b90b9e
lib+spec+proof+autocorres: update for renamed Reader_Option_Monad
corlewis Jul 7, 2023
9b9e613
lib/monads: move different monads to subdirectories
corlewis Jul 7, 2023
2c8f9ee
lib+spec+proof+autocorres: consistent Nondet filename prefix
corlewis Jul 18, 2023
67946d4
lib: consistent Trace filename prefix
corlewis Jul 18, 2023
aa8b108
lib/monads: reorder files in ROOT
corlewis Jul 19, 2023
0e0e0ca
lib/monads: add select_wp and alternative_wp to wp set for Nondet monad
corlewis Aug 1, 2023
0211681
proof+autocorres: update for select_wp and alternative_wp
corlewis Aug 1, 2023
f6eaad5
arm abstract+design: reorder object_type enum
lsf37 Aug 11, 2023
f7c3ee5
drefine: adjust for object_type enum reorder
lsf37 Aug 11, 2023
71dc79a
arm crefine: proof updates for object_type enum reorder
lsf37 Aug 11, 2023
540bb64
arm-hyp abstract+design: object_type enum reorder
lsf37 Aug 11, 2023
4d97b26
arm-hyp crefine: proof update for object_type enum reorder
lsf37 Aug 11, 2023
631bc30
lib/monads: move lifting/splitting section earlier in Nondet_VCG
corlewis Aug 9, 2023
fde22d7
lib/monads: minor cleanup and restyle in nondet monad
corlewis Aug 9, 2023
a084de4
refine: update for changes to nondet monad
corlewis Aug 14, 2023
477e8d2
lib/monads: restyle Trace_Monad.thy
corlewis Jul 19, 2023
380520c
lib/monads: refactor trace monad theories
corlewis Jul 19, 2023
6dbcf40
lib/monads: split content out into Trace_RG and Trace_No_Trace
corlewis Aug 14, 2023
4a44874
lib/monads: restyle and reorder trace monad files
corlewis Aug 14, 2023
917fff5
lib: update for trace monad refactor
corlewis Aug 14, 2023
1482841
lib: add a breakpoint for corres_cleanup
lsf37 Jun 30, 2023
51ebfd6
lib: enforce simp (no_asm) in Corres_Method
lsf37 Jun 30, 2023
7595c02
riscv refine: adjust for (no_asm) in Corres_Method
lsf37 Jul 1, 2023
f80d7f8
lib: on the use of corres_liftM_simp rules
lsf37 Aug 30, 2023
0969196
lib: factor out is_safe_wp method
lsf37 Aug 30, 2023
c4369f5
lib: add docs and test for Corres_Method
lsf37 Aug 30, 2023
deade60
crefine: change misleading proof step in CSpace_RAB_C
Xaphiosis Sep 14, 2023
322f4f9
aarch64 refine: remove pspace_canonical'
lsf37 Jun 6, 2023
6e57667
aarch64 refine: invariant update lemmas
lsf37 Sep 27, 2023
7ae4e55
aarch64 refine: ArchAcc_R sorry free
lsf37 Jun 6, 2023
c77d649
aarch64 aspec: sync with Haskell
lsf37 Jun 7, 2023
d16b4fd
aarch64 ainvs: new invariant on vmid_table
lsf37 Jul 3, 2023
345818d
aarch64 aspec: cleanByVA_PoU in perform_pg_inv_map
lsf37 Jul 4, 2023
7713dff
aarch64 ainvs: updates for spec change
lsf37 Jul 4, 2023
438e27a
aarch64 aspec: fix do_flush spec bug
lsf37 Jul 5, 2023
c628181
aarch64 aspec+ainvs: add valid_asid_map invariant
lsf37 Jul 4, 2023
d16d35e
aarch64 refine: VSpace_R sorry-free
lsf37 Jul 3, 2023
f14217e
aarch64 refine: progress in Retype_R
lsf37 Jul 17, 2023
e74d5fe
aarch64 refine: progress in Retype_R
lsf37 Jul 18, 2023
4913aa8
aarch64 haskell: tweak createNewCaps definition
lsf37 Jul 18, 2023
2ec696f
aarch64 refine: Retype_R sorry-free
lsf37 Jul 18, 2023
1ea097a
aarch64 refine: Untyped_R sorry-free
lsf37 Jul 18, 2023
1f60044
aarch64 refine: Schedule_R sorry-free
lsf37 Jul 19, 2023
73ba0ce
aarch64 refine: IpcCancel_R sorry-free
lsf37 Jul 20, 2023
522cef1
aarch64 refine: Finalise_R sorry-free
lsf37 Jul 21, 2023
0e8048b
aarch64 aspec+ainvs: sync user_vtop check with C
lsf37 Jul 23, 2023
d849c0b
aarch64 haskell: fix syscall arg error reporting
lsf37 Jul 23, 2023
e2355c7
aarch64 haskell: check cap type in checkVSpaceRoot
lsf37 Jul 23, 2023
1fb96c7
aarch64 ainvs: mark addrFromPPtr_mask_ipa
lsf37 Jul 23, 2023
c745d4e
aarch64 aspec: fix flush type in decode_vspace_invocation
lsf37 Jul 23, 2023
da76bca
aarch64 refine: Arch_R sorry-free
lsf37 Jul 23, 2023
1f05109
aarch64 refine: Ipc_R sorry-free
lsf37 Jul 26, 2023
a0311bd
aarch64 refine: Interrupt_R sorry-free
lsf37 Jul 26, 2023
ffd038f
aarch64 refine: ADT_H sorry-free
lsf37 Jul 27, 2023
1fde048
aarch64 refine: progress in Detype_R
lsf37 Jul 28, 2023
8f2710d
aarch64 refine: Detype_R sorry-free
lsf37 Aug 9, 2023
2e3c97d
aarch64 refine: Orphanage sorry-free
Xaphiosis Aug 10, 2023
cf0e636
aarch64 refine: resolve trivial FIXMEs
lsf37 Aug 22, 2023
43c0759
aarch64 refine: leave comment instead of FIXME
lsf37 Aug 22, 2023
6bfdecd
aarch64 refine: defer some FIXMEs to CRefine
lsf37 Aug 22, 2023
c263749
aarch64 refine: consolidate dmo_invs_no_cicd' lemmas
lsf37 Aug 23, 2023
62618fc
aarch64 refine: improve decode invariance crunch
lsf37 Aug 23, 2023
4c69a42
lib: fix ML warning
lsf37 Aug 24, 2023
6793a94
lib: move lemmas from refine/AARCH64/ArchAcc
lsf37 Aug 24, 2023
5f74194
aarch64 refine: move lemmas to lib
lsf37 Aug 24, 2023
9f7e8f8
word_lib: anti-monotonicity of shiftr
lsf37 Aug 24, 2023
fe3ebf0
lib: lemmas moved from aarch64 refine
lsf37 Aug 24, 2023
dc4955d
aarch64 refine: lemma moved to Word_Lib
lsf37 Aug 24, 2023
2251bf8
aarch64 refine: lemmas moved to lib
lsf37 Aug 24, 2023
26a3a6e
aarch64 refine: lemmas moved to aarch64 ainvs
lsf37 Aug 24, 2023
a24ddbe
aarch64 refine: move lemmas internally
lsf37 Aug 24, 2023
de50741
lib+aarch64 refine: move lemmas to lib
lsf37 Aug 24, 2023
0369a4b
lib+ainvs+aarch64 refine: move+consolidate vcg_op_lift lemmas
lsf37 Aug 24, 2023
dcf6ee4
aarch64 ainvs+refine: move lemmas from Refine
lsf37 Aug 28, 2023
5497666
aarch64 ainvs+refine: remove unused dom_ucast_eq
lsf37 Aug 28, 2023
df31523
lib/monads: more cleanup and restyle in nondet monad
corlewis Aug 18, 2023
7999632
proof: update for changes to nondet monad
corlewis Aug 18, 2023
d66ac95
lib/monads/trace: copy in definitions and rules from nondet
corlewis Aug 24, 2023
0aac7ac
lib/monads/trace: update definitions and rules taken from nondet
corlewis Aug 24, 2023
293b97c
lib/monads/trace: prove more lemmas connecting valid and validI
corlewis Aug 24, 2023
3333395
lib/monads: improve style of nondet and trace
corlewis Oct 5, 2023
34038fc
lib/monads/nondet: remove uses of _tac methods
corlewis Sep 20, 2023
6680297
lib/monads: add no_fail_ex_lift and no_fail_grab_asm
michaelmcinerney Oct 5, 2023
e7cca6a
lib: improve corres_underlying rules for whileLoop
michaelmcinerney Oct 5, 2023
6721c7a
lib: sync Word_Lib with AFP
lsf37 Sep 1, 2023
3f66cb0
lib/Eisbach_Tools: morphism type changed in Isabelle2023
lsf37 Sep 1, 2023
eeae2af
lib: Isabelle2023 update
lsf37 Sep 1, 2023
286278d
misc: goto-error jEdit macro: update for 2023
Xaphiosis Sep 6, 2023
450234e
aspec: mapsto syntax update for Isabelle2023
lsf37 Sep 13, 2023
83fc513
c-parser: sync Simpl from AFP for Isabelle2023
lsf37 Sep 15, 2023
be44fad
c-parser: update to Isabelle2023 maps-to syntax
lsf37 Sep 15, 2023
26807f7
c-parser: adapt standalone parser to Isabelle2023
lsf37 Sep 18, 2023
f88d2d4
clib: update to Isabelle2023 mapsto syntax
lsf37 Sep 16, 2023
3141584
proof: update to Isabelle2023 mapsto syntax
lsf37 Sep 16, 2023
f7768ee
sep-capDL: update to Isabelle2023 mapsto syntax
lsf37 Sep 16, 2023
4c0b3df
capdDL-api: update to Isabelle2023 mapsto syntax
lsf37 Sep 16, 2023
0f99a75
autocorres: update to Isabelle2023
lsf37 Sep 16, 2023
0d984f3
camkes: update to Isabelle2023 mapsto syntax
lsf37 Sep 16, 2023
ad24d95
word lib: fix broken style introduced from AFP
lsf37 Oct 6, 2023
3036f22
Merge branch 'master' into rt
corlewis Oct 11, 2023
3308a0b
rt proof: update for merge
corlewis Oct 11, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
lib/monads: restyle and reorder trace monad files
Signed-off-by: Corey Lewis <[email protected]>
corlewis committed Aug 23, 2023
commit 4a44874a26beb6414149a249ae4e1b50e14f42d1
69 changes: 39 additions & 30 deletions lib/Monads/trace/Trace_Monad.thy
Original file line number Diff line number Diff line change
@@ -41,9 +41,9 @@ abbreviation map_tmres_rv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a) tmres
section "The Monad"

text \<open>
tmonad returns a set of non-deterministic computations, including
tmonad returns a set of non-deterministic computations, including
a trace as a list of "thread identifier" \<times> state, and an optional
pair result, state when the computation did not fail.\<close>
pair of result and state when the computation did not fail.\<close>
type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set"

text \<open>Returns monad results, ignoring failures and traces.\<close>
@@ -86,10 +86,12 @@ abbreviation(input) bind_rev ::
"g =<< f \<equiv> f >>= g"

text \<open>
The basic accessor functions of the state monad. @{text get} returns
the current state as result, does not fail, and does not change the state.
@{text "put s"} returns nothing (@{typ unit}), changes the current state
to @{text s} and does not fail.\<close>
The basic accessor functions of the state monad. @{text get} returns the
current state as result, does not change the state, and does not add to the
trace. @{text "put s"} returns nothing (@{typ unit}), changes the current
state to @{text s}, and does not add to the trace. @{text "put_trace xs"}
returns nothing (@{typ unit}), does not change the state, and adds @{text xs}
to the trace.\<close>
definition get :: "('s,'s) tmonad" where
"get \<equiv> \<lambda>s. {([], Result (s, s))}"

@@ -107,10 +109,10 @@ subsection "Nondeterminism"

text \<open>
Basic nondeterministic functions. @{text "select A"} chooses an element
of the set @{text A}, does not change the state, and does not fail
(even if the set is empty). @{text "f \<sqinter> g"} executes @{text f} or
executes @{text g}. It retuns the union of results of @{text f} and
@{text g}, and may have failed if either may have failed.\<close>
of the set @{text A} as the result, does not change the state, does not add
to the trace, and does not fail (even if the set is empty). @{text "f \<sqinter> g"}
executes @{text f} or executes @{text g}. It returns the union of results and
traces of @{text f} and @{text g}.\<close>
definition select :: "'a set \<Rightarrow> ('s, 'a) tmonad" where
"select A \<equiv> \<lambda>s. (Pair [] ` Result ` (A \<times> {s}))"

@@ -119,13 +121,13 @@ definition alternative :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightar
"f \<sqinter> g \<equiv> \<lambda>s. (f s \<union> g s)"

text \<open>
The @{text select_f} function was left out here until we figure
FIXME: The @{text select_f} function was left out here until we figure
out what variant we actually need.\<close>

subsection "Failure"

text \<open>
The monad function that always fails. Returns an empty set of results and sets the failure flag.\<close>
The monad function that always fails. Returns an empty trace with a Failed result.\<close>
definition fail :: "('s, 'a) tmonad" where
"fail \<equiv> \<lambda>s. {([], Failed)}"

@@ -208,6 +210,7 @@ lemma elem_bindE:

text \<open>Each monad satisfies at least the following three laws.\<close>

\<comment> \<open>FIXME: is this necessary? If it is, move it\<close>
declare map_option.identity[simp]

text \<open>@{term return} is absorbed at the left of a @{term bind}, applying the return value directly:\<close>
@@ -445,31 +448,36 @@ text \<open>
definition last_st_tr :: "(tmid * 's) list \<Rightarrow> 's \<Rightarrow> 's" where
"last_st_tr tr s0 \<equiv> hd (map snd tr @ [s0])"

text \<open>Nondeterministically add all possible environment events to the trace.\<close>
definition env_steps :: "('s,unit) tmonad" where
"env_steps \<equiv>
do
s \<leftarrow> get;
\<comment> \<open>Add unfiltered environment events to the trace\<close>
xs \<leftarrow> select UNIV;
tr \<leftarrow> return (map (Pair Env) xs);
put_trace tr;
\<comment> \<open>Pick the last event of the trace as the final state\<close>
put (last_st_tr tr s)
od"
do
s \<leftarrow> get;
\<comment> \<open>Add unfiltered environment events to the trace\<close>
xs \<leftarrow> select UNIV;
tr \<leftarrow> return (map (Pair Env) xs);
put_trace tr;
\<comment> \<open>Pick the last event of the trace as the final state\<close>
put (last_st_tr tr s)
od"

text \<open>Add the current state to the trace, tagged as a self action.\<close>
definition commit_step :: "('s,unit) tmonad" where
"commit_step \<equiv>
do
s \<leftarrow> get;
put_trace [(Me,s)]
od"
do
s \<leftarrow> get;
put_trace [(Me,s)]
od"

text \<open>
Record the action taken by the current thread since the last interference point and
then add unfiltered environment events.\<close>
definition interference :: "('s,unit) tmonad" where
"interference \<equiv>
do
commit_step;
env_steps
od"
do
commit_step;
env_steps
od"


section "Library of additional Monadic Functions and Combinators"
@@ -616,7 +624,8 @@ subsection "Loops"
text \<open>
Loops are handled using the following inductive predicate;
non-termination is represented using the failure flag of the
monad.\<close>
monad.
FIXME: update comment about non-termination\<close>

inductive_set whileLoop_results ::
"('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> (('r \<times> 's) \<times> ((tmid \<times> 's) list \<times> ('s, 'r) tmres)) set"
90 changes: 43 additions & 47 deletions lib/Monads/trace/Trace_Monad_Equations.thy
Original file line number Diff line number Diff line change
@@ -46,38 +46,40 @@ lemma fail_bind[simp]:
by (simp add: bind_def fail_def)


subsection \<open>Alternative env_steps with repeat\<close>

lemma mapM_Cons:
"mapM f (x # xs) = do
y \<leftarrow> f x;
ys \<leftarrow> mapM f xs;
return (y # ys)
od"
y \<leftarrow> f x;
ys \<leftarrow> mapM f xs;
return (y # ys)
od"
and mapM_Nil:
"mapM f [] = return []"
by (simp_all add: mapM_def sequence_def)

lemma mapM_x_Cons:
"mapM_x f (x # xs) = do
y \<leftarrow> f x;
mapM_x f xs
od"
y \<leftarrow> f x;
mapM_x f xs
od"
and mapM_x_Nil:
"mapM_x f [] = return ()"
by (simp_all add: mapM_x_def sequence_x_def)

lemma mapM_append:
"mapM f (xs @ ys) = (do
fxs \<leftarrow> mapM f xs;
fys \<leftarrow> mapM f ys;
return (fxs @ fys)
od)"
fxs \<leftarrow> mapM f xs;
fys \<leftarrow> mapM f ys;
return (fxs @ fys)
od)"
by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc)

lemma mapM_x_append:
"mapM_x f (xs @ ys) = (do
x \<leftarrow> mapM_x f xs;
mapM_x f ys
od)"
x \<leftarrow> mapM_x f xs;
mapM_x f ys
od)"
by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc)

lemma mapM_map:
@@ -88,37 +90,31 @@ lemma mapM_x_map:
"mapM_x f (map g xs) = mapM_x (f o g) xs"
by (induct xs; simp add: mapM_x_Nil mapM_x_Cons)

primrec
repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
where
primrec repeat_n :: "nat \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
"repeat_n 0 f = return ()"
| "repeat_n (Suc n) f = do f; repeat_n n f od"

lemma repeat_n_mapM_x:
"repeat_n n f = mapM_x (\<lambda>_. f) (replicate n ())"
by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil)

definition
repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad"
where
definition repeat :: "('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
"repeat f = do n \<leftarrow> select UNIV; repeat_n n f od"

definition
env_step :: "('s,unit) tmonad"
where
definition env_step :: "('s,unit) tmonad" where
"env_step =
(do
s' \<leftarrow> select UNIV;
put_trace_elem (Env, s');
put s'
od)"
do
s' \<leftarrow> select UNIV;
put_trace_elem (Env, s');
put s'
od"

abbreviation
"env_n_steps n \<equiv> repeat_n n env_step"

lemma elem_select_bind:
"(tr, res) \<in> (do x \<leftarrow> select S; f x od) s
= (\<exists>x \<in> S. (tr, res) \<in> f x s)"
= (\<exists>x \<in> S. (tr, res) \<in> f x s)"
by (simp add: bind_def select_def)

lemma select_bind_UN:
@@ -127,17 +123,17 @@ lemma select_bind_UN:

lemma select_early:
"S \<noteq> {}
\<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
= do y \<leftarrow> select S; x \<leftarrow> f; g x y od"
\<Longrightarrow> do x \<leftarrow> f; y \<leftarrow> select S; g x y od
= do y \<leftarrow> select S; x \<leftarrow> f; g x y od"
apply (simp add: bind_def select_def Sigma_def)
apply (rule ext)
apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm)
done

lemma repeat_n_choice:
"S \<noteq> {}
\<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
= (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)"
\<Longrightarrow> repeat_n n (do x \<leftarrow> select S; f x od)
= (do xs \<leftarrow> select {xs. set xs \<subseteq> S \<and> length xs = n}; mapM_x f xs od)"
apply (induct n; simp?)
apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong)
apply (simp add: select_early bind_assoc)
@@ -152,8 +148,8 @@ lemma repeat_n_choice:

lemma repeat_choice:
"S \<noteq> {}
\<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
= (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)"
\<Longrightarrow> repeat (do x \<leftarrow> select S; f x od)
= (do xs \<leftarrow> select {xs. set xs \<subseteq> S}; mapM_x f xs od)"
apply (simp add: repeat_def repeat_n_choice)
apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind)
done
@@ -164,27 +160,27 @@ lemma put_trace_append:

lemma put_trace_elem_put_comm:
"do y \<leftarrow> put_trace_elem x; put s od
= do y \<leftarrow> put s; put_trace_elem x od"
= do y \<leftarrow> put s; put_trace_elem x od"
by (simp add: put_def put_trace_elem_def bind_def insert_commute)

lemma put_trace_put_comm:
"do y \<leftarrow> put_trace xs; put s od
= do y \<leftarrow> put s; put_trace xs od"
= do y \<leftarrow> put s; put_trace xs od"
apply (rule sym; induct xs; simp)
apply (simp add: bind_assoc put_trace_elem_put_comm)
apply (simp add: bind_assoc[symmetric])
done

lemma mapM_x_comm:
"(\<forall>x \<in> set xs. do y \<leftarrow> g; f x od = do y \<leftarrow> f x; g od)
\<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od"
\<Longrightarrow> do y \<leftarrow> g; mapM_x f xs od = do y \<leftarrow> mapM_x f xs; g od"
apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons)
apply (simp add: bind_assoc[symmetric], simp add: bind_assoc)
done

lemma mapM_x_split:
"(\<forall>x \<in> set xs. \<forall>y \<in> set xs. do z \<leftarrow> g y; f x od = do (z :: unit) \<leftarrow> f x; g y od)
\<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od"
\<Longrightarrow> mapM_x (\<lambda>x. do z \<leftarrow> f x; g x od) xs = do y \<leftarrow> mapM_x f xs; mapM_x g xs od"
apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc)
apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x])
apply simp
@@ -237,15 +233,15 @@ lemma repeat_eq_twice[simp]:
apply (rule ext, fastforce intro: exI[where x=0])
done

lemmas repeat_eq_twice_then[simp]
= repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc]
lemmas repeat_eq_twice_then[simp] =
repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc]

lemmas env_steps_eq_twice[simp]
= repeat_eq_twice[where f=env_step, folded env_steps_repeat]
lemmas env_steps_eq_twice_then[simp]
= env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc]
lemmas env_steps_eq_twice[simp] =
repeat_eq_twice[where f=env_step, folded env_steps_repeat]
lemmas env_steps_eq_twice_then[simp] =
env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc]

lemmas mapM_collapse_append = mapM_append[symmetric, THEN bind_then_eq,
simplified bind_assoc, simplified]
lemmas mapM_collapse_append =
mapM_append[symmetric, THEN bind_then_eq, simplified bind_assoc, simplified]

end
4 changes: 2 additions & 2 deletions lib/Monads/trace/Trace_No_Fail.thy
Original file line number Diff line number Diff line change
@@ -17,9 +17,9 @@ begin
subsection "Non-Failure"

text \<open>
With the failure flag, we can formulate non-failure separately from validity.
With the failure result, we can formulate non-failure separately from validity.
A monad @{text m} does not fail under precondition @{text P}, if for no start
state that satisfies the precondition it sets the failure flag.
state that satisfies the precondition it returns a @{term Failed} result.
\<close>
definition no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> bool" where
"no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> Failed \<notin> snd ` (m s)"
23 changes: 15 additions & 8 deletions lib/Monads/trace/Trace_No_Trace.thy
Original file line number Diff line number Diff line change
@@ -11,32 +11,39 @@ theory Trace_No_Trace
WPSimp
begin

definition
no_trace :: "('s,'a) tmonad \<Rightarrow> bool"
where
subsection "No Trace"

text \<open>
A monad of type @{text tmonad} does not have a trace iff for all starting
states, all of the potential outcomes have the empty list as a trace and do
not return an @{term Incomplete} result.\<close>
definition no_trace :: "('s,'a) tmonad \<Rightarrow> bool" where
"no_trace f = (\<forall>tr res s. (tr, res) \<in> f s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete)"

lemmas no_traceD = no_trace_def[THEN iffD1, rule_format]

lemma no_trace_emp:
"no_trace f \<Longrightarrow> (tr, r) \<in> f s \<Longrightarrow> tr = []"
"\<lbrakk>no_trace f; (tr, r) \<in> f s\<rbrakk> \<Longrightarrow> tr = []"
by (simp add: no_traceD)

lemma no_trace_Incomplete_mem:
"no_trace f \<Longrightarrow> (tr, Incomplete) \<notin> f s"
by (auto dest: no_traceD)

lemma no_trace_Incomplete_eq:
"no_trace f \<Longrightarrow> (tr, res) \<in> f s \<Longrightarrow> res \<noteq> Incomplete"
"\<lbrakk>no_trace f; (tr, res) \<in> f s\<rbrakk> \<Longrightarrow> res \<noteq> Incomplete"
by (auto dest: no_traceD)

lemma no_trace_is_triple:

subsection \<open>Set up for @{method wp}\<close>

lemma no_trace_is_triple[wp_trip]:
"no_trace f = triple_judgement \<top> f (\<lambda>() f. id no_trace f)"
by (simp add: triple_judgement_def split: unit.split)

lemmas [wp_trip] = no_trace_is_triple

(* Since valid_validI_wp in wp_comb doesn't work, we add the rules directly in the wp set *)
subsection \<open>Rules\<close>

lemma no_trace_prim:
"no_trace get"
"no_trace (put s)"
353 changes: 195 additions & 158 deletions lib/Monads/trace/Trace_RG.thy

Large diffs are not rendered by default.

13 changes: 6 additions & 7 deletions lib/Monads/trace/Trace_VCG.thy
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ text \<open>
This section defines a Hoare logic for partial correctness for
the interference trace monad as well as the exception monad.
The logic talks only about the behaviour part of the monad and ignores
the failure flag.
failures and the trace.
The logic is defined semantically. Rules work directly on the
validity predicate.
@@ -29,12 +29,11 @@ text \<open>
bool (a state predicate), the postcondition is a function from return value
to state to bool. A triple is valid if for all states that satisfy the
precondition, all result values and result states that are returned by
the monad satisfy the postcondition. Note that if the computation returns
the empty set, the triple is trivially valid. This means @{term "assert P"}
does not require us to prove that @{term P} holds, but rather allows us
to assume @{term P}! Proving non-failure is done via a separate predicate and
calculus (see Trace_No_Fail).\<close>

the monad satisfy the postcondition. Note that if the result of the
computation is the empty set then the triple is trivially valid. This means
@{term "assert P"} does not require us to prove that @{term P} holds, but
rather allows us to assume @{term P}! Proving non-failure is done via a
separate predicate and calculus (see Trace_No_Fail).\<close>
definition valid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
"\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> mres (f s). Q r s')"