iddqd หรือ unsafe Rust ประเภทที่ยากที่สุด

• iddqd เป็นไลบรารีแมปของ Rust ที่ยืมคีย์จากค่า และถูกใช้เพื่อคงดัชนีในหน่วยความจำของเรคคอร์ดขนาดใหญ่ เช่น inventory ของดิสก์และ sled ใน control plane ของ Omicron ของ Oxide ซึ่งความถูกต้องเป็นเรื่องสำคัญมาก
• BTreeMap มาตรฐานจะเก็บคีย์และค่าแยกกัน ทำให้การส่งต่อยุ่งยากหรืออาจเกิดคีย์ซ้ำที่ไม่สอดคล้องกัน แต่ IdOrdMap จะดึงคีย์จากฟิลด์ภายในเรคคอร์ดเพื่อใช้ค้นหา
• unsafe Rust คือทางหนีสำหรับแสดงโปรแกรมที่ปลอดภัยแต่คอมไพเลอร์พิสูจน์ไม่ได้ และเมื่อโค้ด generic เรียก trait implementation ที่ผู้ใช้ให้มา ก็ต้องทนต่อแม้แต่ safe Rust แบบผิดธรรมดา
• mutable iteration ของ iddqd อาศัย invariant ที่ว่าดัชนีทั้งหมดต้องแตกต่างกันเพื่อขยาย lifetime และ implementation ของ Ord แบบผิดธรรมชาติอาจทำให้ B-tree กับ item set ไม่ตรงกัน จนสร้างดัชนีซ้ำที่ชี้ไปยังรายการเดียวกันได้
• การแก้ไขคือเปรียบเทียบทั้งคีย์และดัชนีร่วมกัน และถ้าล้มเหลวให้ถอยกลับไปใช้ linear scan ที่ไม่เรียกโค้ดผู้ใช้ พร้อมทั้งต้องใช้ Miri, การทดสอบแบบ model-based, panic fault injection และการรีวิวเชิงปฏิปักษ์ด้วย LLM ร่วมกันจึงจะได้ความเชื่อมั่นเพียงพอ

---

ปัญหาที่ iddqd แก้ไข

• iddqd เป็นไลบรารี Rust ที่ให้แมปซึ่งยืมคีย์จากค่า และ Oxide ใช้มันอย่างกว้างขวางใน control plane ของ Omicron
• Omicron คือซอฟต์แวร์ที่อยู่ใจกลางของ Oxide rack ทำหน้าที่จัดสรรทรัพยากรอย่าง compute และ storage และทำให้ rack ทำงานต่อเนื่องได้ หาก iddqd ทำงานผิดพลาด control plane อาจทำงานผิดไปในลักษณะที่คาดเดาได้ยากและวิเคราะห์หาสาเหตุได้ยาก
• โครงสร้างอย่าง BTreeMap<Email, User> ในไลบรารีมาตรฐานของ Rust จะเก็บ email ซึ่งเป็นคีย์ แยกจากค่า
• หากต้องส่งคีย์กับค่าควบคู่กัน ต้องใช้ get_key_value เพื่อดึง (email, user) ออกมา และถ้าสร้างโครงสร้างแยกอย่าง UserRecord ตั้งแต่ตอน fetch ก็จะจัดการยากเมื่อมีชนิดเรคคอร์ดจำนวนมาก
• หากคัดลอก email ไปไว้ใน User ด้วย ก็จะเกิดความเสี่ยงที่ email ในคีย์ของแมปกับ email ภายในค่าจะไม่ตรงกัน
• IdOrdMap ใช้ trait IdOrdItem เพื่อดึงคีย์จากเรคคอร์ด โดยชนิดคีย์สามารถยืมมาจากค่าได้ เช่น type Key<'a> = &'a Email
• ที่ Oxide แพตเทิร์นนี้เหมาะมากกับเรคคอร์ดขนาดใหญ่ เช่นผลลัพธ์จากการ query ฐานข้อมูล และถูกใช้เป็นประโยชน์ในการทำดัชนีเรคคอร์ดขนาดใหญ่ทั่วทั้ง control plane

ความสามารถเพิ่มเติม

