แปล crate `core` และ `alloc` ของ Rust เป็น Coq เพื่อทำการพิสูจน์เชิงรูปนัย

การแปล crate core และ alloc ของ Rust

การรันครั้งแรก 🐥

• จากการรันครั้งแรกกับ crate alloc และ core ของ Rust โดยใช้ coq-of-rust ได้ไฟล์โค้ด Coq ขนาดหลายแสนบรรทัดออกมาสองไฟล์
• สิ่งนี้แสดงให้เห็นว่าเครื่องมือสามารถทำงานกับโค้ดเบสขนาดใหญ่ได้ แต่โค้ด Coq ที่สร้างขึ้นยังคอมไพล์ไม่ผ่าน โดยข้อผิดพลาดเกิดขึ้นไม่บ่อยนัก (ประมาณหนึ่งครั้งต่อทุก ๆ หลายพันบรรทัด)

ขนาดของโค้ด Rust ขาเข้า (อ้างอิงจากคำสั่ง cloc)

• alloc: โค้ด Rust 26,299 บรรทัด

• core: โค้ด Rust 54,192 บรรทัด

• เนื่องจากต้องขยายแมโครก่อนแปล ขนาดที่ต้องแปลจริงจึงมากกว่านี้

การแยกโค้ดที่สร้างขึ้น 🪓

• การเปลี่ยนแปลงหลักคือแยกผลลัพธ์ที่ coq-of-rust สร้างออกมาให้เป็นหนึ่งไฟล์ต่อหนึ่งไฟล์ Rust ขาเข้า
• ที่ทำได้เช่นนี้เพราะสามารถแปลได้โดยไม่ขึ้นกับลำดับของนิยาม แม้ว่า Coq จะไม่อนุญาตการอ้างอิงวนกันระหว่างไฟล์ Rust แต่ก็ยังสามารถแยกไฟล์ได้อยู่

ขนาดของผลลัพธ์

• alloc: ไฟล์ Coq 54 ไฟล์, โค้ด Coq 171,783 บรรทัด
• core: ไฟล์ Coq 190 ไฟล์, โค้ด Coq 592,065 บรรทัด

ข้อดีของการแยกโค้ด

• อ่านและสำรวจโค้ดที่สร้างขึ้นได้ง่ายขึ้น
• คอมไพล์แบบขนานได้ ทำให้คอมไพล์ง่ายขึ้น
• ดีบักได้ง่ายขึ้นโดยโฟกัสทีละไฟล์
• ข้ามไฟล์ที่คอมไพล์ไม่ผ่านได้ง่าย
• ติดตามการเปลี่ยนแปลงของไฟล์เดี่ยวได้ง่าย จึงดูแลรักษาได้สะดวกขึ้น

การแก้บั๊กบางส่วน 🐞

• มีบั๊กที่เกิดจากการชนกันของชื่อโมดูล ซึ่งเกิดขึ้นตอนเลือกชื่อโมดูลของบล็อก impl
• จึงเพิ่มข้อมูลเข้าไปในชื่อโมดูลมากขึ้นเพื่อให้มีความเป็นเอกลักษณ์มากขึ้น เช่น เพิ่มเงื่อนไข where

ตัวอย่าง

• การ implement ชนิด Mapping สำหรับ trait Default:

  #[derive(Default)]
  struct Mapping<K, V> {
    // ...
  }
  

• โค้ด Coq แบบเดิม:

  Module Impl_core_default_Default_for_dns_Mapping_K_V.
  (* ...trait implementation ... *)
  End Impl_core_default_Default_for_dns_Mapping_K_V.
  

• โค้ด Coq ที่แก้ไขแล้ว:

  Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
  (* ... *)
  

รายชื่อไฟล์ที่คอมไพล์ไม่ผ่าน

• alloc/boxed.v

• core/any.v

• core/array/mod.v

• core/cmp/bytewise.v

• core/error.v

• core/escape.v

