ガイド
アシュアランスケース
アシュアランスケースとは、システムが定められた用途に十分であるというチームの論証で、各主張、その主張が向けられる用途、そしてそれが拠って立つ証拠から成ります。ケースはリリースポリシーの隣の assurance.yaml に置くのでプルリクエストでレビューされ、Oloproof は各主張を手元の証拠に照らして読みます。主張が証明されたとは決して言いません。どの主張が現在の合格した証拠に拠っているか、どの主張が不合格、古い、または欠けている証拠に拠っているか、どの主張が前提だけに拠っているかを示します。
ケースを書く
version: 1
goals:
- id: G1
statement: The assistant routes tickets well enough for first-line support
scope: first-line support tickets in English
strategy: argue over label accuracy and the misrouting hazard
reassess_when: [the model changes, a new language is supported]
goals:
- id: G1.1
statement: Labels are accurate
evidence:
- rule: label-floor
- id: G1.2
statement: Misrouting stays rare
evidence:
- hazard: missed-label
- record: records/release-42.json
defeaters:
- id: D1
statement: Tickets in other languages misroute
resolved_by:
- rule: label-floor
suite: multilingual
- id: G1.3
statement: The deployment runs the model that was evaluated
assumptions: [the model is pinned by digest in the deployment manifest]ゴールは主張です。最上位のゴールは scope、つまりその主張が向けられる想定用途を述べ、サブゴールはそれを引き継ぎます。strategy は、サブゴールがどのようにゴールを論証するかを言葉で述べます。evidence の各項目は、次のいずれか 1 つだけを挙げます。
- rule: release.yaml のルール。各システムの各スイートでの最新実行で読みます。system と suite は、どの実行を数えるかを絞り込みます。
- hazard: hazards.yaml のハザード（ハザード登録簿）。
- proof: 形式的な性質。証明ルールと同じように読みます（形式証明）。その性質について最後に受け取った結果で、同じモデルの DISPROVED が優先されます。model（ダイジェスト）は一つの形式化されたモデルに絞り込みます。プロジェクトが結果を保持するまで、このリンクは何も支持しません。
- record: oloproof record export が書き出した決定レコードのファイル。プロジェクトのルートからの相対パスで指定します。
assumptions は、ゴールが当然とみなしていることです。defeater はゴールが偽でありうる理由で、その resolved_by の証拠がすべてそれを支持するまで未解決のままです。reassess_when は、何があればチームがゴールに立ち返るべきかを述べます。
確認する
oloproof assurance check確認では、ポリシーにないルールや登録簿にないハザードを挙げたケース、または最上位のゴールが範囲を述べていないケースを拒否し、2 で終了します。そうでなければツリーを表示し、各ゴールに次の 4 つのステータスのいずれかを付けます。
- supported: その証拠のすべての項目とすべてのサブゴールが、現在の証拠に基づいてゴールを支持し、未解決の反証要因がありません。
- undermined: 何らかの証拠が不合格である、古い、または矛盾している、サブゴールが損なわれている、または反証要因が未解決です。
- assumptions_only: 何もゴールを支持しておらず、述べられた前提に拠っています。
- unsupported: それ以外のすべてで、各欠落の名前が挙がります。一部の支持と欠落をあわせ持つゴールは支持されていないものとなります。主張の強さは、拠って立つもののうち最も弱いものの強さだからです。
ルールは、それを決定したすべての最新実行が PASS と言うときにゴールを支持し、いずれかが FAIL と言うときにゴールを損ないます。INSUFFICIENT_EVIDENCE と MANUAL_REVIEW は何も支持しません。ハザードは、それを測定するすべてのルールが合格するときに支持します。形式的結果は、性質が PROVED のときに支持し、DISPROVED のとき、または 1 つのモデルについて 2 つの結果が食い違うときに損ないます。結果が証明するのは形式化されたモデルについてであり、デプロイについてではありません。レコードは、その内容のダイジェストがいまもその ID に一致し、その決定が PASS のときに支持します。もはやプロジェクトに一致しない実行（システム、スイート、評価器、ポリシーのいずれかが変わった）からの証拠は古く、ゴールを損ないます。これらのステータスはケースのものであって決定ではなく、終了コードを変えることもありません。--json は同じレポートをパイプライン向けに書き出します。
表示される場所
oloproof run は実行とともにケースを記録し、oloproof push は実行のケースを、その証明リンクが名指しする形式的結果とともにワークスペースに運び、oloproof export はエンジンによるケースの読み取り結果をバンドルの隣に書き出します。Safety and risk ページでは、エンジンが書いたとおりの各ステータスとともにツリーを表示し、各ルールはその証拠にリンクします。ワークスペースでは、ケースはプッシュした実行に照らして読まれます。比較するプロジェクトファイルがないため鮮度はそこでは比較されず、レコードのリンクを読むのは oloproof assurance check だけです。決定レコードはその実行が記録したケースを名指しし、record verify はそれをチームの言明として報告します。