Update requirements based on the PR review

REQUIREMENTS.sdoc

@@ -11,6 +11,13 @@ OPTIONS:
 
 [FREETEXT]
 This document contains all OpenSUT requirements, and was created with the help of `StrictDocs <https://strictdoc.readthedocs.io/en/stable/>`_. For text formatting, the reStructuredText markup syntax is supported, see `the RST cheatsheet <https://bashtage.github.io/sphinx-material/rst-cheatsheet/rst-cheatsheet.html>`_.
+
+If you are new to requirement writing, we recommend reading first the *21 Top Engineering Tips
+for writing an exceptionally clear requirements document* from QRA (available as `PDF here <https://github.com/GaloisInc/VERSE-OpenSUT/blob/main/docs/QRA_Clear_Requirements.pdf>`_)
+
+The OpenSUT requirements are split into different sections and subsections. Each requirement has its section number (e.g. *4.1.1.2 Actuation Logic*) and its Unique Identifier (UID). The section number is used only in this document, the UID guaranteed to be globally unique. On top of UID, we also use StrictDocs' `MID <https://strictdoc.readthedocs.io/en/stable/strictdoc_01_user_guide.html#machine-identifiers-mid>`_. For requirement tracing and coverage measurement, we use primarily the UID.
+
+Requirements that use the word *shall* are binding and must be satisfied, while requirements using the word *should* are non-binding, and can be considered optional or nice-to-have. A *rationale* is provided when appropriate for a given requirement.
 [/FREETEXT]
 
 [SECTION]
@@ -61,7 +68,7 @@ MID: 4361d44f1b65433e88092bfbb0bc0d41
 UID: TA2-REQ-45
 TITLE: Task TA2.1.1.C
 STATEMENT: >>>
-Develop CN specifications for components with rich code-level specifications.
+Develop VERSE Toolchain specifications for components with rich code-level specifications.
 <<<
 
 [/SECTION]
@@ -114,7 +121,7 @@ Support two Phase 1 continuous integration events.
 [SECTION]
 MID: 0860f7ea4f254939bec1bfb31c35e2bb
 UID: SECTION-OR-Code-requirements
-TITLE: OpenSUT Code requirements
+TITLE: OpenSUT Code Requirements
 
 [FREETEXT]
 In this section we list requirements about the overall OpenSUT code, its structure, coverage and format.
