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: Մշակողները նշում են, որ գոյություն ունեցող ապացույցներից ոչ մեկը վնասված չէ, և ինքնատիպ պրովերները հաղթահարում են փոփոխությունը:

Snapshot-ների համար վերիֆիկացիայի պայմաններ

Creusot-ը այժմ վերիֆիկացիայի պայմաններ է գեներացնում snapshot-ների համար, որոնք Rust-ի ծրագրերում ներկառուցված տրամաբանական արտահայտումներ են: Սա բարելավում է lemma ֆունկցիաների օգտագործումը՝ իդիոմ, որը նման է Creusot-ի նման վերիֆիկացիայի գործիքներում:

lemma-ը կարող է գրվել որպես տրամաբանական ֆունկցիա requires և ensures պայմաններով, ինչը նշանակում է պնդում, որ hyp(x) ենթադրում է concl(x)-ը բոլոր x-երի համար: Ասերտի snapshot!-ում այժմ փոխվում է, որպեսզի լինի hyp(n)-ը ճշմարիտ և ընդունելի, որ concl(n)-ը ճշմարիտ է կոնկրետ n արգումենտի համար՝ մասնավորացված: Սա չի պարտադրում պրովերներին ունիվերսալ քանտոր ինստանցիացնել:

Նշումները համեմատում են սովորական ծրագրային lemma-ի կանչի հետ: Նախորդ ոճը նույնպես ունի requires և ensures պայմաններ, բայց այն զուգորդում է Rust-ի ֆունկցիայի կանչին և պետք է անցնի borrow checker-ը, ինչը կարող է պահանջել boilerplate, երբ նպատակը միայն փաստերի ֆիքսումն է: Snapshot-ները հեռացվում են, ուստի դրանք գոյություն ունեն միայն պաշտոնական ապացույցների համար: 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