Creusot 0.14.0: מפרטי סדר חלקי, תנאי אימות ל-snapshot וניווט ב-rust-analyzer

סדרים חלקיים

Creusot 0.14.0 הוא מהדורה של כלי האימות הפורמלי של Rust. בהערות המהדורה נאמר שסדרים חלקיים הם חלק קטן מהתכונות החדשות, והשאר מופיע ב-changelog המלא.

גרסאות מוקדמות יותר הגבילו את מפרט PartialOrd לסדרים מלאים. מגרסה 0.13.0 ההגבלה רוככה כדי לאפשר גם סדרים חלקיים. תכונת הסדר המלא הקודמת, OrdLogic, הסתמכה על cmp_log, האנלוג הלוגי של cmp, שמחזיר Ordering. הדבר הפך את השלמות למשתמעת: כל שני איברים היו חייבים להשוות כ-Less, Equal או Greater.

תכונת הסדר החלקי המחמיר החדשה, PartialOrdLogic, מבוססת לעומת זאת על lt_log, פונקציית השוואה לוגית, עם חוקי אי-רפלקסיביות וטרנזיטיביות. השלמות היא כעת חוק נפרד ב-OrdLogic, בשם lt_log_total, שמבטיח self < other || self == other || other < self. המפתחים מציינים שאף אחת מההוכחות הקיימות לא נפגעה ושמוכיחים אוטומטיים התמודדו עם השינוי.

תנאי אימות עבור snapshots

Creusot מייצר כעת תנאי אימות עבור snapshots, שהם ביטויים לוגיים המוטמעים בתוכניות Rust. זה משפר את השימוש בפונקציות lemma, אידיומה בכלי אימות דומים ל-Creusot.

ניתן לכתוב lemma כפונקציה לוגית עם תנאי requires ו-ensures, כלומר טענה ש-hyp(x) מרמז על concl(x) עבור כל x. קריאה ל-lemma בתוך snapshot! הופכת כעת להצהרה ש-hyp(n) נכון, ולהנחה ש-concl(n) נכון, כשהיא מותאמת לארגומנט n קונקרטי. זה לא מכריח את המוכיחים לבצע אינסטנציאציה של כמת אוניברסלי.

ההערות משוות זאת לקריאה רגילה ל-lemma תוכניתית. גם לסגנון המוקדם הזה יש תנאי requires ו-ensures, אבל הוא מכניס קריאה לפונקציית Rust וחייב לעבור את ה-borrow checker, מה שעשוי לדרוש boilerplate כשהמטרה היא רק לתעד עובדות. snapshots נמחקים, ולכן הם קיימים רק לצורך הוכחה פורמלית. בעבר לא נוצרו תנאי אימות עבור snapshot!, כי הם לא היו נחוצים ל-soundness, אך הם עוזרים לגלות שגיאות במפרט מוקדם יותר, למשל אינדוקס מחוץ לגבולות, ומאפשרים טכניקות חדשות.

תמיכה ב-rust-analyzer

Go to definition פועל כעת במפרטי Pearlite. כדי להפעיל זאת, מאקרוים של מפרט כמו requires, ensures, proof_assert! ו-snapshot! מורחבים עבור rust-analyzer, במקום להימחק בזמן קומפילציה רגילה. Creusot מספק את פרמטרי המדריך עבור האפשרויות הדרושות ל-rust-analyzer.

קוד Pearlite מורחב אינו מיועד ל-rustc, מפני שהוא עובר בודק טיפוסים אך לא ב-borrow checker. זו לא הייתה בעיה, מכיוון ש-rust-analyzer אינו מבצע borrow checking. הבעיה שנותרה הייתה שלטוקנים שהתקבלו ממאקרוים של Pearlite היו span-ים גסים מדי. בדוגמה, a + b מתרחב ל-AddLogic::add_logic(a, b), ולכל טוקן שנוצר היה ה-span של הביטוי כולו. כתוצאה מכך, Go to definition מתוך כל מקום בתוך הביטוי הזה חיפש הגדרות עבור creusot_std, logic, ops, AddLogic ו-add_logic.

התיקון נותן ל-add_logic את ה-span של +, בעוד שלמזהים אחרים יש span ברוחב אפס, ש-rust-analyzer מתעלם ממנו. מייחסים לשרה קיניונס את הבהרת העניין. המפתחים אומרים שכתוצאה מכך הניווט במפרטים ב-Creusot נעים בהרבה.

שאלות

קוראים שיש להם שאלות על Creusot יכולים להצטרף לערוץ ה-Zulip של הפרויקט או לפתוח דיון או issue במאגר של Creusot.

מקורות: Lobsters