İçeriğe geç
Belgeler
Değişiklik günlüğüFiyatlandırmaKonsolu aç

Kılavuzlar

Kanıt grafiği

Kanıt grafiği, bir sürüm kararının dayandığı her şeydir; tek bir JSON dosyasında türlü düğümler ve türlü kenarlar olarak yazılır. Bir çalıştırmanın değerlendirdiği sistem, süit ve değerlendirici sürümlerini, ondan hesaplanan tahminleri, bunları bir politikaya göre okuyan kararları, bu kararları onaylayan onayları, kararların ölçtüğü tehlikeleri, destekledikleri güvence argümanı iddialarını ve yanlarındaki biçimsel sonuçları içerir. Ayrıca kanıtın nerede eksik, güncelliğini yitirmiş ya da çelişkili olduğunu adlandırır; böylece bir inceleyici boşlukları başka bir şey okumadan önce görür.

Grafiği çizmek

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

Çalıştırma verilmezse grafik, her sistemin her süitteki son çalıştırmasını kapsar; tehlike kaydının ve güvence argümanının karşısında okunduğu çalıştırmaların aynısı. Bir çalıştırma kimliğiyle o çalıştırmayı ve onu okuyan her iddiayı kapsar. --record ile yalnızca bir karar kaydı dosyasından çizilir; böylece ikinci bir taraf, deponuz olmadan kaydın neler taşıdığını görebilir; kaydın yalnızca adlandırdığı şeyler (tehlike kaydı ve güvence argümanı, özetleriyle) notlarda listelenir. --out olmadan grafik ekrana yazdırılır.

İçinde ne var

Dosya "graph": "oloproof.evidence_graph/v1" der. Her düğümün bir id değeri (türlü, örneğin run:run_01J9 ya da decision:run_01J9/label-floor), bir type, bir label, attributes (bir durum, bir aralık, bir özet) ve dayandığı şeyi belirten bir basis değeri vardır:

  • computed: motor tarafından kaydedilmiş kanıttan hesaplanmış; aralığıyla bir tahmin, bir karar;
  • signed: imzasını oloproof record verify komutunun denetlediği kayıtlı bir runner tarafından imzalanmış;
  • attested: adı belirtilen kişilerce beyan edilmiş; sürüm politikası, bir onay, bir tehlike, bir iddia;
  • imported: başka bir araçtan alınmış; oloproof scores import ile okunan puanlar, bir çözücünün sonucu.

Düğüm türleri system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim ve proof şeklindedir. Kenarlar da türlüdür: bir çalıştırma bir sistem sürümünü evaluates ile değerlendirir ve bir süit sürümü üzerinde on_suite ile çalışır; bir tahmin bir çalıştırmadan computed_from ile hesaplanır ve bir değerlendirici sürümü tarafından judged_by ile yargılanır; bir karar bir tahmini bir politikaya göre reads ve under_policy ile okur; bir onay bir kararı approves ile onaylar; bir tehlike bir karar tarafından measured_by ile ölçülür; ve bir iddia kararlar, tehlikeler, biçimsel sonuçlar ve alt hedefleri tarafından supported_by ile desteklenir.

Neyi bildirir

  • dangling: hedefi grafikte bulunmayan bir kenar, nedeniyle birlikte. Hiçbir çalıştırmanın karara bağlamadığı bir kuralı adlandıran tehlike ya da metriğinin saklanmış sonucu olmayan karar, kaybolmak yerine burada görünür.
  • stale: kanıtı artık karşılaştırıldığı şeyle eşleşmeyen bir çalıştırma; her nedeni ve ona dayanan her düğümle birlikte. Yerelde bir çalıştırma projenin şimdiki haliyle karşılaştırılır; çalışma alanında ve proje dosyası olmadığında ise depodaki aynı sistem ve süitin en yeni çalıştırmasıyla. Bir kayıttan çizilen grafik hiçbir şeyi eskimiş olarak bildirmez, çünkü karşılaştırılacak bir şey yoktur.
  • contradictions: aynı özellik ve aynı model için çelişen iki biçimsel sonuç ve geçmeyen kanıta dayanılarak savunulan bir iddia.

Grafikteki hiçbir şey bir karar vermez: durumlar motorun kararlarıdır ve bir iddianın durumu oloproof assurance check komutunun bildirdiği durumdur.

Çalışma alanında

Bir çalıştırmanın kanıt sayfası, motorun gönderdiğiniz kanıttan çizdiği grafiği, yönetilen bir çalıştırmanın karar kaydının yanında indirilmek üzere sunar.

Sonraki adımlar