คุณเขียน Rust ใช่ไหม ดังนั้นต้องรู้จักกับ Creusot สักหน่อย อย่าพลาดของดี

ก่อนจะเข้าเนื้อหาหลัก ขอแอบสปอยนิดนึงว่า… สิ่งที่คุณกำลังจะได้จาก Creusot

คือความสามารถในการ “เขียนเงื่อนไขความถูกต้องของระบบ”
ลงไปในโค้ดของคุณโดยตรง

แล้วให้ Creusot ทำหน้าที่เป็น “ผู้พิสูจน์”

ว่าฟังก์ชันนั้น
ทำงาน “ตรงตามที่คุณระบุไว้” จริงหรือไม่

และถ้าวันหนึ่ง
สิ่งที่โค้ดทำ มันขัดแย้งกับสิ่งที่คุณบอกว่า “ควรจะเป็น”

❌ โค้ดนั้นจะไม่มีวัน build ผ่าน

แต่ก่อนอื่น เพื่อให้เราคุยกันได้ลึกขึ้น ผมอยากปูความเข้าใจเรื่อง macro ใน Rust สักเล็กน้อย

ถ้าคุณเคยเห็นอะไรแบบนี้

#[some_attribute] //<--หมายถึงตรงนี้
fn do_something() { ... }

สิ่งที่อยู่ข้างบนฟังก์ชันพวกนี้ มันไม่ใช่ comment ไม่ใช่ decoration เฉย ๆ

มันคือ “macro”

บางคนจะเรียกมันว่า preprocessor ก็พอได้ (แม้ในเชิงเทคนิค Rust จะไม่ได้ใช้คำนี้ตรง ๆ แบบ C)

แต่ภาพที่ควรนึกคือ

🧠 มันคือ “โปรแกรมเล็ก ๆ” ที่มารันก่อนโค้ดคุณจริง ๆ

ตอนที่คุณสั่ง build

สิ่งที่เกิดขึ้นไม่ใช่ rustc เอาโค้ดคุณไป compile ตรง ๆ ทันที แต่จะมีช่วงหนึ่งที่ macro พวกนี้ถูก execute ก่อนเสมอ

โค้ดที่มี macro กำกับไว้ จะไม่ถูกมองว่าเป็นโค้ดธรรมดาอีกต่อไป

แต่จะถูก “โยนเข้าไปให้ macro จัดการ”

ภาพในหัวของคุณตอนนี้ควรเป็นแบบนี้

1. เริ่มจาก โค้ดของคุณถูกสั่ง build
2. rustc จะ compile ตัว macro ให้กลายเป็นโปรแกรมเล็กๆก่อน
3. จากนั้น โค้ดที่มี macro กำกับ จะถูกส่งเข้าไปให้โปรแกรมเล็กๆพวกนั้น
4. macro จะทำงานกับโค้ดตามที่มันถูกเขียนไว้
5. มันอาจ rewrite โค้ดของคุณ หรือ generate โค้ดใหม่ขึ้นมาโดยที่คุณไม่เห็น (ซ่อนการทำงานไว้เบื้องหลัง)
6. แล้วผลลัพธ์สุดท้าย ถึงจะถูกส่งต่อให้ compiler ทำงานจริง

ซึ่ง macro สามารถทำได้หลายอย่างมาก เช่น

• แก้ไขโค้ดของคุณ (rewrite)

• generate โค้ดเพิ่ม

• ตรวจสอบเงื่อนไขบางอย่าง

• ❗ และมันสามารถ “หยุดการ build” ได้เลย ถ้ามันไม่พอใจ

ตรงนี้แหละคือจุดตั้งต้นที่สำคัญ

เพราะ Creusot ไม่ได้เป็นแค่ library ธรรมดา แต่มัน “ใช้พลังของ macro” เพื่อแทรก logic บางอย่างเข้าไปในโค้ดของคุณ และสิ่งที่มันตรวจสอบ มันลึกกว่าที่ compiler ปกติทำ

งั้นลองดู use case ง่าย ๆ ก่อน แบบที่ไม่ต้องคิดเยอะ แต่เห็นภาพทันที

สมมติว่าเรามีฟังก์ชันแบบนี้

fn plus_one(x: i32) -> i32 {
    x + 1
}

