From 10b90c823f4a86964e1055b47567d3c4f5b57900 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 6 Mar 2023 12:20:58 +0100 Subject: [PATCH 1/2] Fix declare_reference behavior - Fix "unchecked" text onto_class antiqutation option - Update text-assert-error function to make meta-arguments optional --- .../Concept_OntoReferencing.thy | 4 +-- Isabelle_DOF-Unit-Tests/TestKit.thy | 27 ++++++++++++------- Isabelle_DOF/thys/Isa_DOF.thy | 20 +++++++++----- 3 files changed, 32 insertions(+), 19 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy index 8fc937f..2d2de41 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy @@ -65,9 +65,9 @@ text-assert-error[ae1]\@{C \c1\}\\Undefined inst declare_reference*[c1::C] \ \forward declaration\ -text\@{C \c1\} \ \ \THIS IS A BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \ +text-assert-error\@{C \c1\} \\Instance declared but not defined, try option unchecked\ -text\@{C (unchecked) \c1\} \ \ \THIS SHOULD BE THE CORRECT BEHAVIOUR! \ +text\@{C (unchecked) \c1\} \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \ diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 5f50117..efe7345 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -29,12 +29,15 @@ section\Testing Commands (exec-catch-verify - versions of std commands)\ fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + ((meta_args, xstring_opt:(xstring * Position.T) option), toks_list:Input.source list) : theory -> theory = let val toplvl = Toplevel.theory_toplevel - + val (((oid,pos),cid_pos), doc_attrs) = meta_args + val oid' = if meta_args = ODL_Meta_Args_Parser.empty_meta_args + then "output" + else oid (* as side-effect, generates markup *) fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy); val pos = Input.pos_of toks; @@ -52,7 +55,7 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark (* type file = {path: Path.T, pos: Position.T, content: string} *) val strg = XML.string_of (hd (Latex.output text)) - val file = {path = Path.make [oid ^ "_snippet.tex"], + val file = {path = Path.make [oid' ^ "_snippet.tex"], pos = @{here}, content = Bytes.string strg} @@ -66,10 +69,13 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark (* ... generating the level-attribute syntax *) in - ( Value_Command.Docitem_Parser.create_and_check_docitem + (if meta_args = ODL_Meta_Args_Parser.empty_meta_args + then I + else + Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = false} {define = true} - oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) + oid pos (cid_transform cid_pos) (attr_transform doc_attrs)) + #> (fn thy => (app (check_n_tex_text thy) toks_list; thy)) end; val _ = @@ -117,10 +123,11 @@ fun error_match2 [_, src] msg = error_match src msg val _ = Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro" - (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true} - I I {markdown = true}) - )); + (ODL_Meta_Args_Parser.opt_attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source + >> (Toplevel.theory o + (fn ((meta_args, xstring_opt), source) => + (gen_enriched_document_command3 error_match2 "TTT" {body=true} + I I {markdown = true} ((meta_args, xstring_opt), source))))); fun update_instance_command (args,src) thy = (Monitor_Command_Parser.update_instance_command args thy diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index fb6370c..247b0fb 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1791,10 +1791,9 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi end (* structure Docitem_Parser *) -val empty_meta_args = ((("", Position.none), NONE), []) fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = - thy |> (if meta_args = empty_meta_args + thy |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args then (K thy) else Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = false} {define = true} @@ -2297,9 +2296,9 @@ ML\ structure ML_star_Command = struct -fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = - thy |> (if meta_args = Value_Command.empty_meta_args - then (K thy) +fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) ctxt = + ctxt |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args + then (K ctxt) else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = false} {define = true} oid pos (I cid_pos) (I doc_attrs)) @@ -2661,10 +2660,17 @@ struct val basic_entity = Document_Output.antiquotation_pretty_source : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; -fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = +fun check_and_mark ctxt cid_decl ({strict_checking = strict}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; - val DOF_core.Instance {cid,inline,...} = DOF_core.get_instance_global name thy + val DOF_core.Instance {cid,inline, defined, ...} = DOF_core.get_instance_global name thy + val _ = if not strict + then if defined + then ISA_core.warn ("Instance defined, unchecked option useless") pos + else () + else if defined + then () + else ISA_core.err ("Instance declared but not defined, try option unchecked") pos val _ = if not inline_req then if inline then () else error("referred text-element is macro! (try option display)") else if not inline then () else error("referred text-element is no macro!") From b1a0d5d739e1dcdf679b81c37c943256776776d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 6 Mar 2023 13:10:20 +0100 Subject: [PATCH 2/2] Fix non unchecked text class anti-quotation --- .../CC_ISO15408/PikeOS_study/PikeOS_ST.thy | 6 +- .../CC_v3_1_R5/CC_terminology.thy | 67 +++++++++++-------- Isabelle_DOF/thys/manual/04_RefMan.thy | 9 +-- 3 files changed, 46 insertions(+), 36 deletions(-) diff --git a/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy b/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy index 6c4a153..45eff34 100644 --- a/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy +++ b/Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy @@ -23,14 +23,14 @@ subsection*[pkossttoerefsubsec::st_ref_cls]\TOE Reference\ text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''", toe_version= "(0,3,4)", prod_name="Some ''S3725''"] -\The @{docitem toeDef} is the operating system PikeOS version 3.4 +\The @{docitem (unchecked) toeDef} is the operating system PikeOS version 3.4 running on the microprocessor family x86 hosting different applications. - The @{docitem toeDef} is referenced as PikeOS 3.4 base + The @{docitem (unchecked) toeDef} is referenced as PikeOS 3.4 base product build S3725 for Linux and Windows development host with PikeOS 3.4 Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\ subsection*[pkossttoeovrvwsubsec::st_ref_cls]\ TOE Overview \ -text*[pkosovrw1::toe_ovrw_cls]\The @{docitem \toeDef\ } is a special kind of operating +text*[pkosovrw1::toe_ovrw_cls]\The @{docitem (unchecked) \toeDef\ } is a special kind of operating system, that allows to effectively separate different applications running on the same platform from each other. The TOE can host user applications that can also be operating systems. User applications can also be diff --git a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy index 4cf8c70..06b2892 100644 --- a/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy +++ b/Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_terminology.thy @@ -49,7 +49,7 @@ Definition* [aas_def, tag= "''adverse actions''"] declare_reference*[toeDef] Definition* [assts_def, tag="''assets''"] - \entities that the owner of the @{docitem toeDef} presumably places value upon \ + \entities that the owner of the @{docitem (unchecked) toeDef} presumably places value upon \ Definition* [asgn_def, tag="''assignment''"] \the specification of an identified parameter in a component (of the CC) or requirement.\ @@ -57,7 +57,8 @@ Definition* [asgn_def, tag="''assignment''"] declare_reference*[sfrs_def] Definition* [assrc_def, tag="''assurance''"] - \grounds for confidence that a @{docitem toeDef} meets the @{docitem sfrs_def}\ + \grounds for confidence that a @{docitem (unchecked) toeDef} + meets the @{docitem (unchecked) sfrs_def}\ Definition* [attptl_def, tag="''attack potential''"] \measure of the effort to be expended in attacking a TOE, expressed in terms of @@ -70,7 +71,8 @@ Definition* [authdata_def, tag="''authentication data''"] \information used to verify the claimed identity of a user\ Definition* [authusr_def, tag = "''authorised user''"] -\@{docitem toeDef} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\ +\@{docitem (unchecked) toeDef} user who may, + in accordance with the @{docitem (unchecked) sfrs_def}, perform an operation\ Definition* [bppDef, tag="''Base Protection Profile''"] \Protection Profile used as a basis to build a Protection Profile Configuration\ @@ -105,8 +107,8 @@ Definition* [cfrm_def,tag="''confirm''"] term is only applied to evaluator actions.\ Definition* [cnnctvty_def, tag="''connectivity''"] -\property of the @{docitem toeDef} allowing interaction with IT entities external to the - @{docitem toeDef} +\property of the @{docitem (unchecked) toeDef} allowing interaction with IT entities external to the + @{docitem (unchecked) toeDef} This includes exchange of data by wire or by wireless means, over any distance in any environment or configuration.\ @@ -123,13 +125,16 @@ declare_reference*[stDef] declare_reference*[ppDef] Definition* [dmnst_conf_def, tag="''demonstrable conformance''"] -\relation between an @{docitem stDef} and a @{docitem ppDef}, where the @{docitem stDef} +\relation between an @{docitem (unchecked) stDef} and a @{docitem (unchecked) ppDef}, + where the @{docitem (unchecked) stDef} provides a solution which solves the generic security problem in the PP -The @{docitem ppDef} and the @{docitem stDef} may contain entirely different statements that discuss +The @{docitem (unchecked) ppDef} and the @{docitem (unchecked) stDef} may contain +entirely different statements that discuss different entities, use different concepts etc. Demonstrable conformance is -also suitable for a @{docitem toeDef} type where several similar @{docitem ppDef}s already exist, thus -allowing the ST author to claim conformance to these @{docitem ppDef}s simultaneously, +also suitable for a @{docitem (unchecked) toeDef} type +where several similar @{docitem (unchecked) ppDef}s already exist, thus +allowing the ST author to claim conformance to these @{docitem (unchecked) ppDef}s simultaneously, thereby saving work.\ Definition* [dmstrt_def, tag="''demonstrate''"] @@ -137,9 +142,10 @@ Definition* [dmstrt_def, tag="''demonstrate''"] Definition* [dpndcy, tag="''dependency''"] \relationship between components such that if a requirement based on the depending - component is included in a @{docitem ppDef}, ST or package, a requirement based on - the component that is depended upon must normally also be included in the @{docitem ppDef}, - @{docitem stDef} or package\ + component is included in a @{docitem (unchecked) ppDef}, ST or package, a requirement based on + the component that is depended upon must normally also be included + in the @{docitem (unchecked) ppDef}, + @{docitem (unchecked) stDef} or package\ Definition* [dscrb_def, tag="''describe''"] \provide specific details of an entity\ @@ -154,7 +160,7 @@ Definition* [dtrmn_def, tag="''determine''"] performed which needs to be reviewed\ Definition* [devenv_def, tag="''development environment''"] -\environment in which the @{docitem toeDef} is developed\ +\environment in which the @{docitem (unchecked) toeDef} is developed\ Definition* [elmnt_def, tag="''element''"] \indivisible statement of a security need\ @@ -166,8 +172,8 @@ Definition* [ensr_def, tag="''ensure''"] consequence is not fully certain, on the basis of that action alone.\ Definition* [eval_def, tag="''evaluation''"] -\assessment of a @{docitem ppDef}, an @{docitem stDef} or a @{docitem toeDef}, - against defined criteria.\ +\assessment of a @{docitem (unchecked) ppDef}, an @{docitem (unchecked) stDef} + or a @{docitem (unchecked) toeDef}, against defined criteria.\ Definition* [eal_def, tag= "''evaluation assurance level''"] \set of assurance requirements drawn from CC Part 3, representing a point on the @@ -292,36 +298,37 @@ declare_reference*[tsf_def] Definition* [prv_def, tag="''prove''"] \show correspondence by formal analysis in its mathematical sense It is completely rigorous in all ways. Typically, “prove” is used when there is - a desire to show correspondence between two @{docitem tsf_def} representations at a high - level of rigour.\ + a desire to show correspondence between two @{docitem (unchecked) tsf_def} + representations at a high level of rigour.\ Definition* [ref_def, tag="''refinement''"] \addition of details to a component\ Definition* [role_def, tag="''role''"] \predefined set of rules establishing the allowed interactions between - a user and the @{docitem toeDef}\ + a user and the @{docitem (unchecked) toeDef}\ declare_reference*[sfp_def] Definition* [scrt_def, tag="''secret''"] \information that must be known only to authorised users and/or the - @{docitem tsf_def} in order to enforce a specific @{docitem sfp_def}\ + @{docitem (unchecked) tsf_def} in order to enforce a specific @{docitem (unchecked) sfp_def}\ declare_reference*[sfr_def] Definition* [sec_stDef, tag="''secure state''"] -\state in which the @{docitem tsf_def} data are consistent and the @{docitem tsf_def} - continues correct enforcement of the @{docitem sfr_def}s\ +\state in which the @{docitem (unchecked) tsf_def} data are consistent + and the @{docitem (unchecked) tsf_def} + continues correct enforcement of the @{docitem (unchecked) sfr_def}s\ Definition* [sec_att_def, tag="''security attribute''"] \property of subjects, users (including external IT products), objects, - information, sessions and/or resources that is used in defining the @{docitem sfr_def}s - and whose values are used in enforcing the @{docitem sfr_def}s\ + information, sessions and/or resources that is used in defining the @{docitem (unchecked) sfr_def}s + and whose values are used in enforcing the @{docitem (unchecked) sfr_def}s\ Definition* [sec_def, tag="''security''"] \function policy set of rules describing specific security behaviour enforced - by the @{docitem tsf_def} and expressible as a set of @{docitem sfr_def}s\ + by the @{docitem (unchecked) tsf_def} and expressible as a set of @{docitem (unchecked) sfr_def}s\ Definition* [sec_obj_def, tag="''security objective''"] \statement of an intent to counter identified threats and/or satisfy identified @@ -340,10 +347,11 @@ Definition* [sr_def, tag="''security requirement''", short_tag="Some(''SR'')"] \requirement, stated in a standardised language, which is meant to contribute to achieving the security objectives for a TOE\ (*<*) -text \@{docitem toeDef}\ +text \@{docitem (unchecked) toeDef}\ (*>*) Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"] -\implementation-dependent statement of security needs for a specific identified @{docitem toeDef}\ +\implementation-dependent statement of security needs for a specific identified + @{docitem (unchecked) toeDef}\ Definition* [slct_def, tag="''selection''"] \specification of one or more items from a list in a component\ @@ -383,7 +391,7 @@ Definition* [toe_res_def, tag="''TOE resource''"] Definition* [toe_sf_def, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"] \combined functionality of all hardware, software, and firmware of a TOE that must be relied upon - for the correct enforcement of the @{docitem sfr_def}s\ + for the correct enforcement of the @{docitem (unchecked) sfr_def}s\ Definition* [tr_vrb_def, tag="''trace, verb''"] \perform an informal correspondence analysis between two entities with only a @@ -434,13 +442,14 @@ effort is required of the evaluator.\ Definition* [dev_def, tag="''Developer''"] \who respond to actual or perceived consumer security requirements in - constructing a @{docitem toeDef}, reference this CC\_Part\_3 + constructing a @{docitem (unchecked) toeDef}, reference this CC\_Part\_3 when interpreting statements of assurance requirements and determining assurance approaches of @{docitem toe}s.\ Definition*[evalu_def, tag="'' Evaluator''"] \who use the assurance requirements defined in CC\_Part\_3 as mandatory statement of evaluation criteria when determining the assurance - of @{docitem toeDef}s and when evaluating @{docitem ppDef}s and @{docitem stDef}s.\ + of @{docitem (unchecked) toeDef}s and when evaluating @{docitem ppDef}s + and @{docitem (unchecked) stDef}s.\ end diff --git a/Isabelle_DOF/thys/manual/04_RefMan.thy b/Isabelle_DOF/thys/manual/04_RefMan.thy index d8d4fb6..b6e1e62 100644 --- a/Isabelle_DOF/thys/manual/04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/04_RefMan.thy @@ -1011,10 +1011,11 @@ text\ declare[[invariants_checking_with_tactics = true]]\} There are still some limitations with this high-level syntax. For now, the high-level syntax does not support the checking of - specific monitor behaviors (see \<^technical>\sec:monitors\). + specific monitor behaviors (see @{technical (unchecked) "sec:monitors"}). For example, one would like to delay a final error message till the closing of a monitor. - For this use-case you can use low-level class invariants (see \<^technical>\sec:low_level_inv\). + For this use-case you can use low-level class invariants + (see @{technical (unchecked) "sec:low_level_inv"}). \ subsection*["sec:monitors"::technical]\ODL Monitors\ @@ -1086,14 +1087,14 @@ text\ sections. For now, the high-level syntax of invariants does not support the checking of specific monitor behaviors like the one just described and you must use - the low-level class invariants (see \<^technical>\sec:low_level_inv\). + the low-level class invariants (see @{technical (unchecked) "sec:low_level_inv"}). Low-level invariants checking can be set up to be triggered when opening a monitor, when closing a monitor, or both by using the \<^ML>\DOF_core.add_opening_ml_invariant\, \<^ML>\DOF_core.add_closing_ml_invariant\, or \<^ML>\DOF_core.add_ml_invariant\ commands respectively, to add the invariants to the theory context - (See \<^technical>\sec:low_level_inv\ for an example). + (See @{technical (unchecked) "sec:low_level_inv"} for an example). \