Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF

Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy

@@ -23,14 +23,14 @@ subsection*[pkossttoerefsubsec::st_ref_cls]\<open>TOE Reference\<close>
 
 text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
       toe_version= "(0,3,4)", prod_name="Some ''S3725''"]
-\<open>The @{docitem toeDef} is the operating system PikeOS version 3.4 
+\<open>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.\<close>
 
 subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
-text*[pkosovrw1::toe_ovrw_cls]\<open>The @{docitem \<open>toeDef\<close> } is a special kind of operating 
+text*[pkosovrw1::toe_ovrw_cls]\<open>The @{docitem (unchecked) \<open>toeDef\<close> } 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

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''"]
- \<open>entities that the owner of the @{docitem toeDef} presumably places value upon \<close>
+ \<open>entities that the owner of the @{docitem (unchecked) toeDef} presumably places value upon \<close>
 
 Definition* [asgn_def, tag="''assignment''"]
 \<open>the specification of an identified parameter in a component (of the CC) or requirement.\<close>
@@ -57,7 +57,8 @@ Definition* [asgn_def, tag="''assignment''"]
 declare_reference*[sfrs_def]
 
 Definition* [assrc_def, tag="''assurance''"]
-  \<open>grounds for confidence that a @{docitem toeDef} meets the @{docitem sfrs_def}\<close>
+  \<open>grounds for confidence that a @{docitem (unchecked) toeDef}
+   meets the @{docitem (unchecked) sfrs_def}\<close>
 
 Definition* [attptl_def, tag="''attack potential''"] 
   \<open>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''"]
   \<open>information used to verify the claimed identity of a user\<close>
 
 Definition* [authusr_def, tag = "''authorised user''"] 
-\<open>@{docitem toeDef} user who may, in accordance with the @{docitem sfrs_def}, perform an operation\<close>
+\<open>@{docitem (unchecked) toeDef} user who may,
+ in accordance with the @{docitem (unchecked) sfrs_def}, perform an operation\<close>
 
 Definition* [bppDef, tag="''Base Protection Profile''"] 
 \<open>Protection Profile used as a basis to build a Protection Profile Configuration\<close>
@@ -105,8 +107,8 @@ Definition* [cfrm_def,tag="''confirm''"]
  term is only applied to evaluator actions.\<close>
 
 Definition* [cnnctvty_def, tag="''connectivity''"]
-\<open>property of the @{docitem toeDef} allowing interaction with IT entities external to the 
+\<open>property of the @{docitem (unchecked) toeDef} allowing interaction with IT entities external to the 
- @{docitem toeDef}
+ @{docitem (unchecked) toeDef}
 
  This includes exchange of data by wire or by wireless means, over any
  distance in any environment or configuration.\<close>
@@ -123,13 +125,16 @@ declare_reference*[stDef]
 declare_reference*[ppDef]
 
 Definition* [dmnst_conf_def, tag="''demonstrable conformance''"] 
-\<open>relation between an @{docitem stDef} and a @{docitem ppDef}, where the @{docitem stDef} 
+\<open>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
+also suitable for a @{docitem (unchecked) toeDef} type
-allowing the ST author to claim conformance to these @{docitem ppDef}s simultaneously,
+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.\<close>
 
 Definition* [dmstrt_def, tag="''demonstrate''"] 
@@ -137,9 +142,10 @@ Definition* [dmstrt_def, tag="''demonstrate''"]
 
 Definition* [dpndcy, tag="''dependency''"] 
 \<open>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 
+ 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 ppDef}, 
+ the component that is depended upon must normally also be included
- @{docitem stDef} or package\<close>
+ in the @{docitem (unchecked) ppDef}, 
+ @{docitem (unchecked) stDef} or package\<close>
 
 Definition* [dscrb_def, tag="''describe''"] 
 \<open>provide specific details of an entity\<close>
@@ -154,7 +160,7 @@ Definition* [dtrmn_def, tag="''determine''"]
  performed which needs to be reviewed\<close>
 
 Definition* [devenv_def, tag="''development environment''"] 
-\<open>environment in which the @{docitem toeDef} is developed\<close>
+\<open>environment in which the @{docitem (unchecked) toeDef} is developed\<close>
 
 Definition* [elmnt_def, tag="''element''"] 
 \<open>indivisible statement of a security need\<close>
@@ -166,8 +172,8 @@ Definition* [ensr_def, tag="''ensure''"]
  consequence is not fully certain, on the basis of that action alone.\<close>
 
 Definition* [eval_def, tag="''evaluation''"] 
-\<open>assessment of a @{docitem ppDef}, an @{docitem stDef} or a @{docitem toeDef}, 
+\<open>assessment of a @{docitem (unchecked) ppDef}, an @{docitem (unchecked) stDef}
- against defined criteria.\<close>
+ or a @{docitem (unchecked) toeDef}, against defined criteria.\<close>
 
 Definition* [eal_def, tag= "''evaluation assurance level''"] 
 \<open>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''"] 
 \<open>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
+ a desire to show correspondence between two @{docitem (unchecked) tsf_def}
- level of rigour.\<close>
+ representations at a high level of rigour.\<close>
 
 Definition* [ref_def, tag="''refinement''"] 
 \<open>addition of details to a component\<close>
 
 Definition* [role_def, tag="''role''"] 
 \<open>predefined set of rules establishing the allowed interactions between
- a user and the @{docitem toeDef}\<close>
+ a user and the @{docitem (unchecked) toeDef}\<close>
 
 declare_reference*[sfp_def]
 
 Definition* [scrt_def, tag="''secret''"]
 \<open>information that must be known only to authorised users and/or the