ฟังก์ชั่นนี้ ทำงานง่ายๆ คือรับค่า x แล้วบวก 1 กลับไป

❓ คำถามคือ ฟังก์ชันนี้ “ถูกต้อง” ไหม?

ในมุมของ Rust

• ✅ มัน compile ผ่าน
• ✅ ไม่มี memory issue
• ✅ ไม่มี data race

ทุกอย่างดูโอเคหมด

แต่ลองคิดอีกมุมนึง

ถ้าในระบบของคุณ ค่าที่ส่งเข้ามา

“💥จำเป็นที่จะต้องคิดเผื่อว่า มันต้องไม่ overflow💥” ล่ะ? เพราะสำหรับ i32

ถ้า

x = i32::MAX //ค่าสูงสุดของ i32 คือ 2147483647

//แล้วหากเอามาบวก 1 เข้าไป
x + 1

สิ่งที่ได้… ไม่ใช่ 2147483648

💥💥💥แต่มันคือ overflow💥💥💥

เพราะตัวแปรมันล้น เกินขอบเขตที่มันเก็บได้

ปกติเราอาจจะเขียนกันแบบนี้

fn plus_one(x: i32) -> i32 {
    assert!(x < i32::MAX);
    x + 1
}

ซึ่งก็ช่วยได้ แต่เหมือนเดิม มันตรวจตอน runtime

แต่กับ Creusot คุณสามารถบอกสิ่งที่ “ต้องเป็นจริงก่อนเรียกฟังก์ชัน” ได้ตรง ๆ

#[requires(x < i32::MAX)] // <-- ตรงนี้ ที่อยากให้ดู
fn plus_one(x: i32) -> i32 {
    x + 1
}

✅ นี่ไม่ใช่การ check แต่มันคือการ “ประกาศกติกา” ให้กับ Creusot

และหน้าที่ของ Creusot คือพยายามพิสูจน์ให้ได้ว่า
ฟังก์ชันนี้ ถูกเขียนให้ทำงาน “ตรงตามกติกา” ที่เราระบุไว้จริงหรือไม่

ถ้ามันพิสูจน์แล้วพบว่า
โค้ดของคุณขัดแย้งกับกติกานี้

❌ โค้ดคุณจะ build ไม่ผ่าน

และไม่แค่นั้น Creusot ไม่ได้เช็คแค่ตัวฟังก์ชัน

แต่มันจะ “ไล่ตรวจทั้งโปรแกรม”

เพื่อมองหาว่า
“ทุกจุดที่เรียกฟังก์ชันนี้”

ต้องสามารถพิสูจน์ได้ว่า
เรียกใช้งานมันอย่างถูกต้อง

ถ้าจุดไหนพิสูจน์ไม่ได้
ทั้งโปรแกรมจะไม่ผ่านการ build

คล้าย ๆ Unit Test แต่ลึกกว่า

เพราะมันไม่ใช่แค่การทดสอบผลลัพธ์
แต่มันคือการพิสูจน์ว่า

“โค้ดของคุณ ถูกเขียนให้สอดคล้องกับเงื่อนไขที่คุณระบุไว้จริง”

ถัดมา เรามาบังคับรูปแบบของ Input และ Output กัน

จากตัวอย่างก่อนหน้า

เราบอกไปแล้วว่า
ฟังก์ชันนี้ “รับค่าแบบไหนได้” ด้วย #[requires(...)]

แต่นั่นยังไม่ครบ

เพราะในหลายกรณี
เราไม่ได้อยากคุมแค่ input

เรายังอยาก “บังคับผลลัพธ์” ด้วยว่า
ฟังก์ชันนี้ต้องคืนค่าอะไรออกมา

กลับมาที่ plus_one

ตอนนี้เรามีแบบนี้

#[requires(x < i32::MAX)]
fn plus_one(x: i32) -> i32 {
    x + 1
}

สิ่งที่เราบอกคือ

ห้ามมีใครเรียกฟังก์ชันนี้ด้วยค่าที่จะทำให้ overflow

แต่เรายังไม่ได้บอกว่า

แล้วผลลัพธ์ต้องเป็นอะไร

เราสามารถระบุได้แบบนี้

#[requires(x < i32::MAX)]
#[ensures(result == x + 1)]
fn plus_one(x: i32) -> i32 {
    x + 1
}