• iddqd รองรับคีย์ที่ซับซ้อนซึ่งยืมมาจากหลายฟิลด์แบบ first-class ทำให้จัดการได้โดยไม่ต้องใช้ทางอ้อมอย่าง dynamic dispatch
• BiHashMap และ TriHashMap จะทำดัชนีรายการหนึ่งด้วยคีย์สองหรือสามชุดตามลำดับ ช่วยหลีกเลี่ยงแพตเทิร์นทั่วไปที่ต้องดูแลหลายแมปด้วยมือ
• implementation ของ Serde จะ serialize เป็น sequence แทนที่จะเป็นแมป ทำให้สามารถ serialize คีย์ที่ไม่ใช่สตริงใน JSON ได้ และปฏิเสธคีย์ซ้ำ
• เพื่อความเข้ากันได้ย้อนหลัง จึงยังรองรับการ serialize ในรูปแมปด้วย

จุดที่ unsafe Rust เริ่มยากขึ้น

• ความเสี่ยงหลักใน Rust คือ undefined behavior (UB) และถ้าโค้ดปลอดภัยไม่สามารถทำให้เกิด UB ได้ไม่ว่าด้วยวิธีใด ก็ถือว่า sound แต่ถ้าทำได้ก็ถือว่า unsound
• ภายใน safe Rust คอมไพเลอร์จะปฏิเสธโปรแกรมที่มี UB แต่เนื่องจากข้อจำกัดของการวิเคราะห์แบบสถิต มันจึงปฏิเสธบางโปรแกรมที่ไม่มี UB ไปด้วย
• คีย์เวิร์ด unsafe คือทางหนีสำหรับแสดงโปรแกรมประเภทนี้ โดยผู้เขียนรับผิดชอบเรื่อง soundness เองและขอให้คอมไพเลอร์เชื่อถือ
• กฎของ Rust ที่โค้ด unsafe ต้องรักษาไว้ ได้แก่ ห้ามเกิด data race, ห้ามอ่านหน่วยความจำที่ยังไม่ถูก initialize หรือถูก free แล้ว, ห้ามมี alias ของ &mut หลายตัวที่อ้างถึงบริเวณหน่วยความจำเดียวกัน, และห้ามแก้ไขข้อมูลที่เป็น immutable
• กฎเหล่านี้ให้เหตุผลได้ยาก โดยเฉพาะเรื่อง mutable aliasing และโดยทั่วไปจึงต้องห่อ unsafe ไว้หลัง abstraction ที่ปลอดภัย

ขั้นของการตรวจสอบ abstraction ที่ปลอดภัย

• split_at_mut เป็นเมธอดที่ปลอดภัยซึ่งแบ่ง mutable slice ออกเป็นสองส่วน แต่การแบ่งแบบนี้แสดงด้วย safe Rust อย่างเดียวไม่ได้ จึงต้องใช้ unsafe
• soundness ของ split_at_mut ขึ้นอยู่กับ invariant ของโค้ดปลอดภัยรอบข้าง เช่น รับ &mut [T] มาจริงหรือไม่, ตรวจแล้วหรือไม่ว่า mid <= slice.len(), และคำนวณความยาวที่เหลืออย่างถูกต้องหรือไม่
• get ของ MyVec<T> ขึ้นอยู่กับเงื่อนไขว่า len ถูกต้องและอยู่ในขอบเขต ซึ่งเงื่อนไขนี้เมธอดอื่นทั้งหมดในโมดูลเดียวกันต้องช่วยกันรักษาไว้
• เมื่อโค้ด generic แบบ unsafe เรียกโค้ดที่ผู้ใช้จัดให้ ความยากจะสูงที่สุด
• โค้ด safe Rust ต้องไม่สามารถทำให้โค้ด unsafe เกิด UB ได้ ไม่ว่าจะเขียนมาแบบผิดธรรมชาติหรือเป็นปฏิปักษ์เพียงใด
• โค้ดอย่าง collect_exact ที่เชื่อ len() ของ ExactSizeIterator แล้วเขียนลงไปตาม capacity จะกลายเป็น unsound โดยทั่วไป หาก iterator คืนค่าความยาวเท็จ เพราะจะเขียนลงหน่วยความจำที่ไม่ได้ถูกจัดสรร
• std::io::Read ก็เป็น trait ที่ implementation ที่มีบั๊กอาจคืนจำนวนไบต์ที่อ่านผิดได้ และ Rust RFC 2930 กล่าวถึงปัญหานี้
• iddqd เป็นโครงสร้างข้อมูล generic ที่เรียก trait implementation จากผู้ใช้ จึงอยู่ในหมวดที่ยากที่สุดนี้

