Verus Nedir?
Verus, Rust dilinde yazılan kodların doğruluğunu doğrulamak için geliştirilmiş bir araçtır. Temel amacı, düşük seviyeli sistem kodunun tam işlevsel doğruluğunu sağlamaktır. Bu, Dafny, Boogie, F*, VCC, Prusti, Creusot, Aeneas, Cogent, Rocq ve Isabelle/HOL gibi mevcut doğrulama çerçevelerinden elde edilen fikirler üzerine inşa edilmiştir.
Doğrulama statik bir süreçtir; Verus, çalışma zamanı kontrolleri eklemez. Bunun yerine, bilgisayarlı teorem kanıtlamayı kullanarak, yürütülebilir Rust kodunun kullanıcı tarafından sağlanan spesifikasyonları her olası yürütme için her zaman karşılayacağını statik olarak doğrular.
Verus'un Hedefleri
Verus'un hedefleri arasında şunlar bulunmaktadır:
Matematiksel İfade: Spesifikasyonları ifade etmek için saf bir matematik dili sağlamak (Dafny, Creusot, F*, Coq, Isabelle/HOL gibi).
Matematiksel Kanıtlar: Kanıtları ifade etmek için matematiksel bir dil sağlamak (Dafny, F*, Coq, Isabelle/HOL gibi) ve bu, yalnızca klasik mantıkla sınırlı.
Düşük Seviyeli Dil: Yürütülebilir kodu ifade etmek için düşük seviyeli, imperatif bir dil sağlamak (VCC gibi), Rust tabanlı bir yapı (Prusti, Creusot, ve Aeneas gibi).
Verifikasyon Koşulları: SMT çözücüsü (Z3 gibi) tarafından verimli bir şekilde çözülebilecek küçük ve basit doğrulama koşulları üretmek.
Bu hedeflere ulaşmak için, Rust'ın düşük seviyeli veri manipülasyonu ile gelişmiş, yüksek seviyeli ve güvenli bir tür sistemi ile birleştiği düşünülmektedir. Rust'ın tür sistemi, üst düzey doğrulama dillerinde sıkça bulunan özellikleri içerir; bu da spesifikasyonları ve kanıtları doğal bir şekilde ifade etmeyi kolaylaştırır.
Rust ve Verus
Rust, doğrulama süreçlerini kolaylaştıran karmaşık destek sunan bir tür sistemine sahiptir. Örneğin, Rust'ın tür sistemi, hafıza ve takas konularını büyük ölçüde halleder. Bu sayede, geri kalan akıl yürütmeler çoğunlukla hafıza ve takas sorunlarını göz ardı ederek, Rust kodunu sanki tamamen işlevsel bir dilde yazılmış gibi ele alır.
Hedef Dışında Kalanlar
Verus, aşağıdaki durumları desteklemeyi planlamamaktadır:
Tüm Rust özellikleri ve kütüphanelerini desteklemek (bunun yerine, kullanıcıların ihtiyaçlarını desteklemek için yüksek değerli özellikler ve kütüphanelere odaklanılacaktır).
Kendini doğrulamak.
Rust/LLVM derleyicilerini doğrulamak.
Rust Bilgisi ve Verus
Bu kılavuz, Rust programlamanın temel bilgilerine aşina olduğunuzu varsaymaktadır. Rust'ı bilmek, Verus ile daha kolay bir başlangıç yapmanızı sağlar. Çünkü Verus, spesifikasyonları, kanıtları ve yürütülebilir kodu ifade etmek için Rust'ın sözdizimini ve tür sistemini kullanır.
Ancak, Rust kodunun doğruluğunu kontrol etmek, yalnızca sıradan yürütülebilir Rust kodu yazmaktan daha fazla bilgi ve teknik gerektirir. Verus, Rust'ın sözdizimini yeni kavramlarla genişletir ve kullanıcıların kod yazarken bazı yeni türler tanımlamasını gerektirir. Örneğin, forall, exists, requires ve ensures gibi yeni kavramlar kullanılır.
Teorem Kanıtlayıcılar ve Zorluklar
Tüm bu kanıtlar, otomatik bir teorem kanıtlayıcısı (özellikle Z3, bir SMT çözücüsü) yardımıyla gerçekleştirilir. SMT çözücüleri genellikle basit özellikleri otomatik olarak kanıtlayabilir. Ancak daha karmaşık kanıtlar, hem programcı hem de SMT çözücüsü tarafından çaba gerektirebilir. Bu kılavuz, SMT çözümlemenin güçlü ve zayıf yönlerini anlamanıza yardımcı olacak ve SMT çözücülerin otomatik olarak ele alamadığı kanıtların kısımlarını doldurma konusunda tavsiyeler verecektir.