ตรง #[ensures(...)]

คือการบอกว่า

หลังจากฟังก์ชันทำงานเสร็จ ค่าที่ return ออกมา จะต้องเท่ากับ x + 1 เท่านั้น หากผิดไปจากนี้ เช่นกรณี overflow จะถูกปัดตกโดยปริยาย

เมื่อมันตรวจทุกแห่งที่เรียกฟังก์ชันนี้ แล้วพบว่ามีจุดใดที่ส่งค่าเข้ามาแล้ว overflow แน่ๆ

❌ มันจะไม่อนุญาตให้ build ผ่าน

สิ่งที่เปลี่ยนไป

ตอนนี้ฟังก์ชันนี้ไม่ได้มีแค่ implementation

แต่มันมี “สัญญา” ครบทั้งสองด้าน

• input ต้องเป็นแบบไหน (requires)
• output ต้องเป็นแบบไหน (ensures)

และสิ่งสำคัญคือ

❗ นี่ไม่ใช่ comment

แต่เป็นสิ่งที่ Creusot จะพยายามพิสูจน์ให้ได้จริง

ลองทำให้มันพังดู

#[requires(x < i32::MAX)]
#[ensures(result == x + 1)]
fn plus_one(x: i32) -> i32 {
    x + 2 // <- เขียนผิด
}

โค้ดนี้ยัง compile ใน Rust ปกติ

แต่สำหรับ Creusot

มันจะพยายามพิสูจน์ว่า

result == x + 1

ซึ่ง “ไม่จริง”

❌ build ไม่ผ่านทันที

นี่แหละคือจุดที่มันเริ่มต่าง

คุณไม่ได้รอให้มี test มาเจอ bug นี้ แต่คุณ “กันมันตั้งแต่ระดับ logic” ตั้งแต่ตอนเขียนโค้ด

ยังไม่จบ คุณกำลังเข้าสู่ความ Advanced ของ Creusot อย่าเพิ่งท้อ 🌸🍑 อ่านต่ออีกนิด

ย้อนกลับไปทำความเข้าใจการทำงานของ Creusot สักนิด ก่อนที่ผมจะท้าทายด้วยโจทย์รูปแบบถัดไป

สิ่งที่ผมอยากให้รู้ไว้คือ

การติดตั้ง Creusot ค่อนข้างซับซ้อน

เพราะมันไม่ได้มีแค่ตัวมันเอง
แต่ต้องติดตั้ง

• Why3
• และ SMT Solvers เพิ่มด้วย

ซึ่งทั้งหมดนี้
คือ “เครื่องมือจริง” ที่อยู่เบื้องหลังการพิสูจน์

โครงสร้างการทำงานของ Creusot

กระบวนการทั้งหมด มันจะไหลเป็นทอด ๆ แบบนี้

1. เขียนโค้ด Rust พร้อมใส่ Logic ลงใน Attribute พิเศษ
2. Creusot จะอ่านโค้ดนั้น แล้วแปลงเป็นภาษา WhyML
3. Why3 (เครื่องมือพิสูจน์) จะรับช่วงต่อ
4. SMT Solvers (เช่น Z3, CVC4) จะพยายาม “หาทางหักล้าง” ตรรกะที่คุณเขียน

ถ้ามัน “หักล้างไม่ได้เลย”

✔️ แปลว่าโค้ดคุณ ถูกต้องตามตรรกะ

ทำไม plus_one ถึงพิสูจน์ได้?

เพราะมันมี “ความสัมพันธ์ที่ชัดเจน”

#[requires(x < i32::MAX)]
#[ensures(result == x + 1)]
fn plus_one(x: i32) -> i32 {
    x + 1
}

สิ่งที่ solver เห็นคือ

• มี input x
• มีเงื่อนไข x < i32::MAX
• มี output = x + 1

ทั้งหมดนี้เชื่อมกันเป็น “สมการ”

มันเลยพิสูจน์ได้

และนี่คือจุดสำคัญมาก

มันไม่ได้ทำงานแบบ Unit Test

มันไม่ได้ “ลองรันโค้ด”

แต่มันกำลัง

วิเคราะห์ความสัมพันธ์ของตรรกะ

เลยทำให้