@@ -372,8 +379,12 @@ MPS shall run Periodic continual self-test of safety signal path (e.g., overlapp
 
 [SECTION]
 MID: 3356cf51d10a4f4b944fa2b0be4a7d57
-UID: SECTION-OR-MPS-Verification-Requirements
-TITLE: MPS Verification Requirements
+UID: SECTION-OR-MPS-Testing-Requirements
+TITLE: MPS Testing Requirements
+
+[FREETEXT]
+Traditionally, this section would be called *Verification Requirements*, but in the context of VERSE *verification* means *providing a formal proof*, thus *testing* is a more appropriate label.
+[/FREETEXT]
 
 [REQUIREMENT]
 MID: a68b1797067440aeb4161c281c0b257f
@@ -431,20 +442,20 @@ MPS shall demonstrate Independence between periodic self-test functions and trip
 
 [SECTION]
 MID: 377a09e7f8fa4c399ea4ae3a9f7c22fd
-UID: SECTION-OR-CN-Requirements
-TITLE: CN Requirements
+UID: SECTION-OR-VERSE-Toolchain-Requirements
+TITLE: VERSE Toolchain Requirements
 
 [FREETEXT]
-CN specific requirements, driven by the TA2 needs. In some cases, we mention a more generic *TA1 tooling*, but CN is the main and likely the only tool.
+VERSE Toolchain specific requirements, driven by the TA2 needs.
 [/FREETEXT]
 
 [SECTION]
 MID: 1bc49bad6c4f481bad154377f5f7f44e
 UID: SECTION-OR-Robustness-requirements
-TITLE: CN Usability requirements
+TITLE: VERSE Toolchain Usability Requirements
 
 [FREETEXT]
-Requirements related to the user experience with CN and TA1 tooling in general.
+Requirements related to the user experience with VERSE Toolchain in general.
 [/FREETEXT]
 
 [REQUIREMENT]
@@ -453,10 +464,10 @@ UID: TA2-REQ-1
 STATUS: Active
 TITLE: No crashing
 STATEMENT: >>>
-CN shall not crash on arbitrary input. Instead, an error message shall be produced.
+VERSE Toolchain shall not crash on arbitrary input. Instead, an error message shall be produced.
 <<<
 RATIONALE: >>>
-Even if a specification is incorrect, or the input file is not a valid C code, CN should gracefully exit.
+Even if a specification is incorrect, or the input file is not a valid C code, VERSE Toolchain should gracefully exit.
 <<<
 
 [REQUIREMENT]
@@ -465,10 +476,10 @@ UID: TA2-REQ-2
 STATUS: Active
 TITLE: Special delimiters
 STATEMENT: >>>
-CN should support multiple special delimiters, such as `//@` or `/*@` or `/**@`. Which special delimiter should be used can be either configurable, or CN should support all of them at the same time (see TA2-REQ-15).
+VERSE Toolchain should support multiple special delimiters, such as `//@` or `/*@` or `/**@`. Which special delimiter should be used can be either configurable, or VERSE Toolchain should support all of them at the same time (see TA2-REQ-15).
 <<<
 RATIONALE: >>>
-In some codebases, CN specs need to co-exist with existing specifications (such as Frama-C ACSL), such that adding CN specs does not break the existing proofs.
+In some codebases, VERSE Toolchain specs need to co-exist with existing specifications (such as Frama-C ACSL), such that adding VERSE Toolchain specs does not break the existing proofs.
 <<<
 RELATIONS:
 - TYPE: Parent
@@ -479,7 +490,7 @@ MID: d1c4883fe05149ab94ca644e5e21eb98
 UID: TA2-REQ-7
 TITLE: Multiple specification languages
 STATEMENT: >>>
-CN shall run on codebases with multiple specification languages, such as Frama-C, SAW, and Cryptol.
+VERSE Toolchain shall run on codebases with multiple specification languages, such as Frama-C, SAW, and Cryptol.
 <<<
 RATIONALE: >>>
 High assurance code might contain multiple different spec languages. For VERSE program, we expect that only Frama-C ACSL specifications will exist directly in the C source code. Other specs, such as SAW and Cryptol, do not change the C code directly.
@@ -490,10 +501,10 @@ MID: ed253cc2440040d8ae16b40d787f8b4f
 UID: TA2-REQ-8
 TITLE: Continuity of existing proofs
 STATEMENT: >>>
-Adding CN specs to a codebase shall not break existing proofs about such codebase.
+Adding VERSE Toolchain specs to a codebase shall not break existing proofs about such codebase.
 <<<
 RATIONALE: >>>
-For example, adding CN specs into an existing high assurance codebase shall not break the existing Frama-C proofs
+For example, adding VERSE Toolchain specs into an existing high assurance codebase shall not break the existing Frama-C proofs
 <<<
 RELATIONS:
 - TYPE: Parent
@@ -502,55 +513,66 @@ RELATIONS:
 [REQUIREMENT]
 MID: 08aa1eec7c5a4f218d9ceeef73c1b938
 UID: TA2-REQ-15
-TITLE: Project specific CN configuration
+TITLE: Project specific VERSE Toolchain configuration
 STATEMENT: >>>
-CN shall support project specific configuration, in the form of a configuration file that will adjust how CN behaves.
+VERSE Toolchain shall support project specific configuration, in the form of a configuration file that will adjust how VERSE Toolchain behaves.
 <<<
 RATIONALE: >>>
 This is a top level requirement, further specified in the child requirements.
 <<<
 
+[REQUIREMENT]
+MID: 4c8d98c9b64c4cfe83ecbd73d785fc27
+UID: TA2-REQ-52
+TITLE: Code similarity
+STATEMENT: >>>
+The code checked by VERSE Toolchain and the code compiled and deployed on the OpenSUT shall be identical.
+<<<
+RATIONALE: >>>
+If the code that can be checked by VERSE Toolchain is substantially different from the code that is compiled and deployed, errors in the production code might not be captures, leading to presence of bugs and vulnerabilities.
+<<<
+
 [/SECTION]
 
 [SECTION]
 MID: 47b21bb670624559b181b882007035d6
 UID: SECTION-OR-Functional-Requirements
-TITLE: CN Functional Requirements
+TITLE: VERSE Toolchain Functional Requirements
 
 [FREETEXT]
-This section lists requirements on the functionality of CN, and the features it provides.
+This section lists requirements on the functionality of VERSE Toolchain, and the features it provides.
 [/FREETEXT]
 
 [REQUIREMENT]
 MID: d7f93f2b664e49778727afb3656b2725
 UID: TA2-REQ-3
 TITLE: Versioned releases
 STATEMENT: >>>
-CN shall provide versioned releases, such that running CN with `-V` flag shall print out the version of the tool.
+VERSE Toolchain shall provide versioned releases, such that running VERSE Toolchain with `-V` flag shall print out the version of the tool.
 <<<
 
 [REQUIREMENT]
 MID: 2a0d10e543ec4f279e2f56d092e7e65e
 UID: TA2-REQ-5
 TITLE: Variadic functions
 STATEMENT: >>>
-CN shall support reasoning about variadic functions, such as `printf()`.
+VERSE Toolchain shall support reasoning about variadic functions, such as `printf()`.
 <<<
 
 [REQUIREMENT]
 MID: 967a8c569dca4e8492d371b030be0f13
 UID: TA2-REQ-4
 TITLE: Packaged releases
 STATEMENT: >>>
-CN shall provide packaged releases using industry standard mechanisms, such as docker, or debian packages.
+VERSE Toolchain shall provide packaged releases using industry standard mechanisms, such as docker, or debian packages.
 <<<
 
 [REQUIREMENT]
 MID: 2db8fe5f16b247eea953e3c944687e33
 UID: TA2-REQ-6
 TITLE: C Unions
 STATEMENT: >>>
-CN shall support reasoning about C union types.
+VERSE Toolchain shall support reasoning about C union types.
 <<<
 RATIONALE: >>>
 For example the MPS code relies heavily on unions, and such code needs to be supported.
@@ -561,12 +583,10 @@ MID: 38dbcc6d1cc042749c550ff7394513db
 UID: TA2-REQ-9
 TITLE: Nested types
 STATEMENT: >>>
-CN shall support reasoning about structs composed of other structs.
+VERSE Toolchain shall support reasoning about structs composed of other structs.
 <<<
 RATIONALE: >>>
-Writing *implicitly* implies that CN should enforce these things without additional CN specifications, in the same way that it implicitly enforces defined behavior. Thus the user does not have to write any additional specs.
-
-For example:
+For example VERSE Toolchain shall be able to reason about the following struct and prove that there is no undefined behavior and that any user defined specification holds for such a struct:
 
 .. code-block:: c
 
@@ -575,34 +595,41 @@ For example:
         T2 *S2;
         T3 S3[];
     }