• core/iter/adapters/flatten.v

• core/net/ip_addr.v

• คิดเป็น 4% ของไฟล์ทั้งหมด และแม้แต่ในไฟล์ที่คอมไพล์ผ่าน ก็อาจยังมีโครงสร้าง Rust ที่ยังไม่ได้รองรับอยู่

ตัวอย่าง 🔎

โค้ดต้นฉบับของเมธอด unwrap_or_default ของชนิด Option

pub fn unwrap_or_default(self) -> T
where
  T: Default,
{
  match self {
    Some(x) => x,
    None => T::default(),
  }
}

โค้ด Coq ที่แปลแล้ว

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

โค้ดฟังก์ชันแบบทำให้ง่ายลง

Definition unwrap_or_default {T : Set}
  {_ : core.simulations.default.Default.Trait T}
  (self : Self T) :
  T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.

• นิยามแบบย่อส่วนนี้ถูกใช้ระหว่างการพิสูจน์โค้ด และการพิสูจน์ความสมมูลอยู่ใน CoqOfRust/core/proofs/option.v

บทสรุป

• การทำให้ไลบรารีมาตรฐานเป็นแบบเชิงรูปนัยช่วยให้เชื่อถือการตรวจพิสูจน์โปรแกรม Rust ได้มากขึ้น

• เป้าหมายถัดไปคือทำให้กระบวนการพิสูจน์ที่ยังยุ่งยากให้ง่ายขึ้น โดยเฉพาะการแยกขั้นตอนอย่างการแก้ชื่อ การนำชนิดขั้นสูงเข้ามาใช้ และการกำจัดผลข้างเคียง ออกจากกระบวนการแสดงว่าการจำลองมีความสมมูลกับโค้ด Rust ต้นฉบับ

• หากสนใจการพิสูจน์เชิงรูปนัยของโปรเจ็กต์ Rust โปรดติดต่อที่ [e-mail] การพิสูจน์เชิงรูปนัยมอบความปลอดภัยระดับสูงสุดด้วยการรับประกันทางคณิตศาสตร์ว่าไม่มีบั๊กเมื่อเทียบกับข้อกำหนดที่กำหนดไว้

แท็ก:

• coq-of-rust
• Rust
• Coq
• การแปล
• core
• alloc

ความเห็นของ GN⁺

1. การบูรณาการ Rust และ Coq: การบูรณาการ Rust กับ Coq ช่วยยกระดับความน่าเชื่อถือของโปรแกรม Rust ได้อย่างมาก เมื่อนำความปลอดภัยของ Rust มารวมกับการพิสูจน์เชิงรูปนัยของ Coq จะมีประโยชน์มากเป็นพิเศษกับแอปพลิเคชันสำคัญ
2. ความสำคัญของระบบอัตโนมัติ: การแปลอัตโนมัติด้วยเครื่องมือ coq-of-rust มีความน่าเชื่อถือสูงกว่าการทำด้วยมือ แต่ก็ยังต้องระวัง เพราะในกระบวนการพิสูจน์ยังอาจเกิดข้อผิดพลาดได้
3. การจัดการโค้ดเบสที่ซับซ้อน: สำหรับการจัดการโค้ดเบสขนาดใหญ่ การแยกโค้ดช่วยเรื่องการบำรุงรักษาและการดีบักได้มาก ซึ่งสำคัญอย่างยิ่งในงานที่ทำร่วมกันเป็นทีม
4. ความจำเป็นของการพิสูจน์เชิงรูปนัย: การพิสูจน์เชิงรูปนัยมีความจำเป็นอย่างยิ่งในสาขาสำคัญ เช่น การเงิน การแพทย์ และการบิน การผสาน Rust กับ Coq สามารถสร้างคุณค่าได้มากในสาขาเหล่านี้
5. ข้อพิจารณาในการนำเทคโนโลยีมาใช้: เมื่อนำเทคโนโลยีใหม่มาใช้ ควรคำนึงถึงเส้นโค้งการเรียนรู้และความเข้ากันได้กับระบบเดิม เครื่องมือพิสูจน์เชิงรูปนัยอย่าง Coq อาจมีเส้นโค้งการเรียนรู้สูง จึงต้องมีการเตรียมตัวและการฝึกอบรมอย่างเพียงพอ