• Unit Test = เช็คด้วยตัวอย่างบางกรณี
• Creusot = พิสูจน์ทุกกรณี (ถ้าทำได้)

สองอย่างนี้ ไม่ได้แทนกัน แต่ “เสริมกัน”

แล้วคำถามสำคัญ

ถ้ามันเก่งเพราะ “ความสัมพันธ์แบบสมการ”

งั้นกรณีที่มันไม่ใช่สมการล่ะ?

เช่น

• ไม่มีสูตร
• ไม่มี x + y
• ไม่มีความต่อเนื่อง

แต่เป็น logic แบบ “แยกเคส”

ตัวอย่างนะ

เมื่อโจทย์ไม่ใช่แค่สมการ แต่เป็น “เงื่อนไขทางธุรกิจ” แบบแยกเคส

จากตัวอย่าง plus_one เราเห็นการใช้สูตรคณิตศาสตร์ง่าย ๆ อย่าง result == x + 1 แต่ในโลกความเป็นจริง งานของเรามักจะเจอกับ Business Logic ที่ไม่ได้เป็นเส้นตรงแบบนั้น

ลองดูโจทย์นี้ครับ:

สมมติว่าเรามีฟังก์ชันที่คำนวณราคาสินค้า แบบหักส่วนลด ตามระดับสมาชิก

โจทย์: ฟังก์ชันคำนวณราคาสินค้าตามระดับสมาชิก

• Bronze → ลด 5%
• Silver → ลด 12%
• Gold → ลด 20%

ข้อสังเกต: มันไม่มีสูตร x + y ที่ครอบคลุมทุกอย่าง แต่มันคือการ “จับคู่” (Mapping) ระหว่างสถานะกับตัวเลข ซึ่งความสัมพันธ์พวกนี้ไม่มีความต่อเนื่องเชิงคณิตศาสตร์เลย เป็นการกำหนดแบบแยกเคส (Discrete) โดยสิ้นเชิง

วิธีการ “ประกาศกติกา” ใน Creusot

แทนที่เราจะเขียนแค่โค้ด แล้วไปลุ้นเอาใน Unit Test ว่าเราพิมพ์ตัวเลขผิดไหม เราจะใช้ match เข้ามาช่วยร่าง “สัญญา” ใน ensures แบบนี้ครับ

#[requires(price >= 0 && price < 1_000_000)] // กันราคาติดลบและกัน overflow เบื้องต้น
#[ensures(match level {
    MemberLevel::Bronze => result == price * 95 / 100,
    MemberLevel::Silver => result == price * 88 / 100,
    MemberLevel::Gold   => result == price * 80 / 100,
})]
fn apply_discount(price: i32, level: MemberLevel) -> i32 {
    match level {
        MemberLevel::Bronze => price * 95 / 100,
        MemberLevel::Silver => price * 88 / 100,
        MemberLevel::Gold   => price * 80 / 100,
    }
}

นี่คือการ “ล็อคสเปค” ด้วยตรรกะ

การใช้ match ใน ensures คือการบังคับให้ “แผนผังความคิด” ของเรากับ “สิ่งที่คอมพิวเตอร์รัน” ต้องตรงกัน 100%

• ถ้าคุณเขียนโค้ดผิด -> Build ไม่ผ่าน
• ถ้าคุณเขียนสัญญาผิด -> Build ไม่ผ่าน
• ถ้ามีเคสที่หลุดรอดสายตา (Edge Case) -> Build ไม่ผ่าน

มันไม่ใช่แค่การเช็คว่า “รันได้ไหม” แต่มันคือการเช็คว่า “คุณทำตามที่พูดไว้หรือเปล่า”

อ่านมาตอนนี้ สรุปว่าเรารู้จักพวกนี้แล้ว

• requires: คือการคัดกรองแขกที่จะเข้างาน (Input ต้องไม่เละ)
• ensures: คือการเซ็นสัญญาว่าจบงานแล้วลูกค้าต้องได้อะไร (Output ต้องเป๊ะ)
• match: คือการกางเงื่อนไขว่า “ถ้ามาแบบนี้ ต้องจบแบบนั้น”

ซึ่งทั้งหมดนี้ Creusot จะใช้พลังของ SMT Solvers ในการ “กางตรรกะ” ออกมาดูทุกซอกทุกมุม เพื่อยืนยันว่าไม่มีทางเลยที่ผลลัพธ์จะหลุดไปจากกติกานี้