+<<<
 
-CN should implicitly enforce that:
+[REQUIREMENT]
+MID: 9dd60eb2b6b74db2ae06ff42ad0505e2
+UID: TA2-REQ-53
+TITLE: User defined type invariants
+STATEMENT: >>>
+VERSE Toolchain should support checking user defined type and data structure invariants. VERSE Toolchain should allow users to annotate types and data structures with invariants, such that the invariant is preserved at every instance of that type.
+<<<
+RATIONALE: >>>
+For example, the user wishes to prove that a pointer of particular type is never NULL. While NULL pointers are allowed under Cerberus C semantics, *dereferencing* a NULL pointer is an undefined behavior. Thus, a user defined invariant that a pointer shall never be NULL should be checkable by VERSE Toolchain.
 
-1) invariants about struct S1 of type T1 are valid
-2) pointer S2 of type T2 is not null, and points to an initialized memory
-3) invariants about type T3 are valid for each element of array S3, and this is true for min and max size of S3, with min=0 and max some sensible default value (uint32_MAX?)
+Or given an array `T3 S3[];` the user wishes to prove that invariants about type T3 are valid for each element of array S3, and this is true for min and max size of S3, with min=0 and max some sensible default value (uint32_MAX?).
 <<<
 
 [REQUIREMENT]
 MID: 0edc5a82bfa34fe79f46c23eb9af9986
 UID: TA2-REQ-10
 TITLE: Specs in header of source file allowed
 STATEMENT: >>>
-CN shall allow the user to write CN specifications in either header (function declaration) or source file (function definition). If CN specs are provided at both function declaration and function definition, CN shall raise an error.
+VERSE Toolchain shall allow the user to write VERSE Toolchain specifications in either header (function declaration) or source file (function definition). If VERSE Toolchain specs are provided at both function declaration and function definition, VERSE Toolchain shall raise an error.
 <<<
 RATIONALE: >>>
-In some cases, writing specs in the header files is more ergonomic. In other cases, there might be no header files. The user shall have a choice that is the most suitable for a particular codebase. If accidentally the user writes multiple CN specs for the same function (in the header and in the source file), CN needs to throw an error an notify the user, as resolving which specs are valid is a complex problem.
+In some cases, writing specs in the header files is more ergonomic. In other cases, there might be no header files. The user shall have a choice that is the most suitable for a particular codebase. If accidentally the user writes multiple VERSE Toolchain specs for the same function (in the header and in the source file), VERSE Toolchain needs to throw an error an notify the user, as resolving which specs are valid is a complex problem.
 <<<
 
 [REQUIREMENT]
 MID: ff63483e56744e10a10d5a9467f81231
 UID: TA2-REQ-12
 TITLE: Explicit assertion checking
 STATEMENT: >>>
-CN shall have a configurable option to either ignore inline `assert()` statements, or to statically check them.
+VERSE Toolchain shall have a configurable option to either ignore inline `assert()` statements, or to statically check them.
 <<<
 RATIONALE: >>>