โครงสร้างภายในของ iddqd

• iddqd รวม ItemSet ซึ่งเป็นรายการของรายการข้อมูล เข้ากับตารางที่เก็บดัชนี slot
• IdHashMap<T> ใช้ hashbrown::HashTable ที่เก็บ ItemSet<T> และ ItemIndex
• ItemSet<T> มี Vec<ItemSlot<T>> และ ItemSlot<T> อาจเป็น Occupied(T) หรือ Vacant { next: ItemIndex }
• free_head จะชี้ไปยัง slot Vacant ที่เพิ่งถูกปล่อยล่าสุด หรือ sentinel ที่หมายถึงไม่มี free slot และ free_head ร่วมกับ slot Vacant ต่าง ๆ จะก่อเป็น free chain
• เมื่อต้องใส่รายการใหม่ ระบบจะตรวจผ่าน free_head ว่ามี slot ที่นำกลับมาใช้ได้หรือไม่ ถ้ามีก็จะเขียนทับ slot Vacant นั้นเป็น Occupied แล้วเลื่อน free_head ไปยังค่าถัดไป
• หากไม่มี free slot ก็จะ push slot Occupied ใหม่ไว้ท้ายสุด จากนั้นจึงดึงคีย์ คำนวณแฮช และบันทึกดัชนีใหม่ลงใน hash table
• การลบทำในทางกลับกัน คือค้นหาดัชนีจากคีย์ใน hash table แล้วลบออก จากนั้นเปลี่ยน ItemSlot นั้นให้เป็น Vacant และเชื่อม free_head เดิมไว้ใน next
• IdOrdMap ใช้ดัชนีแบบ B-tree แทน hash table ส่วน BiHashMap และ TriHashMap จะเก็บ hash table สองและสามชุดตามลำดับ

mutable iteration และการขยาย lifetime

• IdOrdMap::iter_mut ทำ mutable iteration ของรายการตามลำดับคีย์
• iterator ของ Rust ต้องไม่ให้ค่าที่คืนมายืมตัว iterator เอง เพราะตัวประกอบอย่าง collect อาจเหลือค่าอย่าง Vec<&mut T> ไว้ได้แม้หลังจาก iterator หายไปแล้ว
• เพื่อให้พฤติกรรมนี้ปลอดภัย iterator ต้องไม่คืนค่าเดียวกันซ้ำสองครั้ง
• borrow checker มองเห็นเพียงการเข้าถึงรายการแบบต่อเนื่อง และไม่สามารถรู้ได้ว่าดัชนีทั้งหมดต่างกัน
• iddqd ใช้การขยาย lifetime ด้วย std::mem::transmute::<&mut T, &'a mut T> ซึ่งอาศัย invariant ว่าดัชนีที่ self.iter คืนมานั้นต่างกันทั้งหมด

บั๊กที่เกิดจาก implementation ของ Ord แบบผิดธรรมชาติ

• ใน IdOrdMap ที่มีห้ารายการเรียงตามคีย์ 0 ถึง 4 หากค้นหาคีย์ 0 ผ่าน Entry API ระบบจะได้ OccupiedEntry ที่เก็บ index 0 ไว้ภายใน
• หลังจากนั้น หาก implementation ของ Ord ของ Key ถูกเปลี่ยนให้คืน Equal เสมอโดยไม่ขึ้นกับค่า OccupiedEntry::remove อาจลบรายการผิดเมื่อไล่ลง B-tree อีกรอบ เพราะอาศัยเพียงการเปรียบเทียบคีย์
• ตัวอย่างเช่น หากใน B-tree มีการเปรียบเทียบ (key = 2, index = 2) ก่อน รายการนั้นจะถูกลบเพราะ Equal และเพราะ OccupiedEntry ถือ index 0 อยู่ item 0 ก็จะถูกลบออกจาก item set
• ในสถานะนี้ B-tree ยังเหลือ index 0 อยู่ แต่ slot 0 ใน item set กลายเป็น vacant แล้ว ขณะที่ item 2 ยังอยู่ใน item set แต่ไม่มีตัวชี้จาก B-tree
• หลังจากนั้นเมื่อ Ord กลับมาทำงานปกติ และมีการแทรกรายการคีย์ 1000 ระบบจะนำ slot 0 ที่ free_head ชี้อยู่กลับมาใช้ใหม่
• ผลคือเกิดดัชนีซ้ำใน B-tree ที่ชี้ไปยัง slot เดียวกัน และ IterMut สามารถสร้าง reference แบบ &mut หลายตัวไปยังหน่วยความจำเดียวกันได้ ทำให้ไม่ sound