[GN⁺]

ความคิดเห็นจาก Hacker News

สรุปความคิดเห็นจาก Hacker News

• ความน่าเชื่อถือของเครื่องมือแปลอัตโนมัติ

  • เครื่องมือแปลอัตโนมัติเริ่มได้รับความเชื่อถือ coq-of-rust เขียนด้วย Rust และสามารถแปลงเป็น Coq เพื่อพิสูจน์ความถูกต้องได้ แนวทางนี้คล้ายกับวิธีป้องกันการโจมตีของ Ken Thompson

• ขนาดของโปรแกรมและการพิสูจน์ยืนยัน

  • ขนาดของโปรแกรมที่ตรวจพิสูจน์ด้วยระบบพิสูจน์กึ่งอัตโนมัติอย่าง Coq ยังมีขนาดเล็ก ค่าใช้จ่ายของการรับประกัน 100% อาจสูงกว่าการรับประกัน 99.9999% ถึง 10 เท่า

• ความเป็นไปได้ของข้อผิดพลาดในกระบวนการแปล

  • มีความเป็นไปได้สูงที่จะเกิดข้อผิดพลาดระหว่างกระบวนการแปลงโค้ดเป็น Coq จึงมีข้อสงสัยต่อความสมเหตุสมผลของการพิสูจน์ยืนยันกับโค้ดต้นฉบับ

• โพสต์ที่เกี่ยวข้องกับคริปโตเคอร์เรนซี

  • มีการส่งโพสต์บล็อกที่มีเนื้อหาเกี่ยวกับคริปโตเคอร์เรนซีไม่มากนัก และยังมีโพสต์ที่พูดถึงแนวทางคล้ายกันสำหรับ Python ด้วย

• ข้อจำกัดของการพิสูจน์แบบเป็นทางการ

  • มีผู้ระลึกได้ว่าเคยพบบั๊กในคอมไพเลอร์ C ที่ผ่านการพิสูจน์แบบเป็นทางการแล้ว จึงตั้งคำถามเรื่องความน่าเชื่อถือของตัว Coq เองและกระบวนการแปล

• การพิสูจน์แบบเป็นทางการของ Rust

  • มีคำถามว่าหากไลบรารีพื้นฐานของ Rust ผ่านการพิสูจน์แบบเป็นทางการแล้ว จะทำให้ได้ระดับคุณภาพการพิสูจน์ด้านการจัดการหน่วยความจำ ตราบใดที่ไม่ใช้โค้ดที่ไม่ปลอดภัยหรือไม่

• การเขียนสเปกสำหรับการพิสูจน์แบบเป็นทางการ

  • มีคำถามว่าการเขียนสเปกสำหรับการพิสูจน์แบบเป็นทางการคล้ายกับการเขียน property test ที่ซับซ้อนกว่าหรือไม่ เพราะการเขียน property test นั้นยากและใช้เวลามากอยู่แล้ว

• การเปรียบเทียบกับแนวทางอื่น

  • มีการขอให้เปรียบเทียบความแตกต่างของแนวทางนี้กับ Aeneas หรือ RustHornBelt และสงสัยว่าจัดการกับ pointer และ mutable borrow อย่างไร

• การยอมรับ Rust ในเคอร์เนล

  • มีคำถามว่าความพยายามลักษณะนี้จะช่วยเร่งการยอมรับ Rust ในเคอร์เนลได้หรือไม่

• การเพิ่ม Rust backend ให้ F*

  • มีคำถามว่าการเพิ่ม Rust backend ให้ F* ต้องใช้ความพยายามมากเพียงใด