-In some codebases, assertions are used only for selective runtime testing, so static checking might produce findings that are not interesting for the developers. The assertions are removed in the production code. Hence having the configurable option for CN is important.
+In some codebases, assertions are used only for selective runtime testing, so static checking might produce findings that are not interesting for the developers. The assertions are removed in the production code. Hence having the configurable option for VERSE Toolchain is important.
 <<<
 RELATIONS:
 - TYPE: Parent
@@ -613,7 +640,7 @@ MID: 239719df3d0746c6be9363179d9c9fa1
 UID: TA2-REQ-13
 TITLE: Well defined default behavior
 STATEMENT: >>>
-If a function is not annotated with any CN specifications, CN shall explicitly state what are the default (implicit) `require`, `ensure` and `modify` clauses.
+If a function is not annotated with any VERSE Toolchain specifications, VERSE Toolchain shall explicitly state what are the default (implicit) `require`, `ensure` and `modify` clauses.
 <<<
 RATIONALE: >>>
 It needs to be stated whether by default each function requires and ensures nothing, or if there are some implicit assumptions, important for compositional reasoning. Same for modification - a sensible default behavior could be that a function without specs is assumed to modify everything. However, in that case compositional reasoning is not really possible, so having a configurable option here might be preferred.
@@ -629,7 +656,7 @@ MID: d0a1826596ee41fcba1230498e92b242
 UID: TA2-REQ-14
 TITLE: Annotation of pure functions
 STATEMENT: >>>
-CN shall have a configurable option to either assume that all functions are `pure` by default, or to require an explicit `pure` annotation.
+VERSE Toolchain shall have a configurable option to either assume that all functions are `pure` by default, or to require an explicit `pure` annotation.
 <<<
 RATIONALE: >>>
 Pure functions are side-effects free, and don't have any persistent static variables (see https://en.wikipedia.org/wiki/Pure_function). In some cases, explicitly stating which functions should be `pure` is easier, while in other codebases, it is reasonable to assume that the functions are `pure` by default. This should be configurable.
@@ -638,37 +665,51 @@ RELATIONS:
 - TYPE: Parent
   VALUE: TA2-REQ-15
 
+[REQUIREMENT]
+MID: 99d58897b02743eb9c35b925b1a5bcfc
+UID: TA2-REQ-51
+TITLE: Check for undefined behavior
+STATEMENT: >>>
+VERSE Toolchain shall check C code for undefined behavior as defined in Cerberus semantics, and raise an error when undefined behavior is found.
+<<<
+RATIONALE: >>>
+This is a base level functionality of VERSE Toolchain, as code with undefined behavior often leads to errors and unintended results.
+<<<
+RELATIONS:
+- TYPE: Parent
+  VALUE: TA2-REQ-16
+
 [/SECTION]
 
 [SECTION]
 MID: 8b79d2b352df4ac2af8e9bdbed7bd64c
 UID: SECTION-OR-Documentation-requirements
-TITLE: CN Documentation requirements
+TITLE: VERSE Toolchain Documentation Requirements
 
 [FREETEXT]
-Documentation of CN, including manuals, tutorials, quick-start guides, code and document generation, and hints and error messages.
+Documentation of VERSE Toolchain, including manuals, tutorials, quick-start guides, code and document generation, and hints and error messages.
 [/FREETEXT]
 
 [REQUIREMENT]
 MID: 82e79a99aa9c4c9ab74c1bbe4535dbda
 UID: TA2-REQ-11
 TITLE: Generating code documentation with specs
 STATEMENT: >>>
-TA1 tools shall generate source code documentation that includes CN specification with CN syntax highlighted.
+TA1 tools shall generate source code documentation that includes VERSE Toolchain specification with VERSE Toolchain syntax highlighted.
 <<<
 RATIONALE: >>>
-Doxygen-like documentation with CN specs included is ideal. It is important that the specs are not treated like comments, but are lifted and highlighted in the generated documents.
+Doxygen-like documentation with VERSE Toolchain specs included is ideal. It is important that the specs are not treated like comments, but are lifted and highlighted in the generated documents.
 <<<
 
 [REQUIREMENT]
 MID: 39e7d83efe9f4073b69ff53f2be42c68
 UID: TA2-REQ-50
 TITLE: Code coverage measurement
 STATEMENT: >>>
-CN should provide means of measuring code coverage, and specifically reporting:
+VERSE Toolchain should provide means of measuring code coverage, and specifically reporting:
 
 1) percentage or LOC of code/functions that have *any* specs
-2) *any* code excluded from CN checking (maybe hiding behind `#ifdef` or some other directive, excluding the code from being examined)
+2) *any* code excluded from VERSE Toolchain checking (maybe hiding behind `#ifdef` or some other directive, excluding the code from being examined)
 3) coverage based on types/classes of specifications (see the different classes we mentioned in the proposal)
 <<<
 RATIONALE: >>>