- @{docitem tsf_def} in order to enforce a specific @{docitem sfp_def}\<close>
+ @{docitem (unchecked) tsf_def} in order to enforce a specific @{docitem (unchecked) sfp_def}\<close>
 
 declare_reference*[sfr_def]
 
 Definition* [sec_stDef, tag="''secure state''"] 
-\<open>state in which the @{docitem tsf_def} data are consistent and the  @{docitem tsf_def} 
+\<open>state in which the @{docitem (unchecked) tsf_def} data are consistent
- continues correct enforcement of the  @{docitem sfr_def}s\<close>
+  and the  @{docitem (unchecked) tsf_def} 
+ continues correct enforcement of the  @{docitem (unchecked) sfr_def}s\<close>
 
 Definition* [sec_att_def, tag="''security attribute''"] 
 \<open>property of subjects, users (including external IT products), objects, 
- information, sessions and/or resources that is used in defining 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 sfr_def}s\<close>
+ and whose values are used in enforcing the @{docitem (unchecked) sfr_def}s\<close>
 
 Definition* [sec_def, tag="''security''"]
 \<open>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\<close>
+ by the @{docitem (unchecked) tsf_def} and expressible as a set of @{docitem (unchecked) sfr_def}s\<close>
 
 Definition* [sec_obj_def, tag="''security objective''"] 
 \<open>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'')"]
 \<open>requirement, stated in a standardised language, which is meant to contribute 
  to achieving the security objectives for a TOE\<close>
 (*<*)
-text \<open>@{docitem toeDef}\<close>
+text \<open>@{docitem  (unchecked) toeDef}\<close>
 (*>*)
 Definition* [st, tag="''Security Target''", short_tag="Some(''ST'')"]
-\<open>implementation-dependent statement of security needs for a specific identified @{docitem toeDef}\<close>
+\<open>implementation-dependent statement of security needs for a specific identified
+ @{docitem (unchecked) toeDef}\<close>
 
 Definition* [slct_def, tag="''selection''"] 
 \<open>specification of one or more items from a list in a component\<close>
@@ -383,7 +391,7 @@ Definition* [toe_res_def, tag="''TOE resource''"]
 
 Definition* [toe_sf_def, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"] 
 \<open>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\<close>
+ for the correct enforcement of the @{docitem  (unchecked) sfr_def}s\<close>
 
 Definition* [tr_vrb_def, tag="''trace, verb''"] 
 \<open>perform an informal correspondence analysis between two entities with only a 
@@ -434,13 +442,14 @@ effort is required of the evaluator.\<close>
 
 Definition* [dev_def, tag="''Developer''"]
 \<open>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.\<close>
 
 Definition*[evalu_def, tag="'' Evaluator''"]
 \<open>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.\<close>
+ of @{docitem  (unchecked) toeDef}s and when evaluating @{docitem ppDef}s
+ and @{docitem  (unchecked) stDef}s.\<close>
 
 end

Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy

@@ -64,9 +64,9 @@ text-assert-error[ae1]\<open>@{C \<open>c1\<close>}\<close>\<open>Undefined inst
 
 declare_reference*[c1::C]     \<comment> \<open>forward declaration\<close>
 
-text\<open>@{C \<open>c1\<close>} \<close>              \<comment> \<open>THIS IS A  BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \<close>
+text-assert-error\<open>@{C \<open>c1\<close>} \<close>\<open>Instance declared but not defined, try option unchecked\<close>
 
-text\<open>@{C (unchecked) \<open>c1\<close>} \<close>  \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
+text\<open>@{C (unchecked) \<open>c1\<close>} \<close>
 
 text*[a1::A, level="Some 0", x = 3]\<open>... phasellus amet id massa nunc, ...\<close>
 text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>

Isabelle_DOF-Unit-Tests/TestKit.thy

@@ -29,12 +29,15 @@ section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<c
 ML\<open> 
 
 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)
+                              oid pos (cid_transform cid_pos) (attr_transform doc_attrs))
-        #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) 
+        #> (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 
+    (ODL_Meta_Args_Parser.opt_attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
-      >> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true}
+      >> (Toplevel.theory o
-                                                            I I {markdown = true}) 
+          (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

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\<open>
 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 = 
+fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) ctxt = 
-         thy |> (if meta_args = Value_Command.empty_meta_args
+         ctxt |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args
-                 then (K thy)                               
+                 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!")

Isabelle_DOF/thys/manual/04_RefMan.thy

@@ -1011,10 +1011,11 @@ text\<open>
   declare[[invariants_checking_with_tactics = true]]\<close>}
   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>\<open>sec:monitors\<close>).
+  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>\<open>sec:low_level_inv\<close>).
+  For this use-case you can use low-level class invariants
+  (see @{technical (unchecked) "sec:low_level_inv"}).
 \<close>
 
 subsection*["sec:monitors"::technical]\<open>ODL Monitors\<close>
@@ -1086,14 +1087,14 @@ text\<open>
   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>\<open>sec:low_level_inv\<close>).
+  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>\<open>DOF_core.add_opening_ml_invariant\<close>,
   \<^ML>\<open>DOF_core.add_closing_ml_invariant\<close>, or \<^ML>\<open>DOF_core.add_ml_invariant\<close> commands
   respectively, to add the invariants to the theory context
-  (See \<^technical>\<open>sec:low_level_inv\<close> for an example).
+  (See @{technical (unchecked) "sec:low_level_inv"} for an example).
 \<close>