Creusot 0.14.0: Kısmi sıralama spesifikasyonları, snapshot VC'leri ve rust-analyzer navigasyonu

Kısmi sıralamalar

Creusot 0.14.0, Rust için resmi doğrulama aracıdır. Sürüm notlarına göre kısmi sıralamalar yeni özelliklerin küçük bir parçasıdır; geri kalanı tam changelog'da.

Önceki sürümler PartialOrd spesifikasyonunu tam sıralamalarla sınırlıyordu. 0.13.0'dan itibaren kısmi sıralamalara izin verildi. Eski OrdLogic trait'i, Ordering döndüren cmp'nin mantıksal karşılığı cmp_log'a dayanıyordu. Bu, tamlığı örtük yapıyordu: her iki öğe Less, Equal veya Greater olarak karşılaştırılmalıydı.

Yeni katı kısmi sıralama trait'i PartialOrdLogic ise bunun yerine, yansımasızlık ve geçişlilik yasalarına sahip mantıksal karşılaştırma fonksiyonu lt_log'a dayanır. Tamlık artık OrdLogic'te lt_log_total adlı ayrı bir yasadır ve self < other || self == other || other < self sağlar. Geliştiriciler mevcut kanıtların zarar görmediğini ve otomatik kanıtlayıcıların değişiklikle başa çıktığını belirtiyor.

Snapshot'lar için doğrulama koşulları

Creusot artık snapshot'lar için, Rust programlarına gömülü mantıksal ifadeler olan doğrulama koşulları üretiyor. Bu, Creusot benzeri doğrulama araçlarında lemma fonksiyonlarının kullanımını iyileştirir.

lemma, requires ve ensures koşullarıyla mantıksal bir fonksiyon olarak yazılabilir; bu, hyp(x)'in tüm x'ler için concl(x)'i gerektirdiği anlamına gelir. Bu lemma'nın snapshot! içinde çağrılması artık hyp(n) için assert'e, concl(n) için varsayıma dönüşür. Bu, kanıtlayıcıları evrensel niceleyiciyi örneklemeye zorlamaz.

Notlar bunu sıradan bir programlama lemma'sı çağrısıyla karşılaştırıyor. O eski stilde de requires ve ensures vardır, ancak Rust fonksiyon çağrısı yerleştirir ve borrow checker'dan geçmelidir; yalnızca gerçekleri kaydetmek istendiğinde boilerplate gerektirebilir. snapshot'lar silinir, bu yüzden yalnızca biçimsel kanıt için vardır. snapshot! için doğrulama koşulları daha önce üretilmiyordu, çünkü soundness için gerekli değildi; ancak bunlar spesifikasyon hatalarını daha erken bulmaya, örneğin sınır dışı indekslemeye, yardımcı olur ve yeni tekniklere olanak sağlar.

rust-analyzer desteği

Go to definition artık Pearlite spesifikasyonlarında çalışıyor. Bunu etkinleştirmek için requires, ensures, proof_assert! ve snapshot! gibi spesifikasyon makroları, normal derlemede silinmek yerine rust-analyzer için genişletiliyor. Creusot, rust-analyzer için gereken seçenek ayarlarını sağlıyor.

Genişletilmiş Pearlite kodu rustc için değildir; tür denetleyicisinden geçer ama borrow checker'dan geçmez. Bu sorun değildi, çünkü rust-analyzer borrow checking yapmaz. Kalan sorun, Pearlite makrolarından gelen token'ların fazla kaba span'lere sahip olmasıydı. Örnekte a + b, AddLogic::add_logic(a, b) olarak genişler ve tüm token'lar tüm ifadenin span'ine sahipti. Sonuç olarak Go to definition bu ifadenin herhangi bir yerinden creusot_std, logic, ops, AddLogic ve add_logic tanımlarını arıyordu.

Düzeltme, add_logic'e +'nın span'ini verirken diğer tanımlayıcılara rust-analyzer'ın yok saydığı sıfır genişlikli span veriyor. Bu, Sara Kinyon'a atfediliyor. Geliştiricilere göre Creusot'ta spesifikasyonlar içinde gezinmek artık çok daha keyifli.

Sorular

Creusot hakkında soruları olan okuyucular projenin Zulip kanalına katılabilir veya Creusot deposunda tartışma ya da issue açabilir.

Kaynaklar: Lobsters