ก่อนจบ ขอตัวอย่างสุดท้าย 👋

เมื่อเงื่อนไขมันยุบยับ เราสามารถมี requires และ ensures ได้หลายตัว เพื่อแยกความรับผิดชอบของแต่ละเงื่อนไขออกจากกันได้นะ

สมมติว่าเราอัปเกรดฟังก์ชันคำนวณส่วนลดเมื่อกี้ ให้มีความเป็น “มืออาชีพ” ขึ้น โดยเพิ่มกฎเหล็กเข้าไปอีก:

1. ต้องมีราคาสินค้า: ราคาห้ามติดลบ และห้ามเกินงบประมาณระบบ (เช่น 1 ล้านบาท)
2. ต้องระบุระดับสมาชิก: ห้ามส่งค่าว่างมา
3. ผลลัพธ์ต้องสมเหตุสมผล: ราคาหลังลด ต้อง “น้อยกว่าหรือเท่ากับ” ราคาเดิมเสมอ (ป้องกันบั๊กที่ลดแล้วราคาดันเพิ่ม!)
4. ต้องตรงตาม Tier: (อันนี้คือ Logic เดิมของเรา)

ลองดูหน้าตาของ “สัญญาหลายบรรทัด” กันครับ

// --- ด่านตรวจขาเข้า (Input Validation) ---
#[requires(price >= 0)]                // 1. ราคาห้ามติดลบ
#[requires(price < 1_000_000)]         // 2. ราคาต้องไม่เว่อร์เกินระบบรับไหว
#[requires(level != MemberLevel::None)] // 3. ต้องเป็นสมาชิกเท่านั้น

// --- สัญญาขาออก (Output Guarantees) ---
#[ensures(result <= price)]            // 4. จบงานแล้ว ราคาต้องไม่แพงกว่าเดิมเด็ดขาด!
#[ensures(result >= 0)]                // 5. จบงานแล้ว ห้ามติดลบ (ไม่มีการแจกเงินคืน)
#[ensures(match level {                // 6. และต้องตรงตามเงื่อนไขเป๊ะๆ
    MemberLevel::Bronze => result == price * 95 / 100,
    MemberLevel::Silver => result == price * 88 / 100,
    MemberLevel::Gold   => result == price * 80 / 100,
    _ => false, // เคสอื่นๆ ที่หลุดมาถือว่าผิดสัญญา
})]
fn apply_professional_discount(price: i32, level: MemberLevel) -> i32 {
    // ... logic ของคุณ ...
}

ทำไมต้องแยกเขียนหลายบรรทัด? เขียนรวมกันไม่ได้เหรอ?

จริง ๆ เราสามารถใช้เครื่องหมาย && (and) เชื่อมยาว ๆ เป็นบรรทัดเดียวได้ครับ แต่การแยกบรรทัดมีข้อดีที่ “โคตรสำคัญ” อยู่ 2 อย่าง:

1. อ่านง่าย (Readability)

ลองนึกภาพคุณกลับมาอ่านโค้ดตัวเองในอีก 3 เดือนข้างหน้า การเห็นเงื่อนไขแยกเป็นข้อ ๆ เหมือน Check-list มันเข้าใจง่ายกว่าการนั่งแกะวงเล็บในสมการยาวเหยียดแน่นอน

2. บอกจุดตายได้แม่นยำ (Error Isolation)

เวลาที่ Creusot พิสูจน์แล้วพบว่าโค้ดคุณ “สอบตก” มันจะบอกได้เลยว่า ตกที่บรรทัดไหน

• ถ้ามันบอกว่าตกตรง #[ensures(result <= price)] คุณจะรู้ทันทีว่า “เฮ้ย! โค้ดเราเขียนอีท่าไหนให้ราคามันเพิ่มขึ้นวะ?”
• มันดีกว่าการที่มันบอกแค่ว่า “เงื่อนไขรวม ๆ ผิดนะ ไปหาเอาเอง”

ยินดีด้วย ตอนนี้คุณได้ใช้ โควต้าการอ่านหนังสือ ครอบคลุมของปีนี้และปีหน้าไปเรียนร้อยแล้ว