วิธีแก้และการแลกกับประสิทธิภาพ

• มีการเปลี่ยนให้ตอนค้นใน B-tree ตรวจทั้งคีย์และความเท่ากันของดัชนีร่วมกัน
• เมื่อค้นหาคีย์ที่มีดัชนีที่รู้แน่อยู่แล้ว จะเปรียบเทียบทั้ง (key, index) ดังนั้นแม้ Ord แบบผิดธรรมชาติจะคืน Equal การเปรียบเทียบระหว่าง (key = 2, index = 2) กับ index 0 ที่กำลังหา ก็จะได้ Less เพราะตัวตัดสินกรณีเสมอใช้ index
• การค้นนี้จะสำเร็จได้ก็ต่อเมื่อ index ที่เก็บไว้ตรงกับ index ที่กำลังค้นจริง ๆ
• ตัวตัดสินกรณีเสมอช่วยกันการจับคู่รายการผิด แต่ไม่ได้รับประกันว่าจะหารายการที่ถูกต้องเจอเสมอ
• B-tree เรียงตามคีย์ ขณะที่ตัวตัดสินกรณีเสมอใช้การเปรียบเทียบ index ดังนั้นลำดับทั้งสองโดยทั่วไปเป็นอิสระต่อกัน
• หากการค้นใน tree ล้มเหลว ระบบจะถอยไปใช้ linear scan ที่ไม่เรียกโค้ดผู้ใช้เพื่อลบ index นั้นออกจาก B-tree
• fallback นี้ทำให้การลบจากที่เดิมเป็นเวลา logarithmic กลายเป็น linear time แต่จะเกิดขึ้นได้ก็ต่อเมื่อมีโค้ดผู้ใช้ที่มีบั๊ก จึงถือเป็นการแลกที่ยอมรับได้

ชั้นของการตรวจสอบ

• เนื่องจาก iddqd ถูกใช้เป็นโครงสร้างข้อมูลพื้นฐาน จึงใช้ทั้งการทบทวนเชิงวิเคราะห์และการตรวจสอบเชิงประจักษ์หลายแบบร่วมกัน
• ทุก unsafe block และ unsafe pattern ถูกวิเคราะห์โดยผู้เขียนและผู้รีวิว Rust จำนวนหนึ่งถึงสามคน
• เหนือแต่ละ unsafe block จะมีคอมเมนต์ // SAFETY: อธิบายเหตุผล และใช้ lint undocumented_unsafe_blocks ของ Clippy เพื่อตรวจว่ามีคอมเมนต์นี้อยู่
• example-based test จะสร้างแมป ดำเนินการต่าง ๆ แล้วตรวจผลลัพธ์ โดย iddqd มีทั้ง unit test ภายในและ integration test ของ public API
• การทดสอบเหล่านี้ยังมีในรูป doctest ด้วย จึงทำหน้าที่เป็นเอกสารไปพร้อมกัน
• มีการทดสอบแบบผิดธรรมชาติที่ป้อน Ord ที่มีบั๊กและ trait implementation อื่น ๆ เข้ามา
• ใน CI จะรันทั้ง regular test และ pathological test ภายใต้ Miri เพื่อจับ UB ได้หลายประเภท
• เงื่อนไขอย่าง invariant ที่ห้ามมีดัชนีซ้ำ สามารถตรวจได้ในสภาพแวดล้อมทดสอบปกตินอก Miri เช่นกัน

model-based testing และ fault injection

