chain of custody for formally-verified software

Relating disparate sources of knowledge in science involves:

• Formally-verified Mathematical Physics (e.g., in Lean). Purpose: verify the mathematical model is consistent with specified axioms.
• Formally-verified software; see https://physicsderivationgraph.blogspot.com/2022/10/tla-comparison.html for a list.
• Performant parallelized software (e.g., MPI + OpenMP + Fortran or C/C++) for High Performance Computing (HPC).
• Peer-reviewed journal articles, e.g., arxiv; rendered using Latex. [Of the four, this has historically been closest to the focus of the Physics Derivation Graph.]

Each of these content sources are independent and involve expressing a mathematical model in different ways. 

While kernels of mathematical models can be implemented in formally-verified software, a lot of scientific computing uses High Performance Computing (HPC). In the HPC realm the compilers and libraries and runtimes can all be sources of bugs. 

Need to compile or interpret software with a verified compiler or interpreter. 

How can the consistency of content across sources be ensured? 

There are 6 bilateral transitions for the 4 sources. For example, how does the model transition between theorem prover (e.g., Lean) and formally-verified software implementation?

Another possible issue: provenance

May need to track provenance of the source code to binaries. Is the verified algorithm what was provided to the compiler? Is the binary I'm currently using related to the compiler output? Need to be able to distinguish "binary I don't know the origin of" from "binary that has a known chain of custody." 

This could be just a log of hashes coupled to metadata for the "where did this come from." The provenance needs to include versions for compilers and libraries and runtimes. The binary should be reproducible. See https://en.wikipedia.org/wiki/Reproducible_builds

MONTEREY PHOENIX grammar, keywords, and common patterns

MONTEREY PHOENIX grammar

In this table A is an event and B and C are events in A

description of pattern	grammar rule
Ordered sequence of events (B followed by C)	A: B C;
Alternative events (B or C)	A: ( B | C );
Optional event (B or no event at all)	A: [ B ];
Ordered sequence of zero or more events B	A: (* B *);
Ordered sequence of one or more events B	A: (+ B +);
Unordered set of events B and C (B and C may happen concurrently)	A: { B, C };
Unordered set of zero or more events B	A: {* B *};
Unordered set of one or more events B	A: {+ B +};

 

description of pattern	grammar rule
name of model	SCHEMA
Identifies an actor	ROOT
event precedence across swimlanes	COORDINATE
if and only if	<->
	<!>
a condition that each valid trace should satisfy	ENSURE
	FOREACH
	BUILD
	DISJ
	MARK
	ONFAIL
	CHECK
	AFTER
	EXISTS
	MAP
	CLEAR
	SHOW
message box that prints text	SAY("hello world")

Common pattern: branching logic in swimlane

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  move_forward
             stops_car
             exits_car;

Common pattern: dependency across swimlanes

COORDINATE
$a: turn_steering_wheel_right FROM driver,
$b: right FROM front_tires
DO 
ADD $a PRECEDES $b; 
OD;

Common pattern: shared events

Driver, Car SHARE ALL move_forward, 
                      turn_left, 
                      turn_right;

MONTEREY PHOENIX model checker

In this blog post I discuss a model involving two actors: a car and a driver. Each actor has an associated set of actions they can take.

For a video walkthrough of this code, see https://youtu.be/r6aPKem6WLs

Using the web interface https://firebird.nps.edu/, run this model

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue */

/* with space as the separator, 
   the events (blue) are an ordered sequence */

ROOT Driver: enters_car 
             starts_car
             move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

Introduce branching logic

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

/* 
      ( A | B ) are alternative events 
*/

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

Events among actors are coordinated

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

/* the two processes are related by specific events */

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;

Actors may take zero or more actions

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

/* 
    {* *} is an unordered set of zero or more events 
*/

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  {* ( move_forward | 
                  turn_left | 
                  turn_right ) *}
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          {* ( move_forward | 
               turn_left | 
               turn_right ) *}
          shutting_down;

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;

Events are shared among actors

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  {* ( move_forward | 
                  turn_left | 
                  turn_right ) *}
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          {* ( move_forward | 
               turn_left | 
               turn_right ) *}
          shutting_down;

Driver, Car SHARE ALL move_forward, 
                      turn_left, 
                      turn_right;

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;