Guides

Graphe de preuves

Le graphe de preuves est tout ce sur quoi repose une décision de publication, écrit sous forme de nœuds typés et d’arêtes typées dans un seul fichier JSON. Il contient les versions de système, de suite et d’évaluateur qu’une exécution a évaluées, les estimations calculées à partir d’elle, les décisions qui les lisent selon une politique, les approbations qui les ont validées, les dangers qu’elles mesurent, les affirmations de l’argumentaire d’assurance qu’elles soutiennent et les résultats formels à côté. Il nomme aussi les endroits où les preuves sont incomplètes, périmées ou contradictoires, afin qu’un relecteur voie les lacunes avant de lire quoi que ce soit d’autre.

Le dessiner

oloproof evidence graph --out graph.json
oloproof evidence graph run_01J9 --out run.json
oloproof evidence graph --record decision-record.json --out record-graph.json

Sans exécution, le graphe couvre la dernière exécution de chaque système sur chaque suite, les mêmes exécutions au regard desquelles sont lus le registre des dangers et l’argumentaire d’assurance. Avec un identifiant d’exécution, il couvre cette exécution et chaque affirmation qui la lit. Avec --record, il est dessiné à partir d’un seul fichier d’enregistrement de décision, pour qu’un tiers voie ce que porte l’enregistrement sans votre stockage ; ce que l’enregistrement ne fait que nommer (son registre des dangers et son argumentaire d’assurance, par empreinte) est listé dans les notes. Sans --out, le graphe est affiché.

Ce qu’il contient

Le fichier indique "graph": "oloproof.evidence_graph/v1". Chaque nœud a un id (typé, comme run:run_01J9 ou decision:run_01J9/label-floor), un type, un label, des attributes (un état, un intervalle, une empreinte) et une basis, ce sur quoi il repose :

computed par le moteur à partir de preuves enregistrées : une estimation avec son intervalle, une décision ;
signed par un runner enregistré, dont oloproof record verify vérifie la signature ;
attested par des personnes nommées : la politique de publication, une approbation, un danger, une affirmation ;
imported depuis un autre outil : des scores lus par oloproof scores import, le résultat d’un solveur.

Les types de nœuds sont system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim et proof. Les arêtes sont typées aussi : une exécution evaluates une version de système et s’exécute on_suite sur une version de suite ; une estimation est computed_from une exécution et judged_by une version d’évaluateur ; une décision reads une estimation under_policy une politique ; une approbation approves une décision ; un danger est measured_by une décision ; et une affirmation est supported_by des décisions, des dangers, des résultats formels et ses sous-objectifs.

Ce qu’il signale

dangling : une arête dont le graphe ne contient pas la cible, avec la raison. Un danger qui nomme une règle qu’une exécution n’a pas décidée, ou une décision dont la métrique n’a aucun résultat stocké, apparaît ici au lieu de disparaître.
stale : une exécution dont les preuves ne correspondent plus à ce à quoi elles sont comparées, avec chaque raison et chaque nœud qui repose sur elle. En local, une exécution est comparée au projet tel qu’il est maintenant ; dans l’espace de travail, et sans fichier de projet, à l’exécution la plus récente du stockage pour le même système et la même suite. Un graphe dessiné à partir d’un enregistrement ne signale rien de périmé, puisqu’il n’y a rien avec quoi le comparer.
contradictions : deux résultats formels pour une même propriété et un même modèle qui divergent, et une affirmation argumentée à partir d’une preuve en échec.

Rien dans le graphe ne décide quoi que ce soit : les états sont les décisions du moteur, et le statut d’une affirmation est celui que rapporte oloproof assurance check.

Dans l’espace de travail

La page de preuves d’une exécution propose le graphe en téléchargement, dessiné par le moteur à partir des preuves que vous avez envoyées, à côté de l’enregistrement de décision d’une exécution gouvernée.

Pour aller plus loin

Argumentaires d’assurance couvre les affirmations que le graphe dessine.
Registre des dangers couvre les dangers qu’une décision mesure.