• iddqd ใช้ randomized testing สองชั้น: model-based testing ที่เทียบกับ oracle ที่ถูกต้อง และ fault injection ที่วางซ้อนอยู่ด้านบน
• model-based testing หรือ stateful property-based testing จะนำลำดับการดำเนินการแบบสุ่มไปใช้กับอินสแตนซ์ของชนิด แล้วเทียบผลกับ oracle ที่ทราบว่าถูกต้อง
• iddqd รัน model-based test อย่างกว้างขวางเทียบกับ NaiveMap oracle ซึ่งไม่มีประสิทธิภาพแต่ชัดเจนว่าถูกต้อง
• fault injection คือการใส่บั๊กแบบสุ่มเข้าไปในโค้ดผู้ใช้ และสำหรับ iddqd แกนที่ได้ผลเป็นพิเศษคือ panic safety
• ต่อให้โค้ดผู้ใช้ panic ระหว่างทำงาน invariant ของแมปก็ต้องไม่พัง
• แต่ละการทำงานของแมปจะถูกแนบ panic countdown แบบสุ่มไว้ และทุกครั้งที่มีการเรียกโค้ดผู้ใช้ countdown จะลดลง 1 จนเมื่อถึง 0 ก็ panic ทำให้เกิดการทดสอบ panic safety แบบสุ่ม
• วิธีนี้พบเจอบั๊กละเอียดอ่อนหลายตัวใน iddqd และบางตัวนำไปสู่ unsoundness
• model-based test ยังตรวจ invariant ภายในอย่าง no-duplicate-index หลังจบแต่ละการทำงานด้วย
• เนื่องจาก model-based test ช้าเกินกว่าจะรันภายใต้ Miri จึงแยกตรวจ invariant ที่ soundness และ correctness พึ่งพาออกมาต่างหาก

การรีวิวเชิงปฏิปักษ์ด้วย LLM และเทคนิคเชิงรูปแบบ

• โมเดล frontier รุ่นปัจจุบันสามารถค้นหา implementation ของโค้ดผู้ใช้แบบผิดธรรมชาติที่ทำให้แมปเสียหายได้หลายแบบ
• ในกรณีหนึ่งที่น่าสนใจ LLM สร้างเส้นทางที่ custom allocator panic ระหว่าง unwind แล้วทำให้ invariant ของแมปพัง
• นี่เป็นปัญหา panic safety คนละแบบกับ panic ทั่วไปจากโค้ดผู้ใช้อย่าง implementation ของ Ord ที่การทดสอบ panic safety เดิมครอบคลุมอยู่แล้ว
• LLM สามารถสร้างข้ออ้างเรื่อง soundness ที่ดูน่าเชื่อแต่ผิดได้ ดังนั้น red-green TDD ที่ใช้ Miri เป็น oracle จึงเป็นแนวป้องกัน
• สำหรับ soundness bug จะเริ่มจากสร้างการทดสอบที่แสดง UB ภายใต้ Miri ก่อน แล้วหลังแก้จึงตรวจอีกครั้งว่าการทดสอบเดิมผ่านได้หรือไม่
• แนวทางใช้ model checker อย่าง Kani เพื่อพิสูจน์ invariant ของแมปนั้นทำได้ยาก เพราะ iddqd ซับซ้อนเกินไปจน proof ที่ต้องใช้ใหญ่เกินกว่าที่เครื่องมือจะรับไหว
• Creusot อาจช่วยพิสูจน์ได้ว่าโค้ด Rust ปลอดจาก panic และความผิดพลาดอื่น แต่ในตอนนี้ยังพิสูจน์ invariant ที่ต้องคงอยู่แม้โค้ดผู้ใช้จะ panic หรือทำงานผิดไม่ได้
• NaiveMap ทำหน้าที่ใกล้เคียง specification ที่สุดสำหรับ iddqd และใน CI มีการรัน model-based test หลายพันครั้งเพื่อสร้างความเชื่อมั่นสูงว่า implementation ตรงกับ specification
• cargo-anneal เป็นเครื่องมือที่กำลังพัฒนาและน่าสนใจ เพราะช่วยใส่ soundness proof แบบ Lean ไว้ใน doc comment ข้างโค้ด unsafe Rust ได้
• iddqd มี invariant ที่ชัดเจนและขอบเขตที่จำกัดแต่ไม่เล็กน้อย จึงเหมาะเป็นตัวเลือก benchmark สำหรับเครื่องมือ formal verification

บทสรุป

• unsafe generic Rust ยากอย่างยิ่ง เพราะต้องรักษา invariant ทุกข้อโดยคำนึงถึงทั้ง trait implementation ตามปกติและแบบปฏิปักษ์
• บั๊กของ iddqd แสดงให้เห็นว่า implementation ของ Ord แบบผิดธรรมชาติสามารถหลอกแมปให้สร้าง mutable alias ไปยังหน่วยความจำเดียวกันได้
• ไม่มีเทคนิคเดียวที่จับบั๊กทั้งหมดได้ จึงต้องใช้ทั้งการให้เหตุผลกับ unsafe ทีละบรรทัดโดยมนุษย์, example-based test, pathological test, randomized test และการรีวิวเชิงปฏิปักษ์ด้วย frontier model ร่วมกัน
• Oxide มองว่าความเข้มงวดระดับนี้สมเหตุสมผลสำหรับโครงสร้างพื้นฐานที่เป็นรากฐาน

