From 5c8eb5381b39a84af40fc3eb7f19c185c89ea91e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 28 Jul 2025 11:53:58 +1000 Subject: [PATCH 1/7] c-parser: make Gamma configurable Make the name of the procedure environment Gamma configurable. This enables operations on Gamma later. Signed-off-by: Gerwin Klein --- tools/c-parser/HPInter.ML | 10 ++++--- tools/c-parser/isar_install.ML | 29 ++++++++++++------- tools/c-parser/modifies_proofs.ML | 21 +++++++------- tools/c-parser/name_generation.ML | 4 +-- tools/c-parser/stmt_translation.ML | 12 ++++---- .../testfiles/modifies_assumptions.thy | 4 +-- 6 files changed, 47 insertions(+), 33 deletions(-) diff --git a/tools/c-parser/HPInter.ML b/tools/c-parser/HPInter.ML index a7a2034561..a331a09428 100644 --- a/tools/c-parser/HPInter.ML +++ b/tools/c-parser/HPInter.ML @@ -25,10 +25,11 @@ sig type fninfo = HPfninfo.t val globalsN : string val asm_to_string : (term -> string) -> ('typ,term,'fact) Element.ctxt -> string - val mk_fninfo : theory -> csenv -> (string -> bool) -> + val mk_fninfo : theory -> csenv -> string -> (string -> bool) -> Absyn.ext_decl list -> fninfo list val make_function_definitions : string -> (* name of locale where definitions will live *) + string -> (* name of procedure environment (\) *) csenv -> (* result of ProgramAnalysis over declarations *) typ list -> (* type arguments to state type operator *) thm list -> (* theorems defining names of functions *) @@ -52,7 +53,7 @@ type csenv = ProgramAnalysis.csenv (* make function information - perform a preliminary analysis on the abstract syntax to extract function names, parameters and specifications *) -fun mk_fninfo thy csenv includeP decllist : fninfo list = let +fun mk_fninfo thy csenv gamma includeP decllist : fninfo list = let open Absyn NameGeneration (* don't fold top-level declarations into the table again: the program analysis that built the csenv in the first place will have already @@ -84,7 +85,7 @@ fun mk_fninfo thy csenv includeP decllist : fninfo list = let [("", Element.Assumes (map nprop2Assume nameproplist))] end | fn_modifies slist => let - val mgoal = Modifies_Proofs.gen_modify_goalstring csenv fname slist + val mgoal = Modifies_Proofs.gen_modify_goalstring csenv gamma fname slist in [("", Element.Assumes [((Binding.name (fname ^ "_modifies"), []), [(mgoal, [])])])] @@ -378,6 +379,7 @@ fun asm_to_string tmw e = (* The following is modelled on the code in HoarePackage.procedures_definition *) fun make_function_definitions localename + gamma_name (cse : ProgramAnalysis.csenv) (styargs : typ list) (nmdefs : thm list) @@ -437,7 +439,7 @@ let end (* name for thm, (proc constant, body constant) *) val (_, lthy) = StaticFun.define_tree_and_thms_with_defs - @{binding \} (map (suffix HoarePackage.implementationN o #fname) fninfo) + (Binding.make (gamma_name, \<^here>)) (map (suffix HoarePackage.implementationN o #fname) fninfo) nmdefs (map get_body fninfo) @{term "id :: int => int"} lthy in Local_Theory.exit_global lthy diff --git a/tools/c-parser/isar_install.ML b/tools/c-parser/isar_install.ML index 0cdd01ba34..049a2f4ab7 100644 --- a/tools/c-parser/isar_install.ML +++ b/tools/c-parser/isar_install.ML @@ -69,7 +69,8 @@ structure C_Includes = Theory_Data val merge = Library.merge (op =) end); -datatype additional_options = MachineState of string | GhostState of string | CRoots of string list +datatype additional_options = + MachineState of string | GhostState of string | CRoots of string list | GammaName of string type install_data = {c_filename : string, locale_names : string list, options: (bool * bool * bool), @@ -160,18 +161,18 @@ in ast0 |> SyntaxTransforms.remove_anonstructs |> SyntaxTransforms.remove_typedefs end -fun define_naming_scheme [] _ = I - | define_naming_scheme fninfo nmdefs = let +fun define_naming_scheme gamma [] _ = I + | define_naming_scheme gamma fninfo nmdefs = let fun name_term fni = SOME (HOLogic.mk_string (#fname fni)) fun name_name fni = #fname fni ^ "_name" in StaticFun.define_tree_and_thms_with_defs - (Binding.name NameGeneration.naming_scheme_name) + (Binding.name (NameGeneration.naming_scheme_name gamma)) (map name_name fninfo) nmdefs (map name_term fninfo) @{term "id :: int => int"} #> snd end -fun define_function_names fninfo thy = let +fun define_function_names gamma fninfo thy = let open Feedback fun decl1 (fni, (n, defs, lthy)) = let open TermsTypes @@ -192,7 +193,7 @@ fun define_function_names fninfo thy = let end val (_, defs, lthy) = List.foldl decl1 (1, [], Named_Target.theory_init thy) fninfo - val lthy' = define_naming_scheme fninfo (List.rev defs) lthy + val lthy' = define_naming_scheme gamma fninfo (List.rev defs) lthy in (defs, Local_Theory.exit_global lthy') end @@ -314,6 +315,10 @@ fun install_C_file0 (((((memsafe),ctyps),cdefs),s),statetylist_opt) thy = let case get_first (fn (GhostState s) => SOME s | _ => NONE) statetylist of NONE => TermsTypes.unit | SOME s => Syntax.read_typ_global thy s + val gamma = + case get_first (fn (GammaName s) => SOME s | _ => NONE) statetylist of + NONE => "\" + | SOME s => s val thy = Config.put_global CalculateState.current_C_filename s thy val thy = CalculateState.store_ghostty (s, gstate_ty) thy val anon_vars = Config.get_global thy use_anon_vars @@ -427,17 +432,19 @@ in case toTranslate of NONE => (fn _ => true) | SOME set => (fn s => Binaryset.member(set,s)) - val fninfo : HPInter.fninfo list = HPInter.mk_fninfo thy cse toTranslateP ast - val (nmdefs, thy) = define_function_names fninfo thy + val fninfo : HPInter.fninfo list = HPInter.mk_fninfo thy cse gamma toTranslateP ast + val (nmdefs, thy) = define_function_names gamma fninfo thy val compile_bodies = stmt_translation.define_functions (globty, styargs) mungedb cse + gamma fninfo rcdinfo ms val (loc2, thy) = HPInter.make_function_definitions localename + gamma cse styargs (List.rev nmdefs) @@ -448,7 +455,7 @@ in thy val thy = if not (Symtab.is_empty (get_defined_functions cse)) then - Modifies_Proofs.prove_all_modifies_goals thy cse toTranslateP styargs loc2 + Modifies_Proofs.prove_all_modifies_goals thy cse gamma toTranslateP styargs loc2 else thy (* like this is ever going to happen *) in C_Installs.map (fn ss => @@ -527,6 +534,7 @@ val defsN = "c_defs" val mtypN = "machinety" val ghosttypN = "ghostty" val rootsN = "roots" +val gammaN = "gamma" local structure P = Parse @@ -542,7 +550,8 @@ val file_inclusion = let val typoptions = P.reserved mtypN |-- (P.$$$ "=" |-- P.embedded >> MachineState) || P.reserved ghosttypN |-- (P.$$$ "=" |-- P.embedded >> GhostState) || - P.reserved rootsN |-- (P.$$$ "=" |-- (P.$$$ "[" |-- P.enum1 "," P.embedded --| P.$$$ "]") >> CRoots) + P.reserved rootsN |-- (P.$$$ "=" |-- (P.$$$ "[" |-- P.enum1 "," P.embedded --| P.$$$ "]") >> CRoots) || + P.reserved gammaN |-- (P.$$$ "=" |-- P.embedded >> GammaName) in ((Scan.option (P.$$$ memsafeN)) -- (Scan.option (P.$$$ typesN)) -- diff --git a/tools/c-parser/modifies_proofs.ML b/tools/c-parser/modifies_proofs.ML index c99cd68798..7793ab344c 100644 --- a/tools/c-parser/modifies_proofs.ML +++ b/tools/c-parser/modifies_proofs.ML @@ -33,17 +33,18 @@ sig goal as something that can be modified. *) - val gen_modify_goalstring : csenv -> string -> string list -> string + val gen_modify_goalstring : csenv -> string -> string -> string list -> string val modifies_vcg_tactic : local_theory -> int -> tactic val modifies_tactic : thm -> local_theory -> tactic - val prove_all_modifies_goals_local : csenv -> (string -> bool) -> typ list -> + val prove_all_modifies_goals_local : csenv -> string -> (string -> bool) -> typ list -> local_theory -> local_theory - val prove_all_modifies_goals : theory -> csenv -> (string -> bool) -> + val prove_all_modifies_goals : theory -> csenv -> string -> (string -> bool) -> typ list -> string -> theory - (* string is the name of the locale where the theorems about Gamma live *) + (* first string is the name of the procedure environment Gamma *) + (* second string is the name of the locale where the theorems about Gamma live *) val sorry_modifies_proofs : bool Config.T val calculate_modifies_proofs : bool Config.T @@ -82,14 +83,14 @@ fun cond_sorry_modifies_proofs VAR ctxt = ctxt' end -fun gen_modify_goalstring csenv fname modstrings = let +fun gen_modify_goalstring csenv gamma fname modstrings = let fun foldthis (vname, vset) = case MSymTab.lookup (ProgramAnalysis.get_addressed csenv) (MString.mk vname) of NONE => Binaryset.add(vset, vname) | SOME _ => Binaryset.add(vset, NameGeneration.global_heap) val vset = List.foldl foldthis (Binaryset.empty String.compare) modstrings in - "\\. \ \\<^bsub>/UNIV\<^esub> {\} Call "^ + "\\. "^ gamma ^" \\<^bsub>/UNIV\<^esub> {\} Call "^ fname ^ "_'proc " ^ "{t. t may_only_modify_globals \ in [" ^ commas (Binaryset.listItems vset) ^ "]}" @@ -292,7 +293,7 @@ in | NONE => prove_mod_inv_prop () end -fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let +fun prove_all_modifies_goals_local csenv gamma includeP tyargs lthy = let open ProgramAnalysis val _ = Feedback.informStr (0, "Proving automatically calculated modifies proofs") val globs_all_addressed = Config.get lthy CalculateState.globals_all_addressed @@ -300,7 +301,7 @@ fun prove_all_modifies_goals_local csenv includeP tyargs lthy = let (* first enter the locale where \ exists, and where all the mappings from function name to function body exist *) val lconsts = Proof_Context.consts_of lthy - val gamma_nm = Consts.intern lconsts "\" + val gamma_nm = Consts.intern lconsts gamma val gamma_t = Syntax.check_term lthy (Const(gamma_nm, dummyT)) val {callgraph,callers} = compute_callgraphs csenv @@ -426,14 +427,14 @@ in lthy end -fun prove_all_modifies_goals thy csenv includeP tyargs globloc = +fun prove_all_modifies_goals thy csenv gamma includeP tyargs globloc = if Config.get_global thy calculate_modifies_proofs then let val lthy = Named_Target.init [] globloc thy in lthy |> Local_Theory.begin_nested |> snd - |> prove_all_modifies_goals_local csenv includeP tyargs + |> prove_all_modifies_goals_local csenv gamma includeP tyargs |> Local_Theory.end_nested |> Local_Theory.exit_global end diff --git a/tools/c-parser/name_generation.ML b/tools/c-parser/name_generation.ML index a877b5a0ff..65f8c36054 100644 --- a/tools/c-parser/name_generation.ML +++ b/tools/c-parser/name_generation.ML @@ -20,7 +20,7 @@ sig val adglob_rcd_tyname : string val adglob_struct_var : string - val naming_scheme_name : string + val naming_scheme_name : string -> string val enum_const_name : string -> string val enum_const_summary_lemma_sfx : string @@ -234,7 +234,7 @@ val adglob_struct_var = "adglobs" val phantom_state_name = "phantom_machine_state" val ghost_state_name = "ghost'state" -val naming_scheme_name = "\\" ^ "_naming" +fun naming_scheme_name gamma = gamma ^ "_naming" val owned_by_fn_name = "owner'ship" val internalAnonStructPfx = "ISA_anon_struct|" diff --git a/tools/c-parser/stmt_translation.ML b/tools/c-parser/stmt_translation.ML index df4c7edc6d..c68b665fb5 100644 --- a/tools/c-parser/stmt_translation.ML +++ b/tools/c-parser/stmt_translation.ML @@ -171,6 +171,7 @@ end fun stmt_term (ctxt : Proof.context) (cse : ProgramAnalysis.csenv) + (gamma : string) (fname : string) (termbuilders : varinfo termbuilder) (varinfo : MString.t -> varinfo option) @@ -181,7 +182,7 @@ fun stmt_term (ctxt : Proof.context) (ms : bool) (stmt : Absyn.statement) : stmt_result = let val stmt_term = - stmt_term ctxt cse fname termbuilders varinfo fninfo + stmt_term ctxt cse gamma fname termbuilders varinfo fninfo statetype globty styargs ms val sg = Proof_Context.theory_of ctxt val progname = Config.get_global sg CalculateState.current_C_filename @@ -460,7 +461,7 @@ in | (FnPtrCall(rty, _ (* argtys *)), _) => let val call_ei = expr_term call_e open NameGeneration - val naming = Const (Sign.intern_const sg naming_scheme_name, + val naming = Const (Sign.intern_const sg (naming_scheme_name gamma), int --> mk_option_ty string_ty) val (pbody, pguard) = MemoryModelExtras.mk_lookup_proc_pair symbol_table naming @@ -771,7 +772,7 @@ in CNameTab.fold foldthis state Symtab.empty end -fun fndefn_term (state : CalculateState.mungedb) cse fninfo rcdinfo ms globty styargs ctxt decl = let +fun fndefn_term (state : CalculateState.mungedb) cse gamma fninfo rcdinfo ms globty styargs ctxt decl = let val thy = Proof_Context.theory_of ctxt open CalculateState val statetype = hd styargs @@ -794,7 +795,7 @@ fun fndefn_term (state : CalculateState.mungedb) cse fninfo rcdinfo ms globty st in (cse2ecenv cse, get_senv cse) end - val stmt_trans = stmt_term ctxt cse fname termbuilders + val stmt_trans = stmt_term ctxt cse gamma fname termbuilders varinfo fninfo statetype globty styargs ms val (body_f, body_parses) = trans_list stmt_trans styargs body @@ -859,6 +860,7 @@ end fun define_functions (globty, styargs) (vdecls : CalculateState.mungedb) cse + gamma fninfo rcdinfo ms @@ -868,7 +870,7 @@ let open TermsTypes CalculateState val fns = extract_defined_functions ast val function_info = - map (fndefn_term vdecls cse fninfo rcdinfo ms globty styargs ctxt) fns + map (fndefn_term vdecls cse gamma fninfo rcdinfo ms globty styargs ctxt) fns in function_info end diff --git a/tools/c-parser/testfiles/modifies_assumptions.thy b/tools/c-parser/testfiles/modifies_assumptions.thy index 8de1a9c4c4..dd4581fe07 100644 --- a/tools/c-parser/testfiles/modifies_assumptions.thy +++ b/tools/c-parser/testfiles/modifies_assumptions.thy @@ -9,7 +9,7 @@ imports "CParser.CTranslation" begin external_file "modifies_assumptions.c" -install_C_file "modifies_assumptions.c" +install_C_file "modifies_assumptions.c" [gamma = \0] context modifies_assumptions begin @@ -25,7 +25,7 @@ thm h_modifies thm j_modifies thm k_modifies -lemma "\ f_'proc = Some f_body" +lemma "\0 f_'proc = Some f_body" apply (simp add: f_impl) done From 0c46d9b00612067ada46b66a08c67f28097a242b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 7 Aug 2025 14:18:52 +0200 Subject: [PATCH 2/7] autocorres: make Gamma configurable Add option for providing the name of the procedure environment \Gamma. Useful when the C parser is instructed to create a custom name for the procedure environment. Signed-off-by: Gerwin Klein --- tools/autocorres/README.md | 5 +++++ tools/autocorres/autocorres.ML | 16 +++++++++++++--- tools/autocorres/function_info.ML | 6 +++--- tools/autocorres/program_info.ML | 4 ++-- tools/autocorres/test-seL4/TestSEL4.thy | 2 +- 5 files changed, 24 insertions(+), 9 deletions(-) diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md index 42d09b19e9..63ede55cde 100644 --- a/tools/autocorres/README.md +++ b/tools/autocorres/README.md @@ -119,6 +119,10 @@ generated locale (named `file`). The options are: + * `gamma = CONSTANT_NAME`: use the given constant name as + the name of the procedure environment to expect from the + C parser. Default: `"\"` + * `no_heap_abs = FUNC_NAMES`: Disable _heap abstraction_ on the given list of functions. @@ -203,6 +207,7 @@ An example of invoking AutoCorres with _all_ of the options is as follows: autocorres [ + gamma = "\", no_heap_abs = a b, force_heap_abs = c d, gen_word_heaps, diff --git a/tools/autocorres/autocorres.ML b/tools/autocorres/autocorres.ML index 6b768d7e21..68eb9cad6c 100644 --- a/tools/autocorres/autocorres.ML +++ b/tools/autocorres/autocorres.ML @@ -24,6 +24,9 @@ struct * work around this, but this is a light-weight solution. *) type autocorres_options = { + (* Name of the procedure environment. *) + gamma_name : string option ref, + (* Do not lift heaps for these functions. *) no_heap_abs : string list option ref, @@ -120,6 +123,10 @@ val named_opt = named_option (Scan.repeat Parse.embedded) val nat_opt = named_option Parse.nat (* Valid options. *) +val gamma_name_parser = + named_option Parse.embedded "gamma" "procedure environment" >> + (fn gamma_name => none_to_some (#gamma_name) gamma_name "autocorres: gamma specified multiple times") + val no_heap_abs_parser = named_opt "no_heap_abs" "function names" >> (fn funcs => none_to_some (#no_heap_abs) funcs "autocorres: no_heap_abs option specified multiple times") @@ -239,6 +246,7 @@ val function_name_suffix_parser = * time; hence the dummy parameter. *) fun default_opts _ = { + gamma_name = ref NONE, no_heap_abs = ref NONE, force_heap_abs = ref NONE, skip_heap_abs = ref NONE, @@ -268,7 +276,8 @@ fun default_opts _ = { val autocorres_parser : (autocorres_options * string) parser = let val option_parser = - (no_heap_abs_parser || + (gamma_name_parser || + no_heap_abs_parser || force_heap_abs_parser || skip_heap_abs_parser || ts_rules_parser || @@ -323,8 +332,9 @@ let | NONE => error ("autocorres: no such locale: " ^ locale_name) (* Fetch program information from the C-parser output. *) - val prog_info = ProgramInfo.get_prog_info lthy filename - val all_simpl_info = FunctionInfo.init_function_info lthy filename + val gamma_name = case !(#gamma_name opt) of SOME g => g | NONE => "\" + val prog_info = ProgramInfo.get_prog_info lthy gamma_name filename + val all_simpl_info = FunctionInfo.init_function_info lthy gamma_name filename val all_simpl_functions = Symset.make (Symtab.keys all_simpl_info) (* Process autocorres options. *) diff --git a/tools/autocorres/function_info.ML b/tools/autocorres/function_info.ML index f582223741..7360c83583 100644 --- a/tools/autocorres/function_info.ML +++ b/tools/autocorres/function_info.ML @@ -92,7 +92,7 @@ sig val all_callees : function_info -> symset; (* Generate initial function_info from the C Parser's output. *) - val init_function_info : Proof.context -> string -> function_info Symtab.table; + val init_function_info : Proof.context -> string -> string -> function_info Symtab.table; type call_graph_info = { (* Topologically sorted function calls, in dependency order. @@ -350,9 +350,9 @@ fun recalc_callees base_infos fn_infos = let |> Symtab.make) end; -fun init_function_info ctxt filename = let +fun init_function_info ctxt gamma_name filename = let val thy = Proof_Context.theory_of ctxt; - val prog_info = ProgramInfo.get_prog_info ctxt filename; + val prog_info = ProgramInfo.get_prog_info ctxt gamma_name filename; val csenv = #csenv prog_info; (* Get information about a single function. *) diff --git a/tools/autocorres/program_info.ML b/tools/autocorres/program_info.ML index ffd5107d4e..412555f2cb 100644 --- a/tools/autocorres/program_info.ML +++ b/tools/autocorres/program_info.ML @@ -133,7 +133,7 @@ fun demangle_name (prog_info: prog_info) m = (* * Extract details from the c-parser about the given program. *) -fun get_prog_info ctxt filename : prog_info = +fun get_prog_info ctxt gamma_name filename : prog_info = let val thy = Proof_Context.theory_of ctxt val csenv = CalculateState.get_csenv thy filename |> the; @@ -146,7 +146,7 @@ fun get_prog_info ctxt filename : prog_info = (* Get the gamma variable, mapping function numbers to function bodies in * SIMPL. *) val gamma = - (Const (Consts.intern (Proof_Context.consts_of ctxt) "\", dummyT) + (Const (Consts.intern (Proof_Context.consts_of ctxt) gamma_name, dummyT) |> Syntax.check_term ctxt) handle TERM _ => error "autocorres: could not find any functions -- \ is not defined." diff --git a/tools/autocorres/test-seL4/TestSEL4.thy b/tools/autocorres/test-seL4/TestSEL4.thy index d7ff3c43b0..28b986d53f 100644 --- a/tools/autocorres/test-seL4/TestSEL4.thy +++ b/tools/autocorres/test-seL4/TestSEL4.thy @@ -13,6 +13,6 @@ begin (* * Test to see if we can parse all of seL4. *) -autocorres [skip_heap_abs, ts_rules = nondet] "../c/build/$L4V_ARCH/kernel_all.c_pp" +autocorres [skip_heap_abs, ts_rules = nondet, gamma = "\0"] "../c/build/$L4V_ARCH/kernel_all.c_pp" end From 4bc767526df2598a5f4dc59b7db9dd4444f85927 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 30 Jul 2025 08:25:35 +1000 Subject: [PATCH 3/7] cspec: parameterise Gamma for multikernel - rename the procedure environment of the original kernel source from Gamma to Gamma0 so that we can introduce a new layer Gamma for procedures with bodies that depend on which core they run on. - override Gamma0 in kernel_all_substitute0 with a version where physBase depends on cpuNum - do the same for kernel_all_global_addresses - automatically prove *_impl theorems for the new Gamma in kernel_all_substitute - automatically prove *_modifies theorems for the new Gamma in kernel_all_substitute - remove *_modifies theorem generation from kernel_all_substitute0, since we don't need them there Signed-off-by: Gerwin Klein --- spec/ROOT | 1 + spec/cspec/AARCH64/Kernel_C.thy | 2 +- spec/cspec/ARM/Kernel_C.thy | 2 +- spec/cspec/ARM_HYP/Kernel_C.thy | 2 +- spec/cspec/KernelState_C.thy | 2 +- spec/cspec/Multikernel_C.thy | 81 +++++++++++++++++++ spec/cspec/RISCV64/Kernel_C.thy | 2 +- spec/cspec/Substitute.thy | 15 ++-- spec/cspec/X64/Kernel_C.thy | 2 +- .../multikernel/AARCH64/ArchMultikernel_C.thy | 64 +++++++++++++++ .../multikernel/ARM/ArchMultikernel_C.thy | 64 +++++++++++++++ .../multikernel/ARM_HYP/ArchMultikernel_C.thy | 64 +++++++++++++++ .../multikernel/RISCV64/ArchMultikernel_C.thy | 65 +++++++++++++++ .../multikernel/X64/ArchMultikernel_C.thy | 54 +++++++++++++ 14 files changed, 407 insertions(+), 13 deletions(-) create mode 100644 spec/cspec/Multikernel_C.thy create mode 100644 spec/cspec/multikernel/AARCH64/ArchMultikernel_C.thy create mode 100644 spec/cspec/multikernel/ARM/ArchMultikernel_C.thy create mode 100644 spec/cspec/multikernel/ARM_HYP/ArchMultikernel_C.thy create mode 100644 spec/cspec/multikernel/RISCV64/ArchMultikernel_C.thy create mode 100644 spec/cspec/multikernel/X64/ArchMultikernel_C.thy diff --git a/spec/ROOT b/spec/ROOT index f05baca972..346a520642 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -81,6 +81,7 @@ session ExecSpec in "design" = Word_Lib + session CSpec in "cspec" = CKernel + directories + "multikernel/$L4V_ARCH" "c/build/$L4V_ARCH/generated/arch/object" "c/build/$L4V_ARCH/generated/sel4" theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty] diff --git a/spec/cspec/AARCH64/Kernel_C.thy b/spec/cspec/AARCH64/Kernel_C.thy index a280b5fdaf..bc7306074b 100644 --- a/spec/cspec/AARCH64/Kernel_C.thy +++ b/spec/cspec/AARCH64/Kernel_C.thy @@ -109,7 +109,7 @@ lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix for these:\ diff --git a/spec/cspec/ARM/Kernel_C.thy b/spec/cspec/ARM/Kernel_C.thy index 60c5c0bb40..2282df5464 100644 --- a/spec/cspec/ARM/Kernel_C.thy +++ b/spec/cspec/ARM/Kernel_C.thy @@ -91,7 +91,7 @@ lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix for these:\ diff --git a/spec/cspec/ARM_HYP/Kernel_C.thy b/spec/cspec/ARM_HYP/Kernel_C.thy index 60c5c0bb40..2282df5464 100644 --- a/spec/cspec/ARM_HYP/Kernel_C.thy +++ b/spec/cspec/ARM_HYP/Kernel_C.thy @@ -91,7 +91,7 @@ lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix for these:\ diff --git a/spec/cspec/KernelState_C.thy b/spec/cspec/KernelState_C.thy index 00b082fcee..9d403bf823 100644 --- a/spec/cspec/KernelState_C.thy +++ b/spec/cspec/KernelState_C.thy @@ -10,7 +10,7 @@ theory KernelState_C imports "Word_Lib.WordSetup" "CLib.BitFieldProofsLib" - "Substitute" + "Multikernel_C" begin type_synonym c_ptr_name = int diff --git a/spec/cspec/Multikernel_C.thy b/spec/cspec/Multikernel_C.thy new file mode 100644 index 0000000000..3759b48ae0 --- /dev/null +++ b/spec/cspec/Multikernel_C.thy @@ -0,0 +1,81 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory Multikernel_C +imports ArchMultikernel_C +begin + +ML \ +structure GammaLift = struct + (* Prove impl theorem for x_proc of the form "\ x_'proc = x_body" + from existing x_impl on \0 and x_'proc \ special_'proc. + Return (thm name, thm). *) + fun prove_impl ctxt special_proc_def gamma_def gamma proc = + let + val _ = tracing ("Proving impl theorem for " ^ proc) + val body_name = unsuffix Hoare.proc_deco proc |> suffix "_body" + val impl_name = unsuffix Hoare.proc_deco proc |> suffix HoarePackage.implementationN + val impl_goal = + Syntax.read_term ctxt (gamma ^ " " ^ proc ^ " = Some " ^ body_name) + |> HOLogic.mk_Trueprop + val proc_def = Proof_Context.get_thm ctxt (proc ^ "_def") + val impl_thm = Proof_Context.get_thm ctxt impl_name + fun impl_tac _ = EVERY [ + simp_tac (ctxt addsimps [gamma_def]) 1, + resolve_tac ctxt @{thms conjI} 1, + simp_tac (ctxt addsimps [special_proc_def, proc_def]) 1, + resolve_tac ctxt @{thms impI} 1, + resolve_tac ctxt [impl_thm] 1] + in + (impl_name, Goal.prove_future ctxt [] [] impl_goal impl_tac) + end + + (* Prove all *_impl theorems, except for the procedure "special", + which we assume has been overridden. *) + fun prove_impls special gamma0 gamma ctxt = + let + val special_proc = suffix Hoare.proc_deco special + val special_proc_def = Proof_Context.get_thm ctxt (special_proc ^ "_def") + + val gamma0_def = Proof_Context.get_thm ctxt (gamma0 ^ "_def") + val gamma_def = Proof_Context.get_thm ctxt (gamma ^ "_def") + + (* \0 is a tree definition that mentions all *_proc constants. + Start with all constants in \0_def and filter out the one we want *) + val proc_names = + Term.add_const_names (Thm.concl_of gamma0_def) [] + |> filter (String.isSuffix Hoare.proc_deco) + |> filter (fn name => Long_Name.base_name name <> special_proc) + |> map Long_Name.base_name + + val impls = map (prove_impl ctxt special_proc_def gamma_def gamma) proc_names + in + Local_Theory.notes (map (fn (n, thm) => ((Binding.name n, []), [([thm], [])])) impls) ctxt |> snd + end +end +\ + +context kernel_all_substitute +begin + +(* prove *_impl theorems *) +local_setup \GammaLift.prove_impls special_proc_name "\0" "\"\ + +(* prove *_modifies theorems in \ *) +local_setup \ + (fn lthy => + Context_Position.set_visible false lthy |> + Modifies_Proofs.prove_all_modifies_goals_local + (CalculateState.get_csenv @{theory} "../c/build/$L4V_ARCH/kernel_all.c_pp" |> the) + "\" + (fn _ => true) + [@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}] |> + Context_Position.restore_visible lthy) +\ + +end + +end diff --git a/spec/cspec/RISCV64/Kernel_C.thy b/spec/cspec/RISCV64/Kernel_C.thy index 272551601b..36d123eac6 100644 --- a/spec/cspec/RISCV64/Kernel_C.thy +++ b/spec/cspec/RISCV64/Kernel_C.thy @@ -88,7 +88,7 @@ lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix for these:\ diff --git a/spec/cspec/Substitute.thy b/spec/cspec/Substitute.thy index 420c1db1ed..393a40424d 100644 --- a/spec/cspec/Substitute.thy +++ b/spec/cspec/Substitute.thy @@ -92,9 +92,9 @@ fun prove_impl_tac ctxt ss = in simp_tac (put_simpset ss ctxt addsimps unfolds) n end); -fun convert_impls ctxt = let +fun convert_impls gamma ctxt = let - val thm = Proof_Context.get_thm ctxt "\_def" + val thm = Proof_Context.get_thm ctxt (gamma ^ "_def") val proc_defs = (Term.add_const_names (Thm.concl_of thm) []) |> filter (String.isSuffix Hoare.proc_deco) @@ -114,12 +114,12 @@ fun convert_impls ctxt = let in Local_Theory.notes (map (fn (n, t) => ((Binding.name n, []), [([t], [])])) saves) ctxt |> snd end -fun take_all_actions prefix src_ctxt proc tm csenv +fun take_all_actions prefix src_ctxt proc tm csenv gamma styargs ctxt = let val (_, ctxt) = convert prefix src_ctxt proc tm (Termtab.empty, ctxt); in ctxt - |> convert_impls - |> Modifies_Proofs.prove_all_modifies_goals_local csenv (fn _ => true) styargs + |> convert_impls gamma + (* |> Modifies_Proofs.prove_all_modifies_goals_local csenv gamma (fn _ => true) styargs *) end end @@ -190,7 +190,7 @@ abbreviation end -locale kernel_all_substitute = substitute_pre +locale kernel_all_substitute0 = substitute_pre begin ML \ @@ -355,8 +355,9 @@ SubstituteSpecs.take_all_actions o guard_halt o guard_htd_updates_with_domain o guard_acc_ptr_adds) - @{term kernel_all_global_addresses.\} + @{term kernel_all_global_addresses.\0} (CalculateState.get_csenv @{theory} "../c/build/$L4V_ARCH/kernel_all.c_pp" |> the) + "\0" [@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}] \ diff --git a/spec/cspec/X64/Kernel_C.thy b/spec/cspec/X64/Kernel_C.thy index 5b77943ff7..8f335ffc45 100644 --- a/spec/cspec/X64/Kernel_C.thy +++ b/spec/cspec/X64/Kernel_C.thy @@ -91,7 +91,7 @@ lemmas ctcb_offset_defs = ctcb_offset_def ctcb_size_bits_def cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS install_C_file "../c/build/$L4V_ARCH/kernel_all.c_pp" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] text \Hide unqualified names conflicting with Kernel_Config names. Force use of Kernel_C prefix for these:\ diff --git a/spec/cspec/multikernel/AARCH64/ArchMultikernel_C.thy b/spec/cspec/multikernel/AARCH64/ArchMultikernel_C.thy new file mode 100644 index 0000000000..bb9679f043 --- /dev/null +++ b/spec/cspec/multikernel/AARCH64/ArchMultikernel_C.thy @@ -0,0 +1,64 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory ArchMultikernel_C +imports Substitute +begin + +(* Example definition for how physBase could vary in a multikernel. + To be generated from config eventually *) +definition ph_base :: "nat \ 32 word" where + "ph_base n = 0x80000000 + 0x00010000 * of_nat n" + +(* Procedure body that depends on an additional logical parameter *) +definition + "physBase_of_cpu n \ TRY + creturn global_exn_var_'_update ret__unsigned_long_'_update (\s. UCAST(32 \ 64) (ph_base n));; + Guard DontReach {} SKIP + CATCH SKIP + END" + +locale kernel_all_substitute = kernel_all_substitute0 + + fixes cpuNum :: nat +begin + +(* Override procedure environment from kernel source to get paramteric behaviour *) +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +(* Provide physBase implementation theorem expected by vcg. Other *_impl theorems will be + generated automatically in Multikernel_C.thy *) +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +(* vcg and similar tools expect physBase_body_def to unfold to a SIMPL command *) +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Do the same for kernel_all_global_addresses *) +locale kernel_all_multi = kernel_all_global_addresses + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Interface to generic proof procedures in Multikernel_C.thy *) +ML \ + val special_proc_name = "physBase" +\ + +end diff --git a/spec/cspec/multikernel/ARM/ArchMultikernel_C.thy b/spec/cspec/multikernel/ARM/ArchMultikernel_C.thy new file mode 100644 index 0000000000..a1c4bfb3db --- /dev/null +++ b/spec/cspec/multikernel/ARM/ArchMultikernel_C.thy @@ -0,0 +1,64 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory ArchMultikernel_C +imports Substitute +begin + +(* Example definition for how physBase could vary in a multikernel. + To be generated from config eventually *) +definition ph_base :: "nat \ 32 signed word" where + "ph_base n = 0x10000000 + 0x00010000 * of_nat n" + +(* Procedure body that depends on an additional logical parameter *) +definition + "physBase_of_cpu n \ TRY + creturn global_exn_var_'_update ret__unsigned_long_'_update (\s. SCAST(32 signed \ 32) (ph_base n));; + Guard DontReach {} SKIP + CATCH SKIP + END" + +locale kernel_all_substitute = kernel_all_substitute0 + + fixes cpuNum :: nat +begin + +(* Override procedure environment from kernel source to get paramteric behaviour *) +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +(* Provide physBase implementation theorem expected by vcg. Other *_impl theorems will be + generated automatically in Multikernel_C.thy *) +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +(* vcg and similar tools expect physBase_body_def to unfold to a SIMPL command *) +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Do the same for kernel_all_global_addresses *) +locale kernel_all_multi = kernel_all_global_addresses + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Interface to generic proof procedures in Multikernel_C.thy *) +ML \ + val special_proc_name = "physBase" +\ + +end diff --git a/spec/cspec/multikernel/ARM_HYP/ArchMultikernel_C.thy b/spec/cspec/multikernel/ARM_HYP/ArchMultikernel_C.thy new file mode 100644 index 0000000000..3c7679ee19 --- /dev/null +++ b/spec/cspec/multikernel/ARM_HYP/ArchMultikernel_C.thy @@ -0,0 +1,64 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory ArchMultikernel_C +imports Substitute +begin + +(* Example definition for how physBase could vary in a multikernel. + To be generated from config eventually *) +definition ph_base :: "nat \ machine_word" where + "ph_base n = physBase + 0x00010000 * of_nat n" + +(* Procedure body that depends on an additional logical parameter *) +definition + "physBase_of_cpu n \ TRY + creturn global_exn_var_'_update ret__unsigned_long_'_update (\s. ucast (ph_base n));; + Guard DontReach {} SKIP + CATCH SKIP + END" + +locale kernel_all_substitute = kernel_all_substitute0 + + fixes cpuNum :: nat +begin + +(* Override procedure environment from kernel source to get paramteric behaviour *) +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +(* Provide physBase implementation theorem expected by vcg. Other *_impl theorems will be + generated automatically in Multikernel_C.thy *) +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +(* vcg and similar tools expect physBase_body_def to unfold to a SIMPL command *) +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Do the same for kernel_all_global_addresses *) +locale kernel_all_multi = kernel_all_global_addresses + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Interface to generic proof procedures in Multikernel_C.thy *) +ML \ + val special_proc_name = "physBase" +\ + +end diff --git a/spec/cspec/multikernel/RISCV64/ArchMultikernel_C.thy b/spec/cspec/multikernel/RISCV64/ArchMultikernel_C.thy new file mode 100644 index 0000000000..33ab5c2471 --- /dev/null +++ b/spec/cspec/multikernel/RISCV64/ArchMultikernel_C.thy @@ -0,0 +1,65 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory ArchMultikernel_C +imports Substitute +begin + +(* Example definition for how physBase could vary in a multikernel. + To be generated from config eventually *) +definition ph_base :: "nat \ machine_word" where + "ph_base n = physBase + 0x00010000 * of_nat n" + +(* Procedure body that depends on an additional logical parameter *) +definition + "physBase_of_cpu n \ TRY + creturn global_exn_var_'_update ret__unsigned_long_'_update (\s. ph_base n);; + Guard DontReach {} SKIP + CATCH SKIP + END" + +locale kernel_all_substitute = kernel_all_substitute0 + + fixes cpuNum :: nat +begin + +(* Override procedure environment from kernel source to get paramteric behaviour *) +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +(* Provide physBase implementation theorem expected by vcg. Other *_impl theorems will be + generated automatically in Multikernel_C.thy *) +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +(* vcg and similar tools expect physBase_body_def to unfold to a SIMPL command *) +lemmas physBase_body_def = physBase_of_cpu_def + +end + +(* Do the same for kernel_all_global_addresses *) +locale kernel_all_multi = kernel_all_global_addresses + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (physBase_'proc \ physBase_of_cpu cpuNum)" + +lemma physBase_impl: + "\ physBase_'proc = Some (physBase_of_cpu cpuNum)" + by (simp add: \_def) + +lemmas physBase_body_def = physBase_of_cpu_def + +end + + +(* Interface to generic proof procedures in Multikernel_C.thy *) +ML \ + val special_proc_name = "physBase" +\ + +end diff --git a/spec/cspec/multikernel/X64/ArchMultikernel_C.thy b/spec/cspec/multikernel/X64/ArchMultikernel_C.thy new file mode 100644 index 0000000000..435ad5f99e --- /dev/null +++ b/spec/cspec/multikernel/X64/ArchMultikernel_C.thy @@ -0,0 +1,54 @@ +(* + * Copyright 2025, Proofcraft Pty Ltd + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory ArchMultikernel_C +imports Substitute +begin + +(* There is no physBase on x64, but we still want the top-level of \ to be a function update. + The function also must mention cpuNum, otherwise \ will not depend on cpuNum outside the + locale, which means its type would not line up with \ in other architectures and generic + proofs would fail. The following dummy definition is used below to achieve the + cpuNum-dependent function update. *) +definition + "addrFromKPPtr_body' n \ kernel_all_global_addresses.addrFromKPPtr_body" + + +locale kernel_all_substitute = kernel_all_substitute0 + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (addrFromKPPtr_'proc \ addrFromKPPtr_body' cpuNum)" + +(* Provide implementation theorem expected by vcg. Other *_impl theorems will be + generated automatically in Multikernel_C.thy *) +lemma addrFromKPPtr_impl: + "\ addrFromKPPtr_'proc = Some addrFromKPPtr_body" + by (simp add: \_def addrFromKPPtr_body'_def) + +end + +(* Do the same for kernel_all_global_addresses *) +locale kernel_all_multi = kernel_all_global_addresses + + fixes cpuNum :: nat +begin + +definition + "\ \ \0 (addrFromKPPtr_'proc \ addrFromKPPtr_body' cpuNum)" + +lemma addrFromKPPtr_impl: + "\ addrFromKPPtr_'proc = Some addrFromKPPtr_body" + by (simp add: \_def addrFromKPPtr_body'_def) + +end + +(* Interface to generic proof procedures in Multikernel_C.thy *) +ML \ + val special_proc_name = "addrFromKPPtr" +\ + +end From ebb04ad90c9e36a62864dd379807416346d96f84 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 31 Jul 2025 11:55:26 +1000 Subject: [PATCH 4/7] crefine lib: automatic substitute refinement Adjust the automatic refinement proof to work for Gammas where one function is overridden. Signed-off-by: Gerwin Klein --- proof/crefine/lib/CToCRefine.thy | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/proof/crefine/lib/CToCRefine.thy b/proof/crefine/lib/CToCRefine.thy index 0d1f4b0c2b..a5774d88b4 100644 --- a/proof/crefine/lib/CToCRefine.thy +++ b/proof/crefine/lib/CToCRefine.thy @@ -7,12 +7,18 @@ theory CToCRefine imports - "CSpec.Substitute" + "CSpec.Multikernel_C" "CLib.SimplRewrite" Lib.Lib "CParser.TypHeapLib" begin +lemma spec_statefn_simulates_fun_upd: + "\ exec_statefn_simulates g UNIV UNIV v v'; + spec_statefn_simulates g G G' \ + \ spec_statefn_simulates g (G(p := Some v)) (G'(p := Some v'))" + by (simp add: spec_statefn_simulates_def) + lemma spec_statefn_simulates_lookup_tree_Node: "\ exec_statefn_simulates g UNIV UNIV v v'; spec_statefn_simulates g (lookup_tree a f) (lookup_tree c f); @@ -44,28 +50,22 @@ val unfold_bodies = Simplifier.make_simproc @{context} theorem spec_refine: notes if_split[split del] shows - "spec_statefn_simulates id (kernel_all_global_addresses.\ symbol_table) - (kernel_all_substitute.\ symbol_table domain)" - apply (simp add: kernel_all_global_addresses.\_def kernel_all_substitute.\_def) + "spec_statefn_simulates id (kernel_all_multi.\ symbol_table cpuNum) + (kernel_all_substitute.\ symbol_table domain cpuNum)" + apply (simp add: kernel_all_multi.\_def kernel_all_substitute.\_def) + apply (rule spec_statefn_simulates_fun_upd, rule exec_statefn_simulates_comI) + apply (simp add: kernel_all_global_addresses.\0_def kernel_all_substitute0.\0_def) apply (intro spec_statefn_simulates_lookup_tree_Node spec_statefn_simulates_lookup_tree_Leaf) apply (tactic \ALLGOALS (asm_simp_tac (put_simpset HOL_ss @{context} addsimps @{thms switch.simps fst_conv snd_conv} addsimprocs [unfold_bodies] |> Splitter.del_split @{thm if_split})) THEN ALLGOALS (TRY o resolve_tac @{context} @{thms exec_statefn_simulates_refl})\) - apply (tactic \ALLGOALS (REPEAT_ALL_NEW (resolve_tac @{context} @{thms exec_statefn_simulates_comI exec_statefn_simulates_additionals}))\) apply (unfold id_apply) apply (tactic \ALLGOALS (TRY o resolve_tac @{context} @{thms refl bij_id})\) apply (tactic \ALLGOALS (TRY o (resolve_tac @{context} @{thms subsetI} THEN' resolve_tac @{context} @{thms CollectI} THEN' REPEAT_ALL_NEW (eresolve_tac @{context} @{thms IntE CollectE conjE exE h_t_valid_c_guard conjI} ORELSE' assume_tac @{context})))\) - (* - apply (tactic {* ALLGOALS (TRY o ((REPEAT_ALL_NEW (rtac @{thm c_guard_field}) THEN' etac @{thm h_t_valid_c_guard}) - THEN_ALL_NEW simp_tac @{simpset} - THEN_ALL_NEW simp_tac @{simpset} - THEN_ALL_NEW K no_tac)) *}) - *) apply (rule bij_id[simplified id_def])+ done (* Woo! *) end - From cb5f7f827e78a521f53881a5cb02f33a1d74d2be Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 31 Jul 2025 11:57:12 +1000 Subject: [PATCH 5/7] crefine: proof updates for Gamma parameterisation - use kernel_all_global_addresses base locale for constants -- these are not modified by kernel_all_substitute and the base version is the most stable name. - assume `cpuNum = 0` in Machine_C for current unicore proof; use explicit cpuNum assumption in the one lemma before Machine_C that depends on cpuNum. - adjust theory imports + locale names and parameters as needed Signed-off-by: Gerwin Klein --- proof/crefine/AARCH64/ADT_C.thy | 4 ++-- proof/crefine/AARCH64/Ipc_C.thy | 7 ++++--- proof/crefine/AARCH64/Machine_C.thy | 5 ++++- proof/crefine/AARCH64/Refine_C.thy | 12 ++++++------ proof/crefine/AARCH64/SR_lemmas_C.thy | 4 ++-- proof/crefine/AARCH64/SyscallArgs_C.thy | 4 ++-- proof/crefine/AARCH64/Tcb_C.thy | 8 ++++---- proof/crefine/AARCH64/VSpace_C.thy | 6 +++--- proof/crefine/AARCH64/Wellformed_C.thy | 2 +- proof/crefine/ARM/ADT_C.thy | 2 +- proof/crefine/ARM/Ipc_C.thy | 7 ++++--- proof/crefine/ARM/Machine_C.thy | 5 +++++ proof/crefine/ARM/Refine_C.thy | 12 ++++++------ proof/crefine/ARM/SR_lemmas_C.thy | 4 ++-- proof/crefine/ARM/SyscallArgs_C.thy | 4 ++-- proof/crefine/ARM/Tcb_C.thy | 8 ++++---- proof/crefine/ARM/VSpace_C.thy | 10 +++++----- proof/crefine/ARM/Wellformed_C.thy | 2 +- proof/crefine/ARM_HYP/ADT_C.thy | 2 +- proof/crefine/ARM_HYP/Arch_C.thy | 2 +- proof/crefine/ARM_HYP/Ipc_C.thy | 7 ++++--- proof/crefine/ARM_HYP/Machine_C.thy | 5 +++++ proof/crefine/ARM_HYP/Refine_C.thy | 12 ++++++------ proof/crefine/ARM_HYP/SR_lemmas_C.thy | 4 ++-- proof/crefine/ARM_HYP/SyscallArgs_C.thy | 4 ++-- proof/crefine/ARM_HYP/Tcb_C.thy | 8 ++++---- proof/crefine/ARM_HYP/VSpace_C.thy | 10 +++++----- proof/crefine/ARM_HYP/Wellformed_C.thy | 2 +- proof/crefine/RISCV64/ADT_C.thy | 4 ++-- proof/crefine/RISCV64/Ipc_C.thy | 6 +++--- proof/crefine/RISCV64/Machine_C.thy | 4 ++++ proof/crefine/RISCV64/Refine_C.thy | 12 ++++++------ proof/crefine/RISCV64/SR_lemmas_C.thy | 4 ++-- proof/crefine/RISCV64/SyscallArgs_C.thy | 4 ++-- proof/crefine/RISCV64/Tcb_C.thy | 8 ++++---- proof/crefine/RISCV64/VSpace_C.thy | 6 +++--- proof/crefine/RISCV64/Wellformed_C.thy | 2 +- proof/crefine/X64/ADT_C.thy | 4 ++-- proof/crefine/X64/Ipc_C.thy | 6 +++--- proof/crefine/X64/Refine_C.thy | 12 ++++++------ proof/crefine/X64/SyscallArgs_C.thy | 4 ++-- proof/crefine/X64/Tcb_C.thy | 8 ++++---- proof/crefine/X64/VSpace_C.thy | 4 ++-- proof/crefine/X64/Wellformed_C.thy | 2 +- proof/crefine/lib/AutoCorresModifiesProofs.thy | 2 +- 45 files changed, 137 insertions(+), 117 deletions(-) diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy index 94e8fd3af1..ec3d02cb7b 100644 --- a/proof/crefine/AARCH64/ADT_C.thy +++ b/proof/crefine/AARCH64/ADT_C.thy @@ -1692,8 +1692,8 @@ where end -locale kernel_global = state_rel + kernel_all_global_addresses -(* repeating ADT definitions in the c-parser's locale now (not the substitute) *) +locale kernel_global = state_rel + kernel_all_multi +(* repeating ADT definitions in the (multikernel-adjusted) C parser's locale now, not the substitute *) begin definition diff --git a/proof/crefine/AARCH64/Ipc_C.thy b/proof/crefine/AARCH64/Ipc_C.thy index 1b8ff37839..f486b3938a 100644 --- a/proof/crefine/AARCH64/Ipc_C.thy +++ b/proof/crefine/AARCH64/Ipc_C.thy @@ -295,9 +295,9 @@ lemma ccap_relation_reply_helpers: (*FIXME: arch-split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" -lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def -abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" -lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def +lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def +abbreviation "exceptionMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]" +lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def lemma syscallMessage_ccorres: "n < unat n_syscallMessage @@ -6072,6 +6072,7 @@ lemma receiveIPC_ccorres [corres]: apply (auto simp: isCap_simps valid_cap'_def) done + lemma sendSignal_dequeue_ccorres_helper: "ccorres (\rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_' (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest diff --git a/proof/crefine/AARCH64/Machine_C.thy b/proof/crefine/AARCH64/Machine_C.thy index fa4385e150..e0580e2bf5 100644 --- a/proof/crefine/AARCH64/Machine_C.thy +++ b/proof/crefine/AARCH64/Machine_C.thy @@ -21,8 +21,11 @@ instance virq_C :: array_inner_packed locale kernel_m = kernel + -(* timer and IRQ common machine ops (function names exist on other platforms *) +(* The current verification is for unicore only *) +assumes cpu_0: + "cpuNum = 0" +(* timer and IRQ common machine ops (function names exist on other platforms *) assumes resetTimer_ccorres: "ccorres dc xfdc \ UNIV [] (doMachineOp resetTimer) diff --git a/proof/crefine/AARCH64/Refine_C.thy b/proof/crefine/AARCH64/Refine_C.thy index 345f508bca..34f56a2853 100644 --- a/proof/crefine/AARCH64/Refine_C.thy +++ b/proof/crefine/AARCH64/Refine_C.thy @@ -1229,8 +1229,8 @@ lemma ccorres_underlying_Fault: lemma monadic_rewrite_\: "monadic_rewrite True False \ (exec_C \ c) - (exec_C (kernel_all_global_addresses.\ symbol_table) c)" - using spec_refine [of symbol_table domain] + (exec_C (kernel_all_multi.\ symbol_table cpuNum) c)" + using spec_refine [of symbol_table cpuNum domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn o_def map_option_case monadic_rewrite_def exec_C_def @@ -1247,8 +1247,8 @@ lemma no_fail_getActiveIRQ_C: done lemma kernel_all_subset_kernel: - "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) - (kernel_global.kernel_call_C symbol_table fp) + "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop) + (kernel_global.kernel_call_C symbol_table cpuNum fp) \ global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def relcomp_unfold in_lift_state_relation_eq) @@ -1298,7 +1298,7 @@ lemma kernel_all_subset_kernel: done theorem true_refinement: - "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) @@ -1310,7 +1310,7 @@ theorem true_refinement: done theorem true_fp_refinement: - "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) diff --git a/proof/crefine/AARCH64/SR_lemmas_C.thy b/proof/crefine/AARCH64/SR_lemmas_C.thy index e7c70bc949..5fb3ec68b1 100644 --- a/proof/crefine/AARCH64/SR_lemmas_C.thy +++ b/proof/crefine/AARCH64/SR_lemmas_C.thy @@ -2567,9 +2567,9 @@ lemma unat_scast_numDomains: (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *) lemma physBase_spec: - "\s. \\ {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }" + "\s. \\ {s} Call physBase_'proc {t. cpuNum = 0 \ ret__unsigned_long_' t = Kernel_Config.physBase }" apply (rule allI, rule conseqPre, vcg) - apply (simp add: Kernel_Config.physBase_def) + apply (simp add: Kernel_Config.physBase_def ph_base_def) done lemma rf_sr_obj_update_helper: diff --git a/proof/crefine/AARCH64/SyscallArgs_C.thy b/proof/crefine/AARCH64/SyscallArgs_C.thy index 1fd8aa919a..0744e0fb07 100644 --- a/proof/crefine/AARCH64/SyscallArgs_C.thy +++ b/proof/crefine/AARCH64/SyscallArgs_C.thy @@ -15,8 +15,8 @@ begin (*FIXME: arch-split: C kernel names hidden by Haskell names *) context kernel_m begin -abbreviation "msgRegistersC \ kernel_all_substitute.msgRegisters" -lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def +abbreviation "msgRegistersC \ kernel_all_global_addresses.msgRegisters" +lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def end context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/AARCH64/Tcb_C.thy b/proof/crefine/AARCH64/Tcb_C.thy index ea516a773e..4f0edae921 100644 --- a/proof/crefine/AARCH64/Tcb_C.thy +++ b/proof/crefine/AARCH64/Tcb_C.thy @@ -1106,10 +1106,10 @@ lemma Arch_performTransfer_ccorres: done (*FIXME: arch-split: C kernel names hidden by Haskell names *) -abbreviation "frameRegistersC \ kernel_all_substitute.frameRegisters" -lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def -abbreviation "gpRegistersC \ kernel_all_substitute.gpRegisters" -lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def +abbreviation "frameRegistersC \ kernel_all_global_addresses.frameRegisters" +lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def +abbreviation "gpRegistersC \ kernel_all_global_addresses.gpRegisters" +lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def lemma frame_gp_registers_convs: "length AARCH64_H.frameRegisters = unat n_frameRegisters" diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy index 2435d92d3c..04b215ff69 100644 --- a/proof/crefine/AARCH64/VSpace_C.thy +++ b/proof/crefine/AARCH64/VSpace_C.thy @@ -327,7 +327,7 @@ lemma addrFromKPPtr_spec: \\ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\" apply vcg apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def - kernelELFBase_def pptrBase_def mask_def) + kernelELFBase_def pptrBase_def mask_def cpu_0) done (* FIXME: move *) @@ -1576,8 +1576,8 @@ lemma setRegister_ccorres: lemma msgRegisters_ccorres: "n < unat n_msgRegisters \ - register_from_H (AARCH64_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" - apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) + register_from_H (AARCH64_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)" + apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def nth_Cons' split: if_split) done diff --git a/proof/crefine/AARCH64/Wellformed_C.thy b/proof/crefine/AARCH64/Wellformed_C.thy index 675730d8dd..b377d12fd6 100644 --- a/proof/crefine/AARCH64/Wellformed_C.thy +++ b/proof/crefine/AARCH64/Wellformed_C.thy @@ -12,7 +12,7 @@ theory Wellformed_C imports "CLib.CTranslationNICTA" CLevityCatch - "CSpec.Substitute" + "CSpec.Multikernel_C" begin context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/ARM/ADT_C.thy b/proof/crefine/ARM/ADT_C.thy index 89bb23572d..63eb4f6640 100644 --- a/proof/crefine/ARM/ADT_C.thy +++ b/proof/crefine/ARM/ADT_C.thy @@ -1552,7 +1552,7 @@ where end -locale kernel_global = state_rel + kernel_all_global_addresses +locale kernel_global = state_rel + kernel_all_multi (* note we're in the c-parser's locale now, not the substitute *) begin diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy index dbc8002df9..18bc7a6f5f 100644 --- a/proof/crefine/ARM/Ipc_C.thy +++ b/proof/crefine/ARM/Ipc_C.thy @@ -278,9 +278,9 @@ lemma ccap_relation_reply_helpers: (*FIXME: arch-split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" -lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def -abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" -lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def +lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def +abbreviation "exceptionMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]" +lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def lemma syscallMessage_ccorres: "n < unat n_syscallMessage @@ -5551,6 +5551,7 @@ lemma receiveIPC_ccorres [corres]: apply (auto simp: isCap_simps valid_cap'_def) done + lemma sendSignal_dequeue_ccorres_helper: "ccorres (\rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest_' (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest diff --git a/proof/crefine/ARM/Machine_C.thy b/proof/crefine/ARM/Machine_C.thy index e9be3743d6..f08e505cd9 100644 --- a/proof/crefine/ARM/Machine_C.thy +++ b/proof/crefine/ARM/Machine_C.thy @@ -15,6 +15,11 @@ imports Ctac_lemmas_C begin locale kernel_m = kernel + + +(* The current verification is for unicore only *) +assumes cpu_0: + "cpuNum = 0" + assumes resetTimer_ccorres: "ccorres dc xfdc \ UNIV [] (doMachineOp resetTimer) diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index 7c4c8efe09..9b6a6b19cd 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -1079,8 +1079,8 @@ lemma ccorres_underlying_Fault: lemma monadic_rewrite_\: "monadic_rewrite True False \ (exec_C \ c) - (exec_C (kernel_all_global_addresses.\ symbol_table) c)" - using spec_refine [of symbol_table domain] + (exec_C (kernel_all_multi.\ symbol_table cpuNum) c)" + using spec_refine [of symbol_table cpuNum domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn o_def map_option_case monadic_rewrite_def exec_C_def @@ -1097,8 +1097,8 @@ lemma no_fail_getActiveIRQ_C: done lemma kernel_all_subset_kernel: - "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) - (kernel_global.kernel_call_C symbol_table fp) + "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop) + (kernel_global.kernel_call_C symbol_table cpuNum fp) \ global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def relcomp_unfold in_lift_state_relation_eq) @@ -1148,7 +1148,7 @@ lemma kernel_all_subset_kernel: done theorem true_refinement: - "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) @@ -1160,7 +1160,7 @@ theorem true_refinement: done theorem true_fp_refinement: - "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) diff --git a/proof/crefine/ARM/SR_lemmas_C.thy b/proof/crefine/ARM/SR_lemmas_C.thy index f83ddcda40..7710d78d88 100644 --- a/proof/crefine/ARM/SR_lemmas_C.thy +++ b/proof/crefine/ARM/SR_lemmas_C.thy @@ -2201,9 +2201,9 @@ lemma msgRegisters_size_sanity: (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *) lemma physBase_spec: - "\s. \\ {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }" + "\s. \\ {s} Call physBase_'proc {t. cpuNum = 0 \ ret__unsigned_long_' t = Kernel_Config.physBase }" apply (rule allI, rule conseqPre, vcg) - apply (simp add: Kernel_Config.physBase_def) + apply (simp add: Kernel_Config.physBase_def ph_base_def) done lemma rf_sr_obj_update_helper: diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index 212d0b8749..df2a7c0a9b 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -14,8 +14,8 @@ begin (*FIXME: arch-split: C kernel names hidden by Haskell names *) context kernel_m begin -abbreviation "msgRegistersC \ kernel_all_substitute.msgRegisters" -lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def +abbreviation "msgRegistersC \ kernel_all_global_addresses.msgRegisters" +lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def end context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 765a84fa06..6383e9a761 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -1036,10 +1036,10 @@ lemma Arch_performTransfer_ccorres: done (*FIXME: arch-split: C kernel names hidden by Haskell names *) -abbreviation "frameRegistersC \ kernel_all_substitute.frameRegisters" -lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def -abbreviation "gpRegistersC \ kernel_all_substitute.gpRegisters" -lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def +abbreviation "frameRegistersC \ kernel_all_global_addresses.frameRegisters" +lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def +abbreviation "gpRegistersC \ kernel_all_global_addresses.gpRegisters" +lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def lemma frame_gp_registers_convs: "length ARM_H.frameRegisters = unat n_frameRegisters" diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy index 4dbe25a60a..9fadf50e23 100644 --- a/proof/crefine/ARM/VSpace_C.thy +++ b/proof/crefine/ARM/VSpace_C.thy @@ -710,7 +710,7 @@ lemma ptrFromPAddr_spec: Call ptrFromPAddr_'proc \\ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\" apply vcg - apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def) + apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def cpu_0) done lemma addrFromPPtr_spec: @@ -718,7 +718,7 @@ lemma addrFromPPtr_spec: Call addrFromPPtr_'proc \\ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\" apply vcg - apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def) + apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def cpu_0) done lemma addrFromKPPtr_spec: @@ -727,7 +727,7 @@ lemma addrFromKPPtr_spec: \\ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\" apply vcg apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def - kernelELFBase_def pptrBase_def mask_def) + kernelELFBase_def pptrBase_def mask_def cpu_0) done abbreviation @@ -1715,8 +1715,8 @@ lemma setRegister_ccorres: lemma msgRegisters_ccorres: "n < unat n_msgRegisters \ - register_from_H (ARM_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" - apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) + register_from_H (ARM_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)" + apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def nth_Cons' split: if_split) done diff --git a/proof/crefine/ARM/Wellformed_C.thy b/proof/crefine/ARM/Wellformed_C.thy index cbf82dbb6f..70efd2422e 100644 --- a/proof/crefine/ARM/Wellformed_C.thy +++ b/proof/crefine/ARM/Wellformed_C.thy @@ -11,7 +11,7 @@ theory Wellformed_C imports "CLib.CTranslationNICTA" CLevityCatch - "CSpec.Substitute" + "CSpec.Multikernel_C" begin context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/ARM_HYP/ADT_C.thy b/proof/crefine/ARM_HYP/ADT_C.thy index 5f0c2d5a54..759cbb1831 100644 --- a/proof/crefine/ARM_HYP/ADT_C.thy +++ b/proof/crefine/ARM_HYP/ADT_C.thy @@ -1718,7 +1718,7 @@ where end -locale kernel_global = state_rel + kernel_all_global_addresses +locale kernel_global = state_rel + kernel_all_multi (* note we're in the c-parser's locale now, not the substitute *) begin diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index 1f63c6c5d1..03ca82edb4 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/proof/crefine/ARM_HYP/Arch_C.thy @@ -2776,7 +2776,7 @@ lemma decodeARMFrameInvocation_ccorres: apply (clarsimp dest!: ccap_relation_PageCap_generics) apply (clarsimp simp: hd_drop_conv_nth hd_conv_nth) (* sync up preprocessor-defined number sources coming from C *) - apply (clarsimp simp: fromPAddr_def paddrTop_def pptrBase_def pptrTop_def + apply (clarsimp simp: fromPAddr_def paddrTop_def pptrBase_def pptrTop_def cpu_0 pptrBaseOffset_def add.commute from_bool_eq_if') apply ceqv diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index 4b9b60e98a..ffbe0edb4e 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -349,9 +349,9 @@ lemma ccap_relation_reply_helpers: (*FIXME: arch-split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" -lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def -abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" -lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def +lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def +abbreviation "exceptionMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]" +lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def lemma syscallMessage_ccorres: "n < unat n_syscallMessage @@ -6076,6 +6076,7 @@ lemma receiveIPC_ccorres [corres]: apply (auto simp: isCap_simps valid_cap'_def) done + lemma sendSignal_dequeue_ccorres_helper: "ccorres (\rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest_' (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest diff --git a/proof/crefine/ARM_HYP/Machine_C.thy b/proof/crefine/ARM_HYP/Machine_C.thy index ec407a80c9..555ab6910e 100644 --- a/proof/crefine/ARM_HYP/Machine_C.thy +++ b/proof/crefine/ARM_HYP/Machine_C.thy @@ -25,6 +25,11 @@ where "setCurrentPDPL2 = undefined" locale kernel_m = kernel + + +(* The current verification is for unicore only *) +assumes cpu_0: + "cpuNum = 0" + assumes resetTimer_ccorres: "ccorres dc xfdc \ UNIV [] (doMachineOp resetTimer) diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index ceb1ad8303..56fc70465b 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -1105,8 +1105,8 @@ lemma ccorres_underlying_Fault: lemma monadic_rewrite_\: "monadic_rewrite True False \ (exec_C \ c) - (exec_C (kernel_all_global_addresses.\ symbol_table) c)" - using spec_refine [of symbol_table domain] + (exec_C (kernel_all_multi.\ symbol_table cpuNum) c)" + using spec_refine [of symbol_table cpuNum domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn o_def map_option_case monadic_rewrite_def exec_C_def @@ -1123,8 +1123,8 @@ lemma no_fail_getActiveIRQ_C: done lemma kernel_all_subset_kernel: - "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) - (kernel_global.kernel_call_C symbol_table fp) + "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop) + (kernel_global.kernel_call_C symbol_table cpuNum fp) \ global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def relcomp_unfold in_lift_state_relation_eq) @@ -1174,7 +1174,7 @@ lemma kernel_all_subset_kernel: done theorem true_refinement: - "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) @@ -1186,7 +1186,7 @@ theorem true_refinement: done theorem true_fp_refinement: - "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) diff --git a/proof/crefine/ARM_HYP/SR_lemmas_C.thy b/proof/crefine/ARM_HYP/SR_lemmas_C.thy index 87b97b6f6d..f39166765b 100644 --- a/proof/crefine/ARM_HYP/SR_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/SR_lemmas_C.thy @@ -2532,9 +2532,9 @@ lemma unat_scast_numDomains: (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *) lemma physBase_spec: - "\s. \\ {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }" + "\s. \\ {s} Call physBase_'proc {t. cpuNum = 0 \ ret__unsigned_long_' t = Kernel_Config.physBase }" apply (rule allI, rule conseqPre, vcg) - apply (simp add: Kernel_Config.physBase_def) + apply (simp add: Kernel_Config.physBase_def ph_base_def) done lemma rf_sr_obj_update_helper: diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index f77a7de87b..3d4bf4ce33 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -14,8 +14,8 @@ begin (*FIXME: arch-split: C kernel names hidden by Haskell names *) context kernel_m begin -abbreviation "msgRegistersC \ kernel_all_substitute.msgRegisters" -lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def +abbreviation "msgRegistersC \ kernel_all_global_addresses.msgRegisters" +lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def end context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index 12bebbefe3..3dfab2b7f4 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -1097,10 +1097,10 @@ lemma Arch_performTransfer_ccorres: done (*FIXME: arch-split: C kernel names hidden by Haskell names *) -abbreviation "frameRegistersC \ kernel_all_substitute.frameRegisters" -lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def -abbreviation "gpRegistersC \ kernel_all_substitute.gpRegisters" -lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def +abbreviation "frameRegistersC \ kernel_all_global_addresses.frameRegisters" +lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def +abbreviation "gpRegistersC \ kernel_all_global_addresses.gpRegisters" +lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def lemma frame_gp_registers_convs: "length ARM_HYP_H.frameRegisters = unat n_frameRegisters" diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy index c01caf9128..21ec1a709b 100644 --- a/proof/crefine/ARM_HYP/VSpace_C.thy +++ b/proof/crefine/ARM_HYP/VSpace_C.thy @@ -782,7 +782,7 @@ lemma ptrFromPAddr_spec: Call ptrFromPAddr_'proc \\ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\" apply vcg - apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def) + apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def cpu_0) done lemma addrFromPPtr_spec: @@ -790,7 +790,7 @@ lemma addrFromPPtr_spec: Call addrFromPPtr_'proc \\ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\" apply vcg - apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def) + apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def cpu_0) done lemma addrFromKPPtr_spec: @@ -799,7 +799,7 @@ lemma addrFromKPPtr_spec: \\ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\" apply vcg apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def - kernelELFBase_def pptrBase_def mask_def) + kernelELFBase_def pptrBase_def mask_def cpu_0) done abbreviation @@ -2833,8 +2833,8 @@ lemma setRegister_ccorres: lemma msgRegisters_ccorres: "n < unat n_msgRegisters \ - register_from_H (ARM_HYP_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" - apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) + register_from_H (ARM_HYP_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)" + apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: if_split) done diff --git a/proof/crefine/ARM_HYP/Wellformed_C.thy b/proof/crefine/ARM_HYP/Wellformed_C.thy index 69c0888aec..bfa064634f 100644 --- a/proof/crefine/ARM_HYP/Wellformed_C.thy +++ b/proof/crefine/ARM_HYP/Wellformed_C.thy @@ -11,7 +11,7 @@ theory Wellformed_C imports "CLib.CTranslationNICTA" CLevityCatch - "CSpec.Substitute" + "CSpec.Multikernel_C" begin context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/RISCV64/ADT_C.thy b/proof/crefine/RISCV64/ADT_C.thy index d821f38722..462837ac4b 100644 --- a/proof/crefine/RISCV64/ADT_C.thy +++ b/proof/crefine/RISCV64/ADT_C.thy @@ -1532,8 +1532,8 @@ where end -locale kernel_global = state_rel + kernel_all_global_addresses -(* repeating ADT definitions in the c-parser's locale now (not the substitute) *) +locale kernel_global = state_rel + kernel_all_multi +(* repeating ADT definitions in the (multikernel-adjusted) C parser's locale now, not the substitute *) begin definition diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index b92a59aced..f1517670be 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -297,9 +297,9 @@ lemma ccap_relation_reply_helpers: (*FIXME: arch-split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" -lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def -abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" -lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def +lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def +abbreviation "exceptionMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]" +lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def lemma syscallMessage_ccorres: "n < unat n_syscallMessage diff --git a/proof/crefine/RISCV64/Machine_C.thy b/proof/crefine/RISCV64/Machine_C.thy index 30d0579c9f..9b8fdcce4d 100644 --- a/proof/crefine/RISCV64/Machine_C.thy +++ b/proof/crefine/RISCV64/Machine_C.thy @@ -17,6 +17,10 @@ begin locale kernel_m = kernel + +(* The current verification is for unicore only *) +assumes cpu_0: + "cpuNum = 0" + assumes setVSpaceRoot_ccorres: "ccorres dc xfdc \ (\\addr___unsigned_long = pt\ \ \\asid___unsigned_long = asid\) [] (doMachineOp (RISCV64.setVSpaceRoot pt asid)) diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index 66c9e92058..978d9b4ab4 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -1090,8 +1090,8 @@ lemma ccorres_underlying_Fault: lemma monadic_rewrite_\: "monadic_rewrite True False \ (exec_C \ c) - (exec_C (kernel_all_global_addresses.\ symbol_table) c)" - using spec_refine [of symbol_table domain] + (exec_C (kernel_all_multi.\ symbol_table cpuNum) c)" + using spec_refine [of symbol_table cpuNum domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn o_def map_option_case monadic_rewrite_def exec_C_def @@ -1108,8 +1108,8 @@ lemma no_fail_getActiveIRQ_C: done lemma kernel_all_subset_kernel: - "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) - (kernel_global.kernel_call_C symbol_table fp) + "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop) + (kernel_global.kernel_call_C symbol_table cpuNum fp) \ global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def relcomp_unfold in_lift_state_relation_eq) @@ -1159,7 +1159,7 @@ lemma kernel_all_subset_kernel: done theorem true_refinement: - "kernel_global.ADT_C symbol_table riscvKSKernelVSpace_C uop + "kernel_global.ADT_C symbol_table riscvKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) @@ -1172,7 +1172,7 @@ theorem true_refinement: (* FIXME: fastpath theorem true_fp_refinement: - "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) diff --git a/proof/crefine/RISCV64/SR_lemmas_C.thy b/proof/crefine/RISCV64/SR_lemmas_C.thy index 45ca112b2f..7326f2cbb6 100644 --- a/proof/crefine/RISCV64/SR_lemmas_C.thy +++ b/proof/crefine/RISCV64/SR_lemmas_C.thy @@ -2141,9 +2141,9 @@ lemma unat_scast_numDomains: (* link up Kernel_Config loaded from the seL4 build system with physBase in C code *) lemma physBase_spec: - "\s. \\ {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }" + "\s. \\ {s} Call physBase_'proc {t. cpuNum = 0 \ ret__unsigned_long_' t = Kernel_Config.physBase }" apply (rule allI, rule conseqPre, vcg) - apply (simp add: Kernel_Config.physBase_def) + apply (simp add: Kernel_Config.physBase_def ph_base_def) done lemma rf_sr_obj_update_helper: diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index 679b366ee9..75a35be6d1 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -15,8 +15,8 @@ begin (*FIXME: arch-split: C kernel names hidden by Haskell names *) context kernel_m begin -abbreviation "msgRegistersC \ kernel_all_substitute.msgRegisters" -lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def +abbreviation "msgRegistersC \ kernel_all_global_addresses.msgRegisters" +lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def end context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 2a2825ab88..5ed2407a58 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -1114,10 +1114,10 @@ lemma Arch_performTransfer_ccorres: done (*FIXME: arch-split: C kernel names hidden by Haskell names *) -abbreviation "frameRegistersC \ kernel_all_substitute.frameRegisters" -lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def -abbreviation "gpRegistersC \ kernel_all_substitute.gpRegisters" -lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def +abbreviation "frameRegistersC \ kernel_all_global_addresses.frameRegisters" +lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def +abbreviation "gpRegistersC \ kernel_all_global_addresses.gpRegisters" +lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def lemma frame_gp_registers_convs: "length RISCV64_H.frameRegisters = unat n_frameRegisters" diff --git a/proof/crefine/RISCV64/VSpace_C.thy b/proof/crefine/RISCV64/VSpace_C.thy index c6f99bbd71..58ab7dd102 100644 --- a/proof/crefine/RISCV64/VSpace_C.thy +++ b/proof/crefine/RISCV64/VSpace_C.thy @@ -867,7 +867,7 @@ lemma addrFromKPPtr_spec: Call addrFromKPPtr_'proc \\ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\" apply vcg - apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def + apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def cpu_0 kernelELFBase_def kernelELFPAddrBase_def mask_def pptrTop_def) done @@ -1027,8 +1027,8 @@ lemma setRegister_ccorres: lemma msgRegisters_ccorres: "n < unat n_msgRegisters \ - register_from_H (RISCV64_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" - apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) + register_from_H (RISCV64_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)" + apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def nth_Cons' split: if_split) done diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index 96d1dc95dd..765d4148fd 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -12,7 +12,7 @@ theory Wellformed_C imports "CLib.CTranslationNICTA" CLevityCatch - "CSpec.Substitute" + "CSpec.Multikernel_C" begin context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/X64/ADT_C.thy b/proof/crefine/X64/ADT_C.thy index a72388c58c..181a807443 100644 --- a/proof/crefine/X64/ADT_C.thy +++ b/proof/crefine/X64/ADT_C.thy @@ -1697,8 +1697,8 @@ where end -locale kernel_global = state_rel + kernel_all_global_addresses -(* repeating ADT definitions in the c-parser's locale now (not the substitute) *) +locale kernel_global = state_rel + kernel_all_multi +(* repeating ADT definitions in the (multikernel-adjusted) C parser's locale now, not the substitute *) begin definition diff --git a/proof/crefine/X64/Ipc_C.thy b/proof/crefine/X64/Ipc_C.thy index 1f880c7bb6..021c9ee48a 100644 --- a/proof/crefine/X64/Ipc_C.thy +++ b/proof/crefine/X64/Ipc_C.thy @@ -296,9 +296,9 @@ lemma ccap_relation_reply_helpers: (*FIXME: arch-split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" -lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def -abbreviation "exceptionMessageC \ kernel_all_substitute.fault_messages.[unat MessageID_Exception]" -lemmas exceptionMessageC_def = kernel_all_substitute.fault_messages_def +lemmas syscallMessageC_def = kernel_all_global_addresses.fault_messages_def +abbreviation "exceptionMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Exception]" +lemmas exceptionMessageC_def = kernel_all_global_addresses.fault_messages_def lemma syscallMessage_ccorres: "n < unat n_syscallMessage diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy index 1cd17d4ae9..22e010fa7b 100644 --- a/proof/crefine/X64/Refine_C.thy +++ b/proof/crefine/X64/Refine_C.thy @@ -1083,8 +1083,8 @@ lemma ccorres_underlying_Fault: lemma monadic_rewrite_\: "monadic_rewrite True False \ (exec_C \ c) - (exec_C (kernel_all_global_addresses.\ symbol_table) c)" - using spec_refine [of symbol_table domain] + (exec_C (kernel_all_multi.\ symbol_table cpuNum) c)" + using spec_refine [of symbol_table cpuNum domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn o_def map_option_case monadic_rewrite_def exec_C_def @@ -1101,8 +1101,8 @@ lemma no_fail_getActiveIRQ_C: done lemma kernel_all_subset_kernel: - "global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) - (kernel_global.kernel_call_C symbol_table fp) + "global_automaton (kernel_global.check_active_irq_C symbol_table cpuNum) (do_user_op_C uop) + (kernel_global.kernel_call_C symbol_table cpuNum fp) \ global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C fp)" apply (clarsimp simp: fw_sim_def rel_semi_def global_automaton_def relcomp_unfold in_lift_state_relation_eq) @@ -1152,7 +1152,7 @@ lemma kernel_all_subset_kernel: done theorem true_refinement: - "kernel_global.ADT_C symbol_table x64KSKernelVSpace_C uop + "kernel_global.ADT_C symbol_table x64KSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) @@ -1165,7 +1165,7 @@ theorem true_refinement: (* FIXME: fastpath theorem true_fp_refinement: - "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop + "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C cpuNum uop \ ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) diff --git a/proof/crefine/X64/SyscallArgs_C.thy b/proof/crefine/X64/SyscallArgs_C.thy index b6339080f2..e10a642be7 100644 --- a/proof/crefine/X64/SyscallArgs_C.thy +++ b/proof/crefine/X64/SyscallArgs_C.thy @@ -14,8 +14,8 @@ begin (*FIXME: arch-split: C kernel names hidden by Haskell names *) context kernel_m begin -abbreviation "msgRegistersC \ kernel_all_substitute.msgRegisters" -lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def +abbreviation "msgRegistersC \ kernel_all_global_addresses.msgRegisters" +lemmas msgRegistersC_def = kernel_all_global_addresses.msgRegisters_def end context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy index 5a731c9aed..a59947d2f8 100644 --- a/proof/crefine/X64/Tcb_C.thy +++ b/proof/crefine/X64/Tcb_C.thy @@ -1105,10 +1105,10 @@ lemma Arch_performTransfer_ccorres: done (*FIXME: arch-split: C kernel names hidden by Haskell names *) -abbreviation "frameRegistersC \ kernel_all_substitute.frameRegisters" -lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def -abbreviation "gpRegistersC \ kernel_all_substitute.gpRegisters" -lemmas gpRegistersC_def = kernel_all_substitute.gpRegisters_def +abbreviation "frameRegistersC \ kernel_all_global_addresses.frameRegisters" +lemmas frameRegistersC_def = kernel_all_global_addresses.frameRegisters_def +abbreviation "gpRegistersC \ kernel_all_global_addresses.gpRegisters" +lemmas gpRegistersC_def = kernel_all_global_addresses.gpRegisters_def lemma frame_gp_registers_convs: "length X64_H.frameRegisters = unat n_frameRegisters" diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy index 6807ad14ec..d99e57df61 100644 --- a/proof/crefine/X64/VSpace_C.thy +++ b/proof/crefine/X64/VSpace_C.thy @@ -1353,8 +1353,8 @@ lemma setRegister_ccorres: lemma msgRegisters_ccorres: "n < unat n_msgRegisters \ - register_from_H (X64_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" - apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) + register_from_H (X64_H.msgRegisters ! n) = (index kernel_all_global_addresses.msgRegisters n)" + apply (simp add: kernel_all_global_addresses.msgRegisters_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: if_split) done diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index 5e808e2409..bc1e0eb2dc 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -11,7 +11,7 @@ theory Wellformed_C imports "CLib.CTranslationNICTA" CLevityCatch - "CSpec.Substitute" + "CSpec.Multikernel_C" begin context begin interpretation Arch . (*FIXME: arch-split*) diff --git a/proof/crefine/lib/AutoCorresModifiesProofs.thy b/proof/crefine/lib/AutoCorresModifiesProofs.thy index f54a3a4d97..8e2ad7b749 100644 --- a/proof/crefine/lib/AutoCorresModifiesProofs.thy +++ b/proof/crefine/lib/AutoCorresModifiesProofs.thy @@ -642,7 +642,7 @@ fun define_modifies_group fn_info prog_info f_names (acc as (callee_modifies, re fun new_modifies_rules filename ctxt = let val all_fn_info = Symtab.lookup (AutoCorresFunctionInfo.get (Proof_Context.theory_of ctxt)) filename |> the; val ts_info = FunctionInfo.Phasetab.lookup all_fn_info FunctionInfo.TS |> the; - val prog_info = ProgramInfo.get_prog_info ctxt filename; + val prog_info = ProgramInfo.get_prog_info ctxt "\" filename; (* Assume that the user has already generated and named modifies rules * for previously-translated callees. *) val existing_modifies = From ad6716b279e63c7f26c33ea3c9b19f5ccb5b35d0 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 7 Aug 2025 13:29:28 +0200 Subject: [PATCH 6/7] infoflowC: cpuNum update Adjust references to the C ADT to include the new cpuNum parameter. Signed-off-by: Gerwin Klein --- proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy | 2 +- proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy b/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy index c81cd92068..c5221c5ad6 100644 --- a/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy @@ -319,7 +319,7 @@ lemma obs_cpspace_user_data_relation[ADT_IF_Refine_assms]: end -sublocale kernel_m \ ADT_IF_Refine_1?: ADT_IF_Refine_1 _ _ _ doUserOp_C_if +sublocale kernel_m \ ADT_IF_Refine_1?: ADT_IF_Refine_1 _ _ _ _ doUserOp_C_if proof goal_cases interpret Arch . case 1 show ?case diff --git a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy index d4d0dea8da..2b8c1e398b 100644 --- a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy @@ -241,7 +241,7 @@ lemma obs_cpspace_user_data_relation[ADT_IF_Refine_assms]: end -sublocale kernel_m \ ADT_IF_Refine_1?: ADT_IF_Refine_1 _ _ _ doUserOp_C_if +sublocale kernel_m \ ADT_IF_Refine_1?: ADT_IF_Refine_1 _ _ _ _ doUserOp_C_if proof goal_cases interpret Arch . case 1 show ?case From a0c3e85f3a797015413f50e0cd30adc1fd83d62c Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 7 Aug 2025 14:21:54 +0200 Subject: [PATCH 7/7] asmrefine: update locale and gamma name Update the locale name to kernel_all_substitute0 and Gamma to Gamma0 for the step down to binary verification. Binary verification uses the parsed version of the kernel, not the parameterised version of the kernel since the binary is not parameterised. Signed-off-by: Gerwin Klein --- proof/asmrefine/SEL4GlobalsSwap.thy | 2 +- proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy | 2 +- proof/asmrefine/export/SEL4SimplExport.thy | 2 +- tools/asmrefine/GraphRefine.thy | 2 +- tools/asmrefine/testfiles/global_array_swap.thy | 2 +- tools/asmrefine/testfiles/global_asm_stmt.thy | 2 +- tools/asmrefine/testfiles/inf_loop.thy | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy index 4a5791499d..241a2b3164 100644 --- a/proof/asmrefine/SEL4GlobalsSwap.thy +++ b/proof/asmrefine/SEL4GlobalsSwap.thy @@ -29,7 +29,7 @@ instance ptr :: (c_type)array_outer_packed .. instance tcb_queue_C :: array_outer_packed .. instance region_C :: array_outer_packed .. -locale graph_refine_locale = kernel_all_substitute +locale graph_refine_locale = kernel_all_substitute0 + assumes globals_list_distinct: "globals_list_distinct domain symbol_table globals_list" assumes globals_list_ok: diff --git a/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy b/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy index af65933ef9..20521c414c 100644 --- a/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy +++ b/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy @@ -8,7 +8,7 @@ theory ArchSEL4SimplExport imports "AsmRefine.SimplExport" "CSpec.Substitute" begin -context kernel_all_substitute begin +context kernel_all_substitute0 begin lemma ctzl_body_refines: "simple_simpl_refines \ (Guard ImpossibleSpec \\x___unsigned_long \ 0\ diff --git a/proof/asmrefine/export/SEL4SimplExport.thy b/proof/asmrefine/export/SEL4SimplExport.thy index c5959ce3da..98e1d054ce 100644 --- a/proof/asmrefine/export/SEL4SimplExport.thy +++ b/proof/asmrefine/export/SEL4SimplExport.thy @@ -14,7 +14,7 @@ val csenv = let in fn () => the_csenv end \ -context kernel_all_substitute begin +context kernel_all_substitute0 begin declare ctcb_offset_defs[simp] diff --git a/tools/asmrefine/GraphRefine.thy b/tools/asmrefine/GraphRefine.thy index e0907659fc..d00450bed4 100644 --- a/tools/asmrefine/GraphRefine.thy +++ b/tools/asmrefine/GraphRefine.thy @@ -1733,7 +1733,7 @@ fun inst_graph_tac ctxt = graph_gamma_tac ctxt THEN' inst_graph_node_tac ctxt fun mk_graph_refines (funs : ParseGraph.funs) ctxt s = let val proc = Syntax.read_term ctxt (Long_Name.base_name s ^ "_'proc") - val gamma = Syntax.read_term ctxt "\" + val gamma = Syntax.read_term ctxt "\0" val invs = Syntax.read_term ctxt "simpl_invariant" val _ = case head_of invs of Const _ => () | _ => raise TERM ("mk_graph_refines: requires simpl_invariant constant", []) diff --git a/tools/asmrefine/testfiles/global_array_swap.thy b/tools/asmrefine/testfiles/global_array_swap.thy index 76ce70dd4f..fe74917e26 100644 --- a/tools/asmrefine/testfiles/global_array_swap.thy +++ b/tools/asmrefine/testfiles/global_array_swap.thy @@ -15,7 +15,7 @@ typedecl cghost_state external_file "global_array_swap.c" install_C_file "global_array_swap.c" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] setup \DefineGlobalsList.define_globals_list_i "global_array_swap.c" @{typ globals}\ diff --git a/tools/asmrefine/testfiles/global_asm_stmt.thy b/tools/asmrefine/testfiles/global_asm_stmt.thy index f925f60eeb..a26da4983f 100644 --- a/tools/asmrefine/testfiles/global_asm_stmt.thy +++ b/tools/asmrefine/testfiles/global_asm_stmt.thy @@ -15,7 +15,7 @@ typedecl cghost_state external_file "global_asm_stmt.c" install_C_file "global_asm_stmt.c" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] setup \DefineGlobalsList.define_globals_list_i "global_asm_stmt.c" @{typ globals}\ diff --git a/tools/asmrefine/testfiles/inf_loop.thy b/tools/asmrefine/testfiles/inf_loop.thy index 72b6233f71..e699017ebe 100644 --- a/tools/asmrefine/testfiles/inf_loop.thy +++ b/tools/asmrefine/testfiles/inf_loop.thy @@ -15,7 +15,7 @@ typedecl cghost_state external_file "inf_loop.c" install_C_file "inf_loop.c" - [machinety=machine_state, ghostty=cghost_state] + [machinety=machine_state, ghostty=cghost_state, gamma=\0] setup \DefineGlobalsList.define_globals_list_i "inf_loop.c" @{typ globals}\