[GN⁺]

ความคิดเห็นจาก Lobste.rs

• ถ้าฉันเข้าใจถูกนะ (กำลังเดินทางเลยอ่านจากมือถือ) ดูเหมือนว่านี่แก้ได้ด้วยการใช้ wrapper type และใช้ HashSet/BTreeSet แทน HashMap/BTreeMap
  ไม่ถึงกับจำเป็นต้องมี wrapper type แต่ถ้ามองเรื่องความปลอดภัยและการบำรุงรักษาในอนาคต ก็น่าจะเป็นตัวเลือกที่ดี
  สิ่งที่ต้องมีคือแค่ wrapper ขนาด 0 ที่ห่อออบเจ็กต์ไว้ แล้วใส่ implementation ของ PartialEq/Hash แบบกำหนดเองที่ดูเฉพาะฟิลด์ที่สนใจ ถ้าต้องการค้นหาโดยไม่สร้างค่าทั้งก้อน ก็อาจสร้าง type ที่สองซึ่ง implement AsRef สำหรับ value type ได้
  วิธีนี้คือการนำ interface เดิมของ HashSet/BTreeSet กลับมาใช้ตรง ๆ โดยไม่ต้องใช้ unsafe แทนที่จะห่อ value/key type ก็อาจสร้าง wrapper ใหม่ของ HashSet/BTreeSet ที่ทำพฤติกรรมแบบนี้ให้แทนได้เช่นกัน

  • ตรงนี้ key คือการผสมกันแบบอิสระของฟิลด์และ subfield ของ record type ซึ่งแสดงด้วย GAT และแพตเทิร์น integer index/slab ก็ขยายเป็น multi-index map ได้อย่างเป็นธรรมชาติด้วย
    มีทั้ง Entry API, การเข้าถึงแบบแก้ไขได้/การวนซ้ำ ฯลฯ อยู่ในนั้นด้วย ภายใน iddqd จัดการเรื่อง mutability อย่างระมัดระวังพอสมควร และในบางจุดก็ใช้ค่าระดับอะตอมเพื่อยอมให้มี interior mutability การจัดการแบบนี้คงทำได้ค่อนข้างยากหากไม่มี index indirection

• ถ้าจะทำ formal verification ให้ iddqd ตอนแรกฉันคงลองใช้ model checker อย่าง Kani เพื่อพิสูจน์ว่า map ไม่ทำลาย invariant ภายใน แต่ที่บอกว่า iddqd ซับซ้อนเกินกว่าที่ Kani จะรับมือได้เล็กน้อย และ proof ที่ต้องใช้ใหญ่เกินกว่าที่เครื่องมือจะไหว ตรงนี้ทำให้ฉันสงสัยมาก
  ช่วยเล่ารายละเอียดส่วนนี้เพิ่มได้ไหม? ฉันสงสัยว่าหมายถึงความซับซ้อนเชิงคำนวณของอัลกอริทึมเสื่อมลงเป็นกรณีเลวร้ายสุดหรือเปล่า
  โดยรวมแล้วนี่น่าสนใจมากในฐานะกรณีศึกษาของ formal methods และดีใจที่ยกประเด็นนี้ขึ้นมา ปกติถ้าดูกรณีที่เครื่องมือ formal verification เดิม ๆ ประสบความสำเร็จในโปรเจ็กต์ขนาดใหญ่ ก็อาจคิดแบบไร้เดียงสาว่าอย่างน้อยก็น่าจะพิสูจน์ความถูกต้องของ data structure ได้ แต่ในความเป็นจริงระดับความยากต่างกันไปตามแต่ละ data structure และถึงแม้อยู่ในภาษาที่มักถูกมองว่าเอื้อต่อการพิสูจน์มากกว่า Rust ซึ่งยอมให้ aliasing แบบไม่จำกัด ก็ยังไม่ใช่เรื่องง่ายในทางปฏิบัติ
  นอกเรื่องไปนิด แต่ฉันก็สงสัยด้วยว่าทำไดอะแกรมกันอย่างไร เขียนสคริปต์ใช้ครั้งเดียวขึ้นมาหรือเปล่า เพราะมันดูเหมือนงานทำเฉพาะให้เข้ากับดีไซน์ของบล็อก/เว็บไซต์ Oxide มากกว่าเป็นเครื่องมือทั่วไป

  • ด้านล่างบทความเขียนไว้ว่า “Diagrams courtesy Ben Leonard.” และ Ben Leonard ก็เป็นดีไซเนอร์ของ Oxide ดังนั้นมันน่าจะเป็น ไดอะแกรมทำมือ ก็ได้
  • แม้จะพยายามพิสูจน์เรื่องพื้นฐานมาก ๆ กับ implementation ของ trait ที่เฉพาะเจาะจงและทำงานได้ดี CBMC ก็ยังใช้ CPU อยู่และ เกิน 10 นาที ก็ยังไม่เสร็จ
    ฉันลองลดขอบเขตลงด้วย เช่น สมมติว่า hashbrown ถูกต้องแล้ว แต่ก็ไม่ได้ช่วยให้คืบหน้ามากนัก ถึงจุดนั้นก็แทบจะยอมแพ้แล้ว สำหรับ implementation ของ trait ที่ทำงานได้ดี ฉันค่อนข้างมั่นใจว่า iddqd ถูกต้อง และสิ่งที่ฉันสนใจจริง ๆ ใน formal methods คือ proof ที่ยังใช้ได้แม้กับ implementation ที่เป็นไปตามอำเภอใจและทำงานผิดพลาด
    แต่ฉันก็ไม่ใช่คนที่ใช้ Kani ได้เก่งที่สุด ถ้าคุณหรือใครก็ตามอยากลองทำเรื่องนี้จริง ๆ ฉันคงดีใจมาก
    ส่วนไดอะแกรม ฉันเริ่มจากร่างด้วย Mermaid ก่อน แล้วดีไซเนอร์มากฝีมือ Ben Leonard ก็นำไปเกลามาเป็นไดอะแกรมด้วยมือให้เข้ากับ ชุดสีและธีม ของเรา

• แพตเทิร์น field-based map ที่ทำดัชนีออบเจ็กต์โดยใช้หนึ่งในฟิลด์ของมันเป็น key เป็นสิ่งที่ฉันรู้สึกเสมอว่าอยากให้ใช้ได้ตลอดใน C#
  เมื่อก่อนเคยพยายามทำอะไรเรียบง่ายเอง แต่ interface มันไม่ค่อยสะอาดนักเลยเลิกไป พออ่านบทความนี้แล้วก็ทำให้อยากลองอีกครั้ง

  • ใช่แล้ว มันเป็นแพตเทิร์นที่มีประโยชน์มาก ฉันสร้างมันขึ้นมาเพราะงานที่ต้องใช้ในบริษัท แต่หลังจากนั้นก็ได้ใช้มันไปทั่ว ตั้งแต่โค้ดเบส production อย่าง cargo-nextest ไปจนถึงโปรเจ็กต์ส่วนตัว
    แม้กรณีใช้ฟิลด์เดียวเป็น key จะพบบ่อยที่สุด แต่ iddqd ยืดหยุ่นพอที่จะใช้การผสมกันแบบใดก็ได้ของฟิลด์, subfield หรือฟังก์ชันที่คำนวณจากฟิลด์ได้อย่างบริสุทธิ์และมีต้นทุนต่ำ ตัวอย่างเช่นลองค้นหา ArtifactKey ใน https://docs.rs/iddqd/latest/iddqd/ ได้ (ขออภัยหากคุณไม่คุ้นกับไวยากรณ์ Rust)
    ตอนออกแบบ iddqd ฉันรู้สึกอย่างแรงกล้าว่าผู้ใช้ควรเข้าถึงพลังทั้งหมดของระบบชนิดของ Rust ได้ ไม่ว่าฉันในฐานะผู้เขียนไลบรารีจะต้องอ้อมไปใช้วิธีแก้มากแค่ไหนก็ตาม ฉันอยากให้ iddqd เป็น ไลบรารีที่ใช้งานแล้วรู้สึกสนุก สำหรับผู้ใช้จริง ๆ โดยเฉพาะเพื่อนร่วมงานของฉัน