moon-certified
Core algorithms and data structures for MoonBit โ partially formally verified
moonbit
formal-verification
moon-prove
algorithms
data-structures
partially-verified
Author
Version
0.1.1
License
Apache-2.0
Repository
Last updated
18 hours ago
Downloads
6
#Moon Certified
็จ MoonBit 0.9 ็ moon prove ๅฝขๅผๅ้ช่ฏ็ณป็ป๏ผๆๅปบ็ป่ฟๆฐๅญฆ่ฏๆ็ๆ ธๅฟ็ฎๆณไธๆฐๆฎ็ปๆๅบใ
#ไธบไปไน้่ฆ่ฟไธช้กน็ฎ
MoonBit 0.9 ๅผๅ
ฅไบ first-class formal verification ่ฝๅ๏ผmoon prove ๆไธบไธ moon buildใmoon test ๅนถๅ็ๅทฅๅ
ท้พๅ
็ฝฎๅฝไปคใๅฎ้่ฟ Why3 + Z3 SMT ๆฑ่งฃๅจ๏ผๅฏนไปฃ็ ่ฟ่กๅ
จ่พๅ
ฅ่ฆ็็ๆญฃ็กฎๆง่ฏๆโโไธๆฏๆต่ฏๆๅ ็ป่พๅ
ฅ็ขฐๅทง่ฟๅๆญฃ็กฎ็ปๆ๏ผ่ๆฏไธไธช่ฆ็ๆๆๅฏ่ฝ่พๅ
ฅ็ๆฐๅญฆ่ฏๆใ
ไฝ็ฎๅ MoonBit ็ๆไธญ๏ผmoonbit-community/verified ไป
ๅ
ๅซ 12 ไธชๆ็จ็บง็คบไพ๏ผv0.0.2๏ผใๆฌ้กน็ฎ็็ฎๆ ๆฏๆๅปบ็ไบง็บง้ช่ฏๅบ๏ผ่ฆ็ๆๅบใๆ็ดขใๆฐๆฎ็ปๆใๅพ็ฎๆณ็ญๆ ธๅฟ้ขๅใ
#้กน็ฎ็ถๆ
0.1.1๏ผ2026-08-27๏ผๅๆญฅ mooncakes.io ไธ GitHub ็่กฅไธ็๏ผ้ฆไธชๆญฃๅผๅๅธไธบ 0.1.0๏ผโ 337 ไธช็ฎๆณๅ
+ ๅ
ฑไบซๅทฅๅ
ทๆจกๅใๅๅธๆถ่ดจ้้จๆง๏ผmoon check --deny-warn 0 errors / 0 warnings๏ผmoon test 6432 ไธชๆต่ฏๅ
จ้จ้่ฟ๏ผmoon fmt --check ๅนฒๅ๏ผmoon prove 17 ไธชๅ
ๅ
จ้จ่ฏๆ้่ฟ๏ผๅ
ถไธญ 9 ไธชไธบ Verified tier๏ผใ
็จณๅฎๆงๅๅฑ๏ผ่ฏฆ่ง docs/API_STABILITY.md๏ผ๏ผ
| ๅฑ็บง | ๅ ๆฐ | ่ฏดๆ |
|---|---|---|
| Verified | 9 | proof-enabled = true๏ผmoon prove๏ผWhy3 + Z3๏ผ้่ฟ |
| Stable | 254 | ๅฎๆดๆต่ฏ่ฆ็๏ผไธป็ๆฌๅ API ๅป็ป |
| Experimental | 74 | ๆญฃ็กฎ๏ผๆต่ฏๅ จ่ฟ๏ผไฝ API ๆชๅป็ป๏ผๅฐ็ๆฌๅฏ่ฝๅๆด |
#ๅ่ฝๆฆ่ง
- 337 ไธช็ฎๆณๅ
๏ผ่ฆ็ๆ ธๅฟ็ฎๆณๅ
จ้ขๅ๏ผ
- ๅนถๅๆฐๆฎ็ปๆ๏ผRingBufferใBoundedQueueใSnapshotMap (COW ๅฟซ็ ง) โ Michael-Scott/Vyukov/Treiber ็ญๅนถๅ็ฎๆณ็ๅ็บฟ็จๆจกๆ (MoonBit ็ผ่ฏ่ณ Wasm/JS, ๆ ๅ็ CAS; ่ชๆ้ๆไพ็ๅฎไบๆฅ)
- ๆไน ๅ/ๅค้จ็ฎๆณ๏ผExternal SortใLSM-TreeใB+TreeใPersistent VectorใHAMT
- ๅญ็ฌฆไธฒ้ซ็บง็ปๆ๏ผSuffix TreeใFM-IndexใWavelet TreeใPalindromic TreeใLyndon ๅ่งฃใSuffix Balanced Tree
- ๅพ้ซ็บง็ฎๆณ๏ผEdmonds Blossom (ไธ่ฌๅพๆๅคงๅน้ )ใDominator TreeใGomory-Hu TreeใStoer-Wagner ๅ จๅฑๆๅฐๅฒใHLPP ๆๅคงๆตใHopcroft-KarpใMin Steiner TreeใHLDใ้ๅฟๅ่งฃใ่ๆ ใๆๅคงๅข (Bron-Kerbosch)ใๅพ็่ฒใไธ็้ๅถๆต
- ๅ ไฝ่ฟ้ถ๏ผ3D ๅธๅ ใVoronoi ๅพใDelaunay ไธ่งๅๅใๅๅนณ้ขไบคใๅจๆๅธๅ
- ๆฐๅญฆ/ๆฐๅผ๏ผFFT (ๅคๆฐ)ใๅ็บฏๅฝขๆณ (LP)ใLU/QR/SVD ๅ่งฃใ็นๅพๅผใNewton ่ฟญไปฃใBerlekamp-Masseyใๅ ฑ่ฝญๆขฏๅบฆๆณใGMRESใL-BFGSใ่ชๅจๅพฎๅ
- ๆฆ็/่ฟไผผ็ปๆ๏ผCount-Min SketchใHyperLogLogใCuckoo FilterใW-TinyLFUใTTL Cache
- ๆฐ่ฎบ่ฟ้ถ๏ผไบๆฌกๅฉไฝใๅๆ นใMรถbius ๅๆผใๆ้ๅใReed-Solomon ็ผ็ ใๅค้กนๅผ่ฟ็ฎ
- DP ่ฟ้ถ๏ผๆฐไฝ DPใ็ถๅ DPใๅธๅฃณๆๅทง (CHT)ใๅๆฒป DPใKnuth ไผๅใSOS DP
- ๆ็ดข/ML ๅบ็ก๏ผBall-TreeใVP-TreeใLSHใTernary Search
- ๅ ถไป๏ผNim ๅๅผ (Sprague-Grundy)ใๆฐดๅบ้ๆ ทใๅ ๆ้ๆบ้ๆ ทใCRCใMo ็ฎๆณใๆ่ถ ๆ ใไบ็ปดๆ ็ถๆฐ็ปใSegment Tree BeatsใExternal Sort
- ็ไบง็บง่ฎพ่ฎก๏ผ
- ๆๆ้ญๆฏๅผๆถ้ค๏ผไฝฟ็จ Option/SPResult ็ฑปๅๆฟไปฃ -1/็ฉบๆฐ็ป็ญๆญงไน่ฟๅๅผ
- ๅ ณ้ฎ็ฎๆณไฝฟ็จ Int64 ๆบขๅบไฟๆค๏ผdijkstra_heapใconvex_hullใmax_flowใdinicใmin_cost_flow ็ญ๏ผ
- ่ชๅนณ่กกๆ ๏ผAVLใ็บข้ปๆ ใBTreeใTreap๏ผไพ่ต็ปๆไธๅ้ไฟ่ฏ O(log n) ้ๅฝๆทฑๅบฆ๏ผๆ ้ไบบไธบๆทฑๅบฆ้ๅถ
- swap ้ไธญๅจ @utils๏ผๆถ้ค 7 ๅค้ๅค๏ผ
- SplitMix64/XorShift64 ้ไธญๅจ @utils/prng๏ผๆถ้คๅคๅ ้ๅค๏ผ
- ๆฏๅฎไพ้ๆบ็งๅญ @utils.fresh_seed()๏ผๆฟไปฃๅ จๅฑๅบๅฎ็งๅญ๏ผ
- ๆต่ฏ/้ช่ฏๅบ็ก่ฎพๆฝ๏ผ
- benchmarks/ ็ฎๅฝ๏ผๆง่ฝๅบๅๆต่ฏ๏ผๅซๆๅบ/ๆ /ๅพ/ๆฐ่ฎบ/ๅญ็ฌฆไธฒ/ๅ ไฝ็ wall-clock ๆถ้ดๆต้ไธๅคๆๅบฆ้ช่ฏ
- test/fuzz/ ็ฎๅฝ๏ผFuzz ๆต่ฏ + ๅฏนๆๆง่พๅ ฅๆต่ฏ๏ผๆๅบๆๅๆ ๅตใๅพ่ช็ฏ/ๆญๅผ/็ฏๆฃๆตใๅญ็ฌฆไธฒ UnicodeใCarmichael ๆฐใๅ ไฝๅ ฑ็บฟ/้ๅค็นใๅนถๅ็ปๆ่พน็๏ผ
- test/stress/ ๅขๅผบ๏ผๆๅบๅๅๆต่ฏ้ช่ฏ็ฝฎๆขๆง่ดจ๏ผ้ไป ๆๅบๆง๏ผ๏ผLIS ๅๅๆต่ฏ้ๆๅฎ้ ๅญๅบๅ้ช่ฏ๏ผ้ไป ๅนณๅก่พน็๏ผ
- test/property_test/ QuickCheck ้ฃๆ ผๅฑๆงๆต่ฏๆกๆถ๏ผ้ๆบ่พๅ ฅ็ๆ + ๅไพ็ผฉๅ๏ผ
- test/test_utils/ ๅ ฑไบซๆต่ฏๅทฅๅ ท๏ผๆถ้ค 14 ไธชๆไปถ็ str_cmp ้ๅค๏ผ
- docs/API_STABILITY.md API ็จณๅฎๆง็ญ็ฅ
- ็ฎๆณๅฎ็ฐ็ญ็ฅ๏ผ
- ๆๅฐ่ดน็จๆๅคงๆต๏ผSuccessive Shortest Paths with Potentials๏ผ้ฆ่ฟญไปฃ SPFA + ๅ็ปญ Dijkstra๏ผ๏ผๅคๆๅบฆ O(VยทE + FยทE log V)
- prim/segment_tree/fenwick/kruskal๏ผๆไพ checked ๅไฝ (Int64 ๆบขๅบๆฃๆต)
- miller_rabin๏ผ็กฎๅฎๆง 12 ่ง่ฏ้ {2,3,5,7,...,37}๏ผ่ฆ็ๅ จ Int64 ่ๅด๏ผSorenson & Webster 2015๏ผ
- euler_sieve๏ผ่ฟๅ None ่้ abort๏ผไธๅ จๅบ Option ็ญ็ฅไธ่ด
- andrew_hull cmp_point๏ผInt64 ๅๆณ้ฒๆบขๅบ๏ผไธ closest_pair ไธ่ด
#้ช่ฏ็ถๆ
#้ช่ฏๆทฑๅบฆๅ็บง
| ็บงๅซ | ๅ | ้ช่ฏๅ ๅฎน | ||
|---|---|---|---|---|
| โ ๅฎๆดๆญฃ็กฎๆง | binary_search | ๆพๅฐๅ่ฟๅๆญฃ็กฎ็ดขๅผ๏ผๆชๆพๅฐ่ฟๅ None | ||
| โ ๅฎๆดๆญฃ็กฎๆง | linear_search | ่ฟๅๆญฃ็กฎ็ดขๅผๆ None | ||
| โ ๅฎๆดๆญฃ็กฎๆง | max_element | ่ฟๅ็็ดขๅผๆๅๆๅคงๅ ็ด | ||
| โ ๅฎๆดๆญฃ็กฎๆง | min_element | ่ฟๅ็็ดขๅผๆๅๆๅฐๅ ็ด | ||
| โ ๅฎๆดๆญฃ็กฎๆง | is_sorted | ่ฟๅ true ๆถๆฐ็ปๆๅบ๏ผ่ฟๅ false ๆถๅญๅจ้ๅบๅฏน | ||
| ๐ถ ๅขๅผบ้ช่ฏ | array_sum | ้่ดๆง + ๆ็ๆฑๅ [nยทlo, nยทhi] + ๅๅๆฐ็ป็ฒพ็กฎ็ญๅผ nยทval | ||
| ๐ถ ๅขๅผบ้ช่ฏ | gcd | ้่ดๆง + ๆด้ค่ชๅๆง d | d + ้ถๆด้คๆง d | 0 |
| ๐ถ ๅขๅผบ้ช่ฏ | fast_power | ้่ดๆง + baseโฅ1 ๆถ resultโฅ1 + baseโฅ1 expโฅ1 ๆถ resultโฅbase | ||
| โ ๏ธ ้จๅ้ช่ฏ | dijkstra | ๆฐ็ป่พน็ + ็ปๆ้ฟๅบฆ๏ผๆ็ญ่ทฏๅพๆไผๆงๆช้ช่ฏ๏ผๅ ฌ็ๅผ็ๅทฒ่ฏๅฎๆ ๆณจ๏ผ | ||
| โ ๏ธ ้จๅ้ช่ฏ | binary_heap | ็ดขๅผ่พน็ (parent/left/right child) | ||
| โ ๏ธ ้จๅ้ช่ฏ | bitset | ๅฎน้้่ด | ||
| โ ๏ธ ้จๅ้ช่ฏ | union_find | self_parent ๅๅงๅๆญฃ็กฎๆง | ||
| โ ๏ธ ้จๅ้ช่ฏ | red_black_tree | empty() ่ฟๅ็ฉบๆ ใsize() ็ปๆ็ญๅผ๏ผ็ผๅญๅญๆฎต้่ดๆง็ฑๆ้ ไฟ่ฏ๏ผไธๅจ่ฏๆ่ๅด๏ผ | ||
| โ ๏ธ ้จๅ้ช่ฏ | kruskal | MST ่พนๆฐ โค n-1 | ||
| โ ๏ธ ้จๅ้ช่ฏ | topological_sort | edge_index ้่ดๆง๏ผไธ็ไธบ้็บฟๆง็ฎๆฏ๏ผ็ฑๆต่ฏ่ฆ็๏ผๆชๅฃฐๆไธบๅทฒ่ฏ๏ผ | ||
| โ ๏ธ ้จๅ้ช่ฏ | kmp | LPS ๆฐ็ป้ฟๅบฆ == pattern ้ฟๅบฆ | ||
| โ ๏ธ ้จๅ้ช่ฏ | combinatorics | ้ถไน็ปๆ โฅ 1 | ||
| โ ๏ธ ้จๅ้ช่ฏ | matrix | identity_int ้ฟๅบฆ nยฒ + transpose_int ้ฟๅบฆ nยทm๏ผ็ดขๅผ่พน็ไฝฟ็จ่ฏๅฎๆ ๆณจ็ๅ ฌ็ๅผ็๏ผ | ||
| โ ๏ธ ้จๅ้ช่ฏ | insertion_sort | nโค1 ๆถ sorted_asc vacuously true | ||
| โ ๏ธ ้จๅ้ช่ฏ | merge_sort | nโค1 ๆถ sorted_asc vacuously true |
้่ฆ่ฏดๆ๏ผ
- โ ๅฎๆดๆญฃ็กฎๆง๏ผZ3 ่ฏๆไบ็ฎๆณ็ๆ ธๅฟๆญฃ็กฎๆง๏ผๆพๅฐๆญฃ็กฎ็ปๆๆๆญฃ็กฎๅคๆญๆๅบๆง๏ผ
- ๐ถ ๅขๅผบ้ช่ฏ๏ผๅจ้จๅ้ช่ฏๅบ็กไธ๏ผๆฐๅขไบๆดๅผบ็ๆง่ดจ้ช่ฏ๏ผๅฆ็ฒพ็กฎ็ญๅผใๅ่ฐๆงใๆด้คๆง็ญ๏ผ
- โ ๏ธ ้จๅ้ช่ฏ๏ผZ3 ่ฏๆไบ้จๅๆง่ดจ๏ผ้่ดๆงใ่พน็ๅฎๅ จ๏ผ๏ผไฝๅฎๆดๆญฃ็กฎๆง้่ฆ้็บฟๆง็ฎๆฏๆจ็๏ผ่ถ ๅบ Z3 ่ชๅจ่ฏๆ่ฝๅ
- proof_axiomatized ๅผ็ graph_index_bound๏ผdijkstra ไธญไฝฟ็จ๏ผๆฏไธไธชๆฐๅญฆไธๆญฃ็กฎไฝ่ขซๅ่ฎพ่้่ฏๆ็้็บฟๆง็ฎๆฏไบๅฎ๏ผๆถๅไธคไธชๅ้็ธไน u * n๏ผZ3 ็บฟๆง็ฎๆฏๆฑ่งฃๅจๆ ๆณ่ชๅจ่ฏๆ๏ผใไฟ็ๆญคๅ ฌ็ๆฏไธบไบ่ฎฉ Z3 ่ฝ้ช่ฏๅฎๅๆ่ฝๅ็้จๅโโๆฐ็ป้ฟๅบฆๅฑๆง result.length() == n
- ๆณๅ็ๆฌๅๆชๅฝขๅผๅ้ช่ฏ๏ผ่กจไธญๆ ๆณจ"โ verified + generic"็ๅ ๏ผๅ ถ โ ไป ๆๅทฒ้ช่ฏ็ Int ็ๆฌ๏ผๆณๅไผด้ๅฝๆฐ๏ผsearch_generic[T] ็ญ๏ผไธๅ้ช่ฏ๏ผๆณจ้ไธญๆ็กฎๆ ๆณจ
- ๆๆ"้จๅ้ช่ฏ"ๅ"ไป ๆต่ฏ้ช่ฏ"็ๅ ้ฝ้่ฟ่ฏฆๅฐฝ็ๆต่ฏๅฅไปถ้ช่ฏๆญฃ็กฎๆง๏ผๅ ๆฌ่พน็ๆ ๅตๅ้ๆบ่พๅ ฅ
#ๆบขๅบ่ฏดๆ
ๅฝขๅผๅ้ช่ฏๅฐ Int ๅปบๆจกไธบๆฐๅญฆๆดๆฐ๏ผไฝ่ฟ่กๆถ Int ๆฏ 32 ไฝๆ็ฌฆๅทๆดๆฐใไปฅไธๅฝๆฐๅจ็ปๆ่ถ
ๅบ 2ยณยนโ1 ๆถไผๅ็้้ปๆบขๅบ๏ผ
| ๅฝๆฐ | ๆบขๅบ่กไธบ | ๅฎๅ จๆฟไปฃ |
|---|---|---|
| fast_power | ็ปๆๅฏ่ฝๅไธบ่ดๆฐ | fast_power_checked๏ผ่ฟๅ Int?๏ผๅทฒไฟฎๅคๆบขๅบๆฃๆต๏ผ |
| gcd | ่พๅ ฅๅฎๅ จ๏ผInt::MIN ไฝฟ็จ Int64 ็ฒพ็กฎ่ฎก็ฎ๏ผไป gcd(Int::MIN,Int::MIN) ้ณไฝ่ณ Int::MAX๏ผ | โ |
| array_sum | ๅคงๆฐ็ปๆฑๅๅฏ่ฝๆบขๅบ | ่ฐ็จ่ ้็กฎไฟๅไธๆบขๅบ |
| sieve | n > 10โท ๆถ่ฟๅ None๏ผOOM ไฟๆค๏ผ | ่ฟๅ FixedArray[Int]? |
| dijkstra_heap | ่ท็ฆปไฝฟ็จ Int64 ็ดฏ็งฏ๏ผๆบขๅบๆถ่ฟๅ None | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค |
| convex_hull | ๅ็งฏไฝฟ็จ Int64 ่ฎก็ฎ | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค |
| max_flow | total_flow ไฝฟ็จ Int64 ็ดฏ็งฏ๏ผ่ฟๅ Int64? ๅบๅๆ ๆ่พๅ ฅ | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค |
| knapsack | n ร capacity > 10โท ๆถ่ฟๅ None | ๅทฒๆทปๅ OOM ไฟๆค |
| lcs | n ร m > 10โท ๆถ่ฟๅ None | ่ฟๅ Int?๏ผๆปๅจๆฐ็ปไผๅ O(min(n,m)) ็ฉบ้ด |
| edit_distance | n ร m > 10โท ๆถ่ฟๅ None | ่ฟๅ Int?๏ผๆปๅจๆฐ็ปไผๅ O(min(n,m)) ็ฉบ้ด |
| counting_sort | ่ดๅผๆ k > 10โท ๆถ่ฟๅ None | ่ฟๅ FixedArray[Int]? |
| pollard_rho | ๅคฑ่ดฅ๏ผ็ด ๆฐๆๆ ๆณๅ่งฃ๏ผๆถ่ฟๅ None | ่ฟๅ Int?๏ผไธ็ด ๆฐ็ปๆๅฏๅบๅ |
| prim | total_weight ็ดฏๅ ไฝฟ็จ Int64 ้ฒๆบขๅบ | prim_mst ่ฟๅ (FixedArray[Int], Int64) |
| segment_tree | ๅบ้ดๅๅฏ่ฝๆบขๅบ Int32 | ๆๆกฃๅทฒๆ ๆณจ๏ผSegmentTree64 ๆไพ checked ๅไฝ่ฟๅ Int? |
| fenwick | ๅ็ผๅๅฏ่ฝๆบขๅบ Int32 | ๆๆกฃๅทฒๆ ๆณจ๏ผFenwick64 ๆไพ checked ๅไฝ่ฟๅ Int? |
| kruskal | total_weight ๅฏ่ฝๆบขๅบ Int32 | ๆๆกฃๅทฒๆ ๆณจ๏ผkruskal_mst_checked ่ฟๅ (FixedArray[Edge], Int64)? |
| min_cost_flow | total_flow/total_cost ไฝฟ็จ Int64 ็ดฏ็งฏ๏ผ่ฟๅ (Int64,Int64)? | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค + ่ด็ฏๆฃๆต |
| dinic | ๆๆๅฎน้ๅๆต้ไฝฟ็จ Int64๏ผ่ฟๅ Int64? | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค + ่ฟญไปฃ DFS |
| interpolation_search | ๅๆณไฝฟ็จ Int64 ้ฒๆญข่ทจ Int32 ่ๅดๆบขๅบ | ๅทฒๆทปๅ ๆบขๅบ้ฒๆค |
| gcd64 | ๆญฃ็กฎๅค็ Int64::MIN๏ผไธๅ้ขๅ ๅ็ปๅฏนๅผ๏ผ | ๅทฒไฟฎๅค |
| is_prime64 | ่ง่ฏ้ๆฉๅฑๅฐๅ จ Int64 ่ๅด๏ผSorenson & Webster 2015๏ผ | ๅทฒไฟฎๅค |
| array_sum | array_sum_checked ่ฟๅ Int?๏ผๆบขๅบ่ฟๅ None๏ผ | ๅทฒๆทปๅ ๅฎๅ จ็ๆฌ |
| matrix | matmul_int_checked ่ฟๅ FixedArray[Int]?๏ผๆบขๅบ่ฟๅ None๏ผ | ๅทฒๆทปๅ ๅฎๅ จ็ๆฌ |
| combinatorics | binomial ๅ ไนๅ้ค๏ผInt64 ไธญ้ด๏ผ๏ผstirling2 ้ขๆฃๆฅๆบขๅบ | ๅทฒไฟฎๅค |
| rolling_hash | ๅๆจกๆฐๅๅธไฝฟ็จ Int64 ไธญ้ด่ฟ็ฎ๏ผๅคงๅญ็ฌฆไธฒไปๅฏ่ฝๆบขๅบ | ๆๆกฃๅทฒๆ ๆณจ๏ผ่ฐ็จ่ ้ๆณจๆ |
| matrix_decomp | ไฝฟ็จ Double ๆตฎ็น่ฟ็ฎ๏ผๆ ๆดๆฐๆบขๅบ้ฃ้ฉ | ๆตฎ็น็ฒพๅบฆ้ๅถ |
| newton_method | ไฝฟ็จ Double ๆตฎ็น่ฟ็ฎ๏ผๆ ๆดๆฐๆบขๅบ้ฃ้ฉ | ๆตฎ็น็ฒพๅบฆ้ๅถ |
#ๆณๅๆถๆ
| ๅ | ๆณๅๆฏๆ | ่ฏดๆ |
|---|---|---|
| insertion_sort | โ FixedArray[T] + cmp | ๅฎๅ จๆณๅ๏ผๆฏๆไปปๆ็ฑปๅ |
| selection_sort | โ FixedArray[T] + cmp | ๅฎๅ จๆณๅ๏ผๆฏๆไปปๆ็ฑปๅ |
| merge_sort | โ FixedArray[T] + cmp | ๅฎๅ จๆณๅ๏ผๆฏๆไปปๆ็ฑปๅ |
| quick_sort | โ FixedArray[T] + cmp | ๅฎๅ จๆณๅ๏ผไธๅไธญ pivot |
| binary_search | โ verified (Int) + generic (unverified) | ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌ + search_generic[T] |
| linear_search | โ verified (Int) + generic (unverified) | ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌ + search_generic[T] |
| max_element | โ verified (Int) + generic (unverified) | ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌ + max_element_generic[T] |
| min_element | โ verified (Int) + generic (unverified) | ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌ + min_element_generic[T] |
| is_sorted | โ verified (Int) + generic (unverified) | ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌ + is_sorted_generic[T] |
| bound_search | โ FixedArray[T] + cmp | lower_bound, upper_bound, binary_search_generic |
| red_black_tree | โ RBNode[T] + cmp | Okasaki ๆๅ ฅ + Kahrs ๅ ้ค |
| binary_heap | โ comparator + Heap ๅฐ่ฃ | min-heap/max-heap ้่ฟ should_swap ็ปไธ |
| hash_table | โ HashTable[K, V] ๆณๅ | ๅผๆพๅฏปๅ + ็บฟๆงๆขๆต๏ผๅซ StringHashTable ๅฐ่ฃ |
| trie | โ String | ๅซ size/enumerate/longest_prefix |
ๆฏ่พๅจ็บฆๅฎ๏ผcmp(a, b) ่ฟๅ่ดๆฐ่กจ็คบ a < b๏ผ0 ่กจ็คบ็ธ็ญ๏ผๆญฃๆฐ่กจ็คบ a > bใ
#็ฑปๅๅฎๅ จ้่ฏฏๅค็
| ๅ | ๆง่ฟๅๅผ | ๆฐ่ฟๅๅผ | ่ฏดๆ |
|---|---|---|---|
| bellman_ford | ็ฉบๆฐ็ป/-1 | SPResult? | None=ๆ ๆ่พๅ ฅ, NegativeCycle=่ด็ฏ, Distances(FixedArray[Int?])=่ท็ฆป |
| floyd_warshall | ็ฉบๆฐ็ป/-1 | SPResult? | ๅไธ๏ผDistances ๅ ๅซ n*n ็ฉ้ต |
| topological_sort | ็ฉบๆฐ็ป | FixedArray[Int]? | None=็ฏๆๆ ๆ่พๅ ฅ |
| dijkstra | FixedArray[Int] (-1=ไธๅฏ่พพ) | FixedArray[Int?] | None=ไธๅฏ่พพ |
| shortest_path | -1 | Int? | None=ไธๅฏ่พพๆๆ ๆ |
| bfs_distances | ็ฉบๆฐ็ป | FixedArray[Int]? | None=ๆ ๆ่พๅ ฅ๏ผ-1 ไฟ็ไธบไธๅฏ่พพๆ ่ฎฐ๏ผBFS ่ทณๆฐ โฅ 0๏ผ |
| bound_search | -1 (็ฉบๆฐ็ป) | 0 | ็ฉบๆฐ็ป่ฟๅ 0๏ผ= ๆฐ็ป้ฟๅบฆ๏ผ๏ผ่ฏญไนไธ่ด |
| mod_inverse | -1 (ๆ ้ๅ ) | Int? | None=ๆ ้ๅ ๆๆ ๆ่พๅ ฅ |
| union_find find | -1 (่ถ็) | Int? | None=่ถ็ |
SPResult ๆไธพๅฎไน๏ผ
pub enum SPResult {
Distances(FixedArray[Int?]) // Some(d)=ๅฏ่พพ, None=ไธๅฏ่พพ
NegativeCycle // ๆฃๆตๅฐ่ด็ฏ
}#ไฝฟ็จๆนๅผ
#็ฏๅข่ฆๆฑ
#่ฟ่ก
# ๅ
้ไปๅบ
git clone https://github.com/Juwan-Hwang/moon-certified.git
cd moon-certified
# ็ฑปๅๆฃๆฅ
moon check
# ่ฟ่กๆต่ฏ (6432 tests)
moon test
# ่ฟ่กๅฝขๅผๅ้ช่ฏ (้่ฆ Why3 1.7.2 + Z3 4.12.x)
moon prove#ๅจ้กน็ฎไธญไฝฟ็จ
ๅ
ๅทฒๅๅธๅฐ mooncakes.io๏ผ
moon add Juwan-Hwang/moon-certifiedfn main {
// Binary search (verified)
let xs = FixedArray::makei(10, fn(i) { i })
let result = @binary_search.search(xs, 5)
println(result) // Some(5)
// Generic binary search with custom comparator
let words = FixedArray::make(4, "")
words[0] = "apple"; words[1] = "banana"; words[2] = "cherry"; words[3] = "date"
let str_cmp = fn(a : String, b : String) -> Int {
let la = a.length(); let lb = b.length()
let min = if la < lb { la } else { lb }
for k = 0; k < min; k = k + 1 {
let c = a[k].to_int() - b[k].to_int()
if c != 0 { return c }
}
la - lb
}
let idx = @binary_search.search_generic(words, "cherry", str_cmp)
println(idx) // Some(2)
// Generic sorting with comparator
let arr = FixedArray::makei(5, fn(i) { 5 - i })
@insertion_sort.insertion_sort(arr, fn(a, b) { a - b })
println(arr) // [1, 2, 3, 4, 5]
// Bellman-Ford with type-safe error handling
let graph = FixedArray::make(9, 0)
graph[0 * 3 + 1] = 4; graph[0 * 3 + 2] = 5; graph[1 * 3 + 2] = -3
match @advanced.bellman_ford(graph, 3, 0) {
Some(Distances(dist)) => println(dist[2]) // Some(1)
Some(NegativeCycle) => println("negative cycle!")
None => println("invalid input")
}
// Red-Black Tree (Okasaki insertion + Kahrs deletion)
let tree : @red_black_tree.RBNode[String] = @red_black_tree.empty()
let tree = @red_black_tree.insert(tree, "hello", str_cmp)
let tree = @red_black_tree.delete(tree, "hello", str_cmp)
println(@red_black_tree.search(tree, "hello", str_cmp)) // false
// KMP string matching
let pos = @kmp.kmp_search("hello world", "world")
println(pos) // Some(6)
// Fenwick Tree (Binary Indexed Tree)
let arr = FixedArray::makei(10, fn(i) { i + 1 })
let ft = @fenwick.build(arr)
println(@fenwick.query(ft, 5)) // 15 (1+2+3+4+5)
// Hash Table (encapsulated)
let ht = @hash_table.hashtable_new_default(16)
@hash_table.hashtable_insert(ht, "key", 42)
println(@hash_table.hashtable_get(ht, "key")) // Some(42)
// Binary Heap (encapsulated)
let h = @binary_heap.heap_new(20)
h.heap_push(5)
h.heap_push(3)
h.heap_push(7)
println(h.heap_pop()) // Some(3)
// Topological Sort (returns Option)
let dag = FixedArray::make(9, 0)
dag[0 * 3 + 1] = 1; dag[1 * 3 + 2] = 1
match @topological_sort.topo_sort(dag, 3) {
Some(order) => println(order) // [0, 1, 2]
None => println("cycle detected")
}
// Dijkstra (returns FixedArray[Int?])
let n = 3
let g = FixedArray::make(n * n, 0)
g[0 * n + 1] = 2; g[1 * n + 2] = 3
let dist = @dijkstra.dijkstra(g, n, 0)
println(dist[2]) // Some(5)
// Fast power with overflow check
match @fast_power.fast_power_checked(2, 30) {
Some(r) => println(r) // 1073741824
None => println("overflow!")
}
// Union-Find (find returns Int?)
let uf = @union_find.new(5)
let _ = @union_find.union(uf, 0, 1)
println(@union_find.find(uf, 0)) // Some(0) or Some(1)
println(@union_find.find(uf, 99)) // None (out of range)
}#ๆๆฏๅ็
ๆฏไธช้ช่ฏ็ฎๆณๅ
ๅซไธค็ฑปๆไปถ๏ผ
| ๆไปถ | ๅ ๅฎน |
|---|---|
| .mbt | ๅฏๆง่กไปฃ็ + ๅฅ็บฆ (proof_require/proof_ensure) + ๅพช็ฏไธๅ้ (proof_invariant) |
| .mbtp | ้ป่พ่ฐ่ฏๅฎไนๅๅผ็ |
้ช่ฏๆต็จ๏ผ
.mbt + .mbtp โ moonc prove โ Why3 + Z3
ๆบไปฃ็ + ่ฐ่ฏ ็ๆ WhyML ่ฏๆๆๆ็ฎๆ #้ช่ฏ็ญ็ฅ
- for ็ดฏๅ ๅจๆจกๅผๆฟไปฃ let mut๏ผDijkstra ็ find-min ๅพช็ฏไฝฟ็จ็ดฏๅ ๅจๆจกๅผ๏ผไฝฟ Z3 ่ฝ้่ฟๅพช็ฏไธๅ้่ฟฝ่ธชๅ้่พน็
- proof_axiomatized ๅผ็๏ผ่ฏๅฎๆ ๆณจ๏ผ๏ผdijkstra ็ graph_index_bound ๆฏๅฏไธ็ๅ ฌ็ๅผ็ใๅฎๅ่ฎพไธไธชๆถๅไธคๅ้็ธไน๏ผu * n๏ผ็้็บฟๆง็ฎๆฏไบๅฎใZ3 ็บฟๆง็ฎๆฏๆฑ่งฃๅจๆ ๆณ่ฏๆ้็บฟๆงไบๅฎ๏ผๅ ๆญค่ฏฅๅผ็่ขซๅ่ฎพ่้่ฏๆใๆฐๅญฆไธๆญฃ็กฎ๏ผu*n + v < n*n <= len๏ผ๏ผไฝๆช้่ฟ Z3 ้ช่ฏใไฟ็ๆญคๅ ฌ็็ๆถ็๏ผZ3 ่ฝ้ช่ฏๆฐ็ป้ฟๅบฆๅฑๆง result.length() == n
- ๅๆฒป้ช่ฏ๏ผๅฐๅฏ้ช่ฏ้จๅ๏ผ่พน็ใ็ปๆญขๆงใๆฐ็ป้ฟๅบฆ๏ผไธไธๅฏ้ช่ฏ้จๅ๏ผ้ๅไธๅ้ไฟๆใๆ็ญ่ทฏๅพๆไผๆง๏ผๅ็ฆป
- ่พๅ ฅๆ ก้ช๏ผๆๆๅฏๅคฑ่ดฅๆไฝๅๅ่พๅ ฅๆ ก้ช๏ผไฝฟ็จ Option/SPResult ่้้ญๆฏๅผ
- comparator ๅๆฐๅ๏ผbinary_heap ็ sift ๆไฝ้่ฟ should_swap ๅฝๆฐๅๆฐ็ปไธไบ min-heap ๅ max-heap ๅฎ็ฐ
- ๅทฒ้ช่ฏ + ๆณๅๅๅฑๆถๆ๏ผๆ็ดขๅ ไฟ็ๅทฒ้ช่ฏ Int ็ๆฌไฝไธบๆญฃ็กฎๆงๅ่๏ผๆณๅ็ๆฌๆฉๅฑๅฐไปปๆ็ฑปๅใๆณจๆ๏ผๆณๅ็ๆฌๆฌ่บซไธๅๅฝขๅผๅ้ช่ฏ๏ผไป ้่ฟๆต่ฏ้ช่ฏ
#MoonBit String ๆฏ่พๆณจๆไบ้กน
MoonBit ็ String ๅ Bytes ็ฑปๅ็ Compare trait ไฝฟ็จ็ญ่ฏๅ
ธๅบ๏ผshortlex order๏ผ๏ผๅ
ๆฏ่พ้ฟๅบฆ๏ผ้ฟๅบฆ็ญ็ๆดๅฐใ่ฟไธๆ ๅ็ๅญๅ
ธๅบไธๅใ
ไพๅฆ๏ผ"date" < "apple" ๅจ MoonBit ไธญไธบ true๏ผๅ ไธบ "date" ้ฟๅบฆไธบ 4๏ผ"apple" ้ฟๅบฆไธบ 5ใ
ๆฌ้กน็ฎๅจ้่ฆๆ ๅๅญๅ
ธๅบ็ๅบๆฏ๏ผ็บข้ปๆ ใไบๅๆฅๆพใๆๅบ็ String ๆต่ฏ๏ผไธญไฝฟ็จ่ชๅฎไน็้ๅญ่ๆฏ่พๅจ๏ผ
let str_cmp = fn(a : String, b : String) -> Int {
let la = a.length(); let lb = b.length()
let min = if la < lb { la } else { lb }
for k = 0; k < min; k = k + 1 {
let ca = a[k].to_int(); let cb = b[k].to_int()
if ca < cb { return -1 }
if ca > cb { return 1 }
}
la - lb
}#้กน็ฎ็ปๆ
moon-certified/
โโโ search/
โ โโโ binary_search/ โ
ไบๅๆฅๆพ (verified Int) + generic (unverified)
โ โโโ bound_search/ ๐ lower_bound/upper_bound (generic)
โ โโโ linear_search/ โ
็บฟๆงๆฅๆพ (verified Int) + generic (unverified)
โ โโโ max_element/ โ
ๆๅคงๅ
็ด (verified Int) + generic (unverified)
โ โโโ min_element/ โ
ๆๅฐๅ
็ด (verified Int) + generic (unverified)
โ โโโ interpolation_search/๐ ๆๅผๆ็ดข (Int64 ้ฒๆบขๅบ)
โ โโโ exponential_search/ ๐ ๆๆฐๆ็ดข (galloping search)
โ โโโ fibonacci_search/ ๐ ๆๆณข้ฃๅฅๆ็ดข (8 tests)
โ โโโ jump_search/ ๐ ่ทณ่ทๆ็ดข (8 tests)
โ โโโ ternary_search/ ๐ ไธๅๆ็ดข (ๅๅณฐๅฝๆฐๆๅผ, 7 tests)
โ โโโ quickselect/ ๐ ๅฟซ้้ๆฉ (็ฌฌ k ๅฐ, 8 tests)
โ โโโ ball_tree/ ๐ Ball-Tree (ๅบฆ้็ฉบ้ด่ฟ้ป, 8 tests)
โ โโโ vp_tree/ ๐ VP-Tree (vantage point ๆ , 8 tests)
โ โโโ lsh/ ๐ LSH ๅฑ้จๆๆๅๅธ (่ฟไผผ่ฟ้ป, 7 tests)
โ โโโ hnsw/ ๐ HNSW (ๅๅฑๅฏๅฏผ่ชๅฐไธ็ๅพ, 8 tests)
โโโ sorting/
โ โโโ insertion_sort/ ๐ ๆๅ
ฅๆๅบ (generic, 12 tests)
โ โโโ selection_sort/ ๐ ้ๆฉๆๅบ (generic, 10 tests)
โ โโโ merge_sort/ ๐ ๅฝๅนถๆๅบ (generic, 15 tests, ็จณๅฎๆงๅทฒ้ช่ฏ)
โ โโโ quick_sort/ ๐ ๅฟซ้ๆๅบ (generic, 15 tests)
โ โโโ heap_sort/ ๐ ๅ ๆๅบ (generic, 12 tests)
โ โโโ counting_sort/ ๐ ่ฎกๆฐๆๅบ (OOM ้ฒๆค, 12 tests)
โ โโโ radix_sort/ ๐ ๅบๆฐๆๅบ LSD (stable, 11 tests)
โ โโโ is_sorted/ โ
ๆๅบๆงๆฃๆฅ (verified Int) + generic (unverified)
โ โโโ external_sort/ ๐ ๅค้จๆๅบ (k ่ทฏๅฝๅนถ, binary_heap ๅค็จ, 8 tests)
โโโ containers/
โ โโโ binary_heap/ ๐ ไบๅๅ (Heap ๅฐ่ฃ
+ HeapG[T] + decrease_key, 17 tests)
โ โโโ hash_table/ ๐ ๅๅธ่กจ K,V ๆณๅ (StringHashTable ๅฐ่ฃ
, 19 tests)
โ โโโ lru_cache/ ๐ LRU Cache O(1) (HashMap+ๅๅ้พ่กจ, 8 tests)
โ โโโ ttl_cache/ ๐ TTL Cache (่ฟๆๆธ
็ + LRU, 10 tests)
โ โโโ w_tinylfu/ ๐ W-TinyLFU ็ผๅญ (Window+SLRU+CMS, 11 tests)
โ โโโ bloom_filter/ ๐ ๅธ้่ฟๆปคๅจ (ๆไผๅๆฐ, 9 tests)
โ โโโ cuckoo_filter/ ๐ ๅธ่ฐท้ธ่ฟๆปคๅจ (ๆฏๆๅ ้ค, 8 tests)
โ โโโ count_min_sketch/ ๐ Count-Min Sketch (ๅๅๅธ+ๅๅนถ, 10 tests)
โ โโโ hyperloglog/ ๐ HyperLogLog ๅบๆฐไผฐ่ฎก (10 tests)
โ โโโ union_find/ ๐ ๅนถๆฅ้ (pub struct, findโInt?, 16 tests)
โ โโโ priority_queue/ ๐ ไผๅ
้ๅ (HeapG[T], ๅจๆๆฉๅฎน, decrease_key, 15 tests)
โ โโโ monotonic/ ๐ ๅ่ฐๆ /ๅ่ฐ้ๅ (next greater/smaller, ๆปๅจ็ชๅฃ, 21 tests)
โ โโโ bitset/ ๐ ไฝ้ (ไฝ่ฟ็ฎ, 8 tests)
โ โโโ deque/ ๐ ๅ็ซฏ้ๅ (็ฏๅฝข็ผๅฒๅบ, 8 tests)
โ โโโ consistent_hash/ ๐ ไธ่ดๆงๅๅธ (่ๆ่็น, 7 tests)
โ โโโ crc/ ๐ CRC ๆ ก้ช (CRC32, 7 tests)
โ โโโ hash_utils/ ๐ ๅๅธๅทฅๅ
ท (next_pow2, Fibonacci ๅๅธ, 6 tests)
โ โโโ lsm_tree/ ๐ LSM-Tree (ๅ
ๅญ MemTable+SSTable+Bloom, 10 tests)
โ โโโ roaring_bitmap/ ๐ Roaring Bitmap (ๅ็ผฉไฝๅพ, 8 tests)
โ โโโ count_sketch/ ๐ Count Sketch (้ข็ไผฐ่ฎก, 7 tests)
โ โโโ concurrent/ ๐ ๅนถๅๅ่ฏญ (RingBuffer/BoundedQueue/SnapshotMap, 9 tests)
โโโ trees/
โ โโโ bst/ ๐ ไบๅๆ็ดขๆ (่ฟญไปฃๅฎ็ฐ, ๆ ๆ ๆบขๅบ้ฃ้ฉ, 22 tests)
โ โโโ avl/ ๐ AVL ๅนณ่กกๆ (O(1) size, 17 tests)
โ โโโ red_black_tree/ ๐ ็บข้ปๆ Okasaki+Kahrs (generic, 23 tests)
โ โโโ btree/ ๐ B-Tree (16 tests)
โ โโโ segment_tree/ ๐ ็บฟๆฎตๆ + LazySegTree (19 tests)
โ โโโ fenwick/ ๐ ๆ ็ถๆฐ็ป (14 tests)
โ โโโ trie/ ๐ ๅญๅ
ธๆ (sparse children, autocomplete, wildcard search, 17 tests)
โ โโโ skip_list/ ๐ ่ทณ่กจ (O(log n) expected, 13 tests)
โ โโโ treap/ ๐ Treap (per-instance RNG, O(log n) expected, 13 tests)
โ โโโ splay/ ๐ ไผธๅฑๆ (iterative bottom-up, amortized O(log n), 10 tests)
โ โโโ sparse_table/ ๐ Sparse Table RMQ (ๆณๅ, O(1) ๅน็ญๆฅ่ฏข, 13 tests)
โ โโโ segment_tree_lazy/ ๐ ็บฟๆฎตๆ Lazy Propagation (ๅบ้ดไฟฎๆน+ๅบ้ดๆฅ่ฏข, 9 tests)
โ โโโ link_cut/ ๐ Link-Cut Tree (Sleator-Tarjan splay, 12 tests)
โ โโโ persistent_vector/ ๐ Persistent Vector (็ปๆๅ
ฑไบซ, O(log n), 9 tests)
โ โโโ bplus_tree/ ๐ B+ Tree (ๅถๅญ้พ่กจ, ่ๅดๆฅ่ฏข, 10 tests)
โ โโโ hamt/ ๐ HAMT (Hash Array Mapped Trie, 10 tests)
โ โโโ li_chao_tree/ ๐ ๆ่ถ
ๆ (็บฟๆฎต็ปดๆคไธๆฌกๅฝๆฐๆๅคงๅผ, 8 tests)
โ โโโ persistent_segment_tree/ ๐ ๅฏๆไน
ๅ็บฟๆฎตๆ (k ๅคงๅผๆฅ่ฏข, 8 tests)
โ โโโ segment_tree_beats/ ๐ Segment Tree Beats (ๅบ้ดๆๅผๅ chmax/chmin, 8 tests)
โ โโโ bit_2d/ ๐ ไบ็ปดๆ ็ถๆฐ็ป (8 tests)
โ โโโ mo_algorithm/ ๐ Mo ็ฎๆณ (็ฆป็บฟๅบ้ดๆฅ่ฏข, 8 tests)
โโโ graph/
โ โโโ bfs_dfs/ ๐ BFS/DFS ้ปๆฅ็ฉ้ต็ (Option ่ฟๅ, 34 tests)
โ โโโ adj_list/ ๐ ้ปๆฅ่กจ็จ็ๅพ (O(V+E) ็ฉบ้ด, 23 tests)
โ โโโ topological_sort/ ๐ ๆๆๆๅบ ้ปๆฅ็ฉ้ต็ (Option ่ฟๅ, 12 tests)
โ โโโ topological_sort_adj/ ๐ ๆๆๆๅบ ้ปๆฅ่กจ็ Kahn (16 tests)
โ โโโ kruskal/ ๐ ๆๅฐ็ๆๆ (14 tests)
โ โโโ prim/ ๐ Prim MST (11 tests)
โ โโโ scc/ ๐ Tarjan SCC ่ฟญไปฃ็ (12 tests)
โ โโโ dijkstra/ โ ๏ธ Dijkstra (partial verified: array bounds only, FixedArray[Int?])
โ โโโ dijkstra_heap/ ๐ ๅ ไผๅ Dijkstra (Int64 ๆบขๅบ้ฒๆค, 11 tests)
โ โโโ johnson/ ๐ Johnson ๅ
จๆบๆ็ญ่ทฏ (่ดๆ+่ด็ฏๆฃๆต, 11 tests)
โ โโโ bidirectional_bfs/ ๐ ๅๅ BFS (13 tests)
โ โโโ a_star/ ๐ A* ๆ็ดข (ไบๅๅ +่ทฏๅพ้ๅปบ, 11 tests)
โ โโโ max_flow/ ๐ Edmonds-Karp ๆๅคงๆต (12 tests)
โ โโโ advanced/ ๐ Bellman-Ford + Floyd-Warshall (SPResult, 19 tests)
โ โโโ min_cost_flow/ ๐ ๆๅฐ่ดน็จๆๅคงๆต SPFA (linked-forward-star, 9 tests)
โ โโโ two_sat/ ๐ 2-SAT (implication graph + Tarjan SCC, 8 tests)
โ โโโ dinic/ ๐ Dinic ๆๅคงๆต (level graph + iterative blocking flow, 8 tests)
โ โโโ lca/ ๐ LCA ๆ่ฟๅ
ฌๅ
ฑ็ฅๅ
(binary lifting, O(log n) query, 11 tests)
โ โโโ bridge_articulation/ ๐ ๆกฅ+ๅฒ็น (Tarjan, ๅค้่พนๅค็, 15 tests)
โ โโโ euler_path/ ๐ ๆฌงๆ่ทฏๅพ/ๅ่ทฏ (Hierholzer, ่ฟญไปฃๅฎ็ฐ, 14 tests)
โ โโโ hungarian/ ๐ ๅ็ๅฉ็ฎๆณ (ไบๅๅพๆไผๅน้
, O(nยณ), 10 tests)
โ โโโ hopcroft_karp/ ๐ Hopcroft-Karp ไบๅๅน้
(O(EโV), 9 tests)
โ โโโ stoer_wagner/ ๐ Stoer-Wagner ๅ
จๅฑๆๅฐๅฒ (O(Vยณ), 10 tests)
โ โโโ max_clique/ ๐ Bron-Kerbosch ๆๅคงๅข (pivot+้ๅๅบฆ, 12 tests)
โ โโโ edmonds_blossom/ ๐ Edmonds ไธ่ฌๅพๆๅคงๅน้
(BFS ๅขๅนฟ, 8 tests)
โ โโโ dominator_tree/ ๐ ๆฏ้
ๆ (Lengauer-Tarjan, 8 tests)
โ โโโ gomory_hu/ ๐ Gomory-Hu ๆ (ๅ
จๅฏนๆๅฐๅฒ, 8 tests)
โ โโโ hlpp/ ๐ HLPP ๆๅคงๆต (้ขๆตๆจ่ฟ, 8 tests)
โ โโโ hld/ ๐ ้้พๅๅ (่ทฏๅพไฟฎๆน/ๆฅ่ฏข, 8 tests)
โ โโโ centroid_decomposition/ ๐ ้ๅฟๅ่งฃ (็นๅๆฒป, 8 tests)
โ โโโ virtual_tree/ ๐ ่ๆ (ๅ
ณ้ฎ็นๅ็ผฉ, 8 tests)
โ โโโ min_steiner_tree/ ๐ ๆๅฐ Steiner ๆ (DP, 8 tests)
โ โโโ graph_coloring/ ๐ ๅพ็่ฒ (DSATUR ๅฏๅๅผ, 8 tests)
โ โโโ flow_with_bounds/ ๐ ไธไธ็็ฝ็ปๆต (8 tests)
โ โโโ pagerank/ ๐ PageRank (ๅน่ฟญไปฃ, 7 tests)
โโโ string/
โ โโโ kmp/ ๐ KMP (17 tests)
โ โโโ rabin_karp/ ๐ Rabin-Karp (25 tests)
โ โโโ suffix_array/ ๐ ๅ็ผๆฐ็ป (15 tests)
โ โโโ z_function/ ๐ Z ็ฎๆณ (z_array + z_search, 19 tests)
โ โโโ manacher/ ๐ Manacher ๅๆ (longest/count/radii, 23 tests)
โ โโโ aho_corasick/ ๐ Aho-Corasick ๅคๆจกๅผๅน้
(sparse children, CJK ๅฎๅ
จ, 12 tests)
โ โโโ boyer_moore/ ๐ Boyer-Moore ๅญ็ฌฆไธฒๆ็ดข (bad-char + good-suffix, 14 tests)
โ โโโ lcp_array/ ๐ LCP ๆฐ็ป (Kasai ็ฎๆณ, O(n), 13 tests)
โ โโโ suffix_automaton/ ๐ ๅ็ผ่ชๅจๆบ SAM (ๅญไธฒๆฅ่ฏข, ไธๅๅญไธฒ่ฎกๆฐ, 12 tests)
โ โโโ suffix_tree/ ๐ ๅ็ผๆ (Ukkonen O(n), 12 tests)
โ โโโ palindromic_tree/ ๐ ๅๆๆ Eertree (ๆๆๅๆๅญไธฒ, 11 tests)
โ โโโ rolling_hash/ ๐ ๆปๅจๅๅธ (ๅๆจกๆฐ้ฒ็ขฐๆ, 12 tests)
โ โโโ lyndon/ ๐ Lyndon ๅ่งฃ (Duval ็ฎๆณ, ๆๅฐ่กจ็คบ, 13 tests)
โ โโโ fm_index/ ๐ FM-Index (่ฎกๆฐ/ๅฎไฝ, 8 tests)
โ โโโ wavelet_tree/ ๐ Wavelet Tree (rank/select, 8 tests)
โ โโโ regex/ ๐ ๆญฃๅ่กจ่พพๅผๅผๆ (Thompson NFA, 10 tests)
โ /// **ๅญ็ฌฆไธฒ็ฎๆณ็ผบๅคฑๅฃฐๆ**๏ผๅฝๅ 22 ไธชๅญ็ฌฆไธฒๅ
่ฆ็ไบๆ ธๅฟๆจกๅผๅน้
ๅๅ็ผ็ปๆ๏ผ
โ /// ไฝไปฅไธ็ฎๆณๅฐๆชๅฎ็ฐ๏ผde Bruijn ๅบๅใLyndon suffix array ๆ้ (LA factor)ใ
โ /// runs (Lempel-Ziv ่งฃๆ)ใSuffix Array โ Tree ไบ่ฝฌๅทฅๅ
ทๅฝๆฐใ
โโโ number_theory/
โ โโโ gcd/ โ ๏ธ GCD (partial verified, handles Int::MIN)
โ โโโ fast_power/ โ ๏ธ ๅฟซ้ๅน (partial verified + checked variant)
โ โโโ int64_utils/ ๐ Int64 ๅทฅๅ
ท (mod64/gcd64/pow_mod64/is_prime64, 21 tests)
โ โโโ prime/ ๐ ็ด ๆฐ็ญ + ๆฉๅฑๆฌงๅ ้ๅพ (OOM ้ฒๆค, 18 tests)
โ โโโ miller_rabin/ ๐ Miller-Rabin ็ด ๆงๆฃ้ช (deterministic, 11 tests)
โ โโโ crt/ ๐ ไธญๅฝๅฉไฝๅฎ็ (coprime + non-coprime, 20 tests)
โ โโโ bsgs/ ๐ BSGS ็ฆปๆฃๅฏนๆฐ (O(โp), 8 tests)
โ โโโ pollard_rho/ ๐ Pollard-Rho ๆดๆฐๅ่งฃ (Miller-Rabin + Brent, 10 tests)
โ โโโ euler_sieve/ ๐ Euler ็บฟๆง็ญ (O(n) + O(log n) ๅ ๅผๅ่งฃ, 11 tests)
โ โโโ ntt/ ๐ ๆฐ่ฎบๅๆข NTT (O(n log n) ๅค้กนๅผไนๆณ, 11 tests)
โ โโโ bigint/ ๐ ๅคงๆดๆฐ่ฟ็ฎ (ๅ ๅไน้ค, 10 tests)
โ โโโ cipolla/ ๐ Cipolla ๅนณๆนๆ น (ๆจก็ด ๆฐ, 17 tests)
โ โโโ finite_field/ ๐ ๆ้ๅ GF(p) ่ฟ็ฎ (7 tests)
โ โโโ mobius/ ๐ Mรถbius ๅๆผ (7 tests)
โ โโโ polynomial/ ๐ ๅค้กนๅผ่ฟ็ฎ (NTT ไนๆณ, 8 tests)
โ โโโ primitive_root/ ๐ ๅๆ น (7 tests)
โ โโโ quadratic_residue/ ๐ ไบๆฌกๅฉไฝ (Tonelli-Shanks, 7 tests)
โ โโโ reed_solomon/ ๐ Reed-Solomon ็ผ่งฃ็ (8 tests)
โ โโโ pohlig_hellman/ ๐ Pohlig-Hellman ็ฆปๆฃๅฏนๆฐ (16 tests)
โ โโโ carmichael/ ๐ Carmichael ๅฝๆฐ (5 tests)
โ โโโ aks/ ๐ AKS ็กฎๅฎๆง็ด ๆฐๆต่ฏ (5 tests)
โ โโโ quadratic_sieve/ ๐ ไบๆฌก็ญๆณๅ ๅผๅ่งฃ (5 tests)
โ โโโ lehman_factor/ ๐ Lehman ๅ ๅผๅ่งฃ (5 tests)
โโโ math/
โ โโโ array_sum/ โ ๏ธ ๆฐ็ปๆฑๅ (partial verified + checked variant)
โ โโโ combinatorics/ ๐ ็ปๅๆฐๅญฆ (็ปๅๆฐ/Catalan/Stirling, Int64 ้ฒๆบขๅบ, 15 tests)
โ โโโ matrix/ ๐ ็ฉ้ต่ฟ็ฎ (ไนๆณ+้ซๆฏๆถๅ
+่กๅๅผ, checked variant, 12 tests)
โ โโโ matrix_decomp/ ๐ ็ฉ้ตๅ่งฃ LU/QR/SVD (้จๅไธปๅ
/Householder/Jacobi, 16 tests)
โ โโโ newton_method/ ๐ Newton ่ฟญไปฃๆณ (ๆ นๆฑ่งฃ+nๆฌกๆ น+ๅนณๆนๆ น, 23 tests)
โ โโโ berlekamp_massey/ ๐ Berlekamp-Massey ็บฟๆง้ๆจ (O(nยฒ), 10 tests)
โ โโโ fft/ ๐ FFT ๅฟซ้ๅ
้ๅถๅๆข (Cooley-Tukey, 11 tests)
โ โโโ simplex/ ๐ ๅ็บฏๅฝขๆณ ็บฟๆง่งๅ (ไธค้ถๆฎต, 10 tests)
โโโ dp/
โ โโโ dp/ ๐ LCS + ็ผ่พ่ท็ฆป + ่ๅ
(OOM ้ฒๆค, 21 tests)
โ โโโ lis/ ๐ LIS O(n log n) (14 tests)
โ โโโ interval_dp/ ๐ ๅบ้ด DP (็ฉ้ต้พไน+ๆไผBST+burst balloons+็ณๅญๅๅนถ, 22 tests)
โ โโโ tree_dp/ ๐ ๆ ๅฝข DP (ๆๅคง็ฌ็ซ้+็ดๅพ+ๅน้
+ๆ ่ๅ
, ่ฟญไปฃDFS, 19 tests)
โ โโโ digit_dp/ ๐ ๆฐไฝ DP (่ฎกๆฐ+ๅไฝๆฐๅญๅ+ไธๅซๆๆฐๅญ, 11 tests)
โโโ geometry/
โ โโโ convex_hull/ ๐ Graham ๅธๅ
(Int64 ้ฒๆบขๅบ, 9 tests)
โ โโโ andrew_hull/ ๐ Andrew ๅ่ฐ้พๅธๅ
(Int64 ้ฒๆบขๅบ, 11 tests)
โ โโโ convex_hull_3d/ ๐ 3D ๅธๅ
(้ๆบๅข้ๆณ+ๅฐๅนณ็บฟ่พน, 12 tests)
โ โโโ half_plane_intersection/ ๐ ๅๅนณ้ขไบค (S&I ็ฎๆณ+ๅ็ซฏ้ๅ, 9 tests)
โ โโโ kd_tree/ ๐ KD-Tree 2D ็ฉบ้ด็ดขๅผ (NN + range search, 13 tests)
โ โโโ rotating_calipers/ ๐ ๆ่ฝฌๅกๅฃณ (ๅธๅ
็ดๅพ+ๅฎฝๅบฆ, CCW/CW, 14 tests)
โ โโโ closest_pair/ ๐ ๆ่ฟ็นๅฏน (ๅๆฒป O(n log n), 9 tests)
โ โโโ segment_ops/ ๐ ็บฟๆฎต็ธไบค+็นๅจๅค่พนๅฝขๅ
(็ฒพ็กฎๆดๆฐๅ็งฏ, 33 tests)
โ โโโ delaunay/ ๐ Delaunay ไธ่งๅๅ (ๅข้ๆณ, 8 tests)
โ โโโ voronoi/ ๐ Voronoi ๅพ (Delaunay ๅฏนๅถ, 7 tests)
โ โโโ dynamic_hull/ ๐ ๅจๆๅธๅ
(ๅจ็บฟๆๅ
ฅ, 8 tests)
โ โโโ min_enclosing_circle/ ๐ ๆๅฐๅ
ๅดๅ (้ๆบๅข้, 7 tests)
โ โโโ minkowski_sum/ ๐ Minkowski ๅ (ๅธๅค่พนๅฝข, 8 tests)
โ โโโ polygon_boolean/ ๐ ๅค่พนๅฝขๅธๅฐ่ฟ็ฎ (ๅนถ/ไบค/ๅทฎ, 8 tests)
โโโ game_theory/
โ โโโ nim_sg/ ๐ Nim ๅๅผ (Sprague-Grundy ๅฎ็, 13 tests)
โ โโโ alpha_beta/ ๐ Alpha-Beta ๅชๆ / Negamax (Tic-Tac-Toe ้ช่ฏ, 7 tests)
โ โโโ mcts/ ๐ Monte Carlo Tree Search (UCT, 7 tests)
โ โโโ gale_shapley/ ๐ Gale-Shapley ็จณๅฎๅน้
(10 tests)
โ โโโ shapley_value/ ๐ Shapley ๅผ (็ฒพ็กฎ+Monte Carlo, 5 tests)
โ โโโ negamax/ ๐ Negamax ๆ็ดข (Alpha-Beta ๅชๆ, 3 tests)
โ โโโ transposition_table/ ๐ ็ฝฎๆข่กจ (Zobrist ๅๅธ, 6 tests)
โโโ random/
โ โโโ reservoir_sampling/ ๐ ๆฐดๅบ้ๆ ท (O(n) ๅจ็บฟ้ๆ ท, 8 tests)
โ โโโ weighted_sampling/ ๐ Alias Method + ๅ ๆๆฐดๅบ้ๆ ท (SplitMix64, 8 tests)
โ โโโ fisher_yates/ ๐ Fisher-Yates ๆด็ (Partial Shuffle, 7 tests)
โ โโโ mersenne_twister/ ๐ Mersenne Twister MT19937 (32/64-bit, 8 tests)
โ โโโ pcg/ ๐ PCG ้ๆบๆฐ็ๆๅจ (32/64-bit, 6 tests)
โ โโโ xoshiro/ ๐ Xoshiro256**/512** PRNG (8 tests)
โ โโโ gaussian_sampling/ ๐ Box-Muller ้ซๆฏ้ๆ ท (6 tests)
โ โโโ zobrist_hash/ ๐ Zobrist ๅๅธ (ๆฃ็็ถๆๅๅธ, 5 tests)
โ โโโ mcmc/ ๐ Metropolis-Hastings MCMC (14 tests)
โ โโโ monte_carlo/ ๐ Monte Carlo ็งฏๅ (7 tests)
โโโ sorting/
โ โโโ timsort/ ๐ TimSort (run ๆฃๆต+ๅฝๅนถๆ , ็จณๅฎ, 12 tests)
โ โโโ introsort/ ๐ Introsort (ๅฟซๆ+ๅ ๆ+ๆๅ
ฅๆ, 10 tests)
โ โโโ pdq_sort/ ๐ Pattern-Defeating Quicksort (10 tests)
โ โโโ bucket_sort/ ๐ ๆกถๆๅบ (10 tests)
โโโ containers/
โ โโโ treiber_stack/ ๐ Treiber ๆ (ๅ็บฟ็จ CAS ๆจกๆ, 8 tests)
โ โโโ mpmc_queue/ ๐ MPMC ้ๅ (ๅ็บฟ็จ CAS ๆจกๆ, Vyukov, 8 tests)
โ โโโ concurrent_hash_map/ ๐ Concurrent HashMap (ๅ็บฟ็จๅๆฎต้ๆจกๆ, 9 tests)
โ โโโ work_stealing/ ๐ Work-Stealing ้ๅ (ๅ็บฟ็จๆจกๆ, Chase-Lev, 8 tests)
โ โโโ lock_free_queue/ ๐ ๆ ้้ๅ (ๅ็บฟ็จๆจกๆ, 8 tests)
โ โโโ skip_list/ ๐ ่ทณ่กจ (็ฌ็ซๅ
, 4 tests)
โ โโโ counting_bloom/ ๐ ่ฎกๆฐๅธ้่ฟๆปคๅจ (5 tests)
โ โโโ cuckoo_hashmap/ ๐ ๅธ่ฐท้ธๅๅธ่กจ (6 tests)
โ โโโ bimap/ ๐ ๅๅๆ ๅฐ (5 tests)
โ โโโ monotonic/ ๐ ๅ่ฐๆ /ๅ่ฐ้ๅ (21 tests)
โโโ trees/
โ โโโ rope/ ๐ Rope (ๅนณ่กกๆ ๅญ็ฌฆไธฒ, O(log n), 12 tests)
โ โโโ interval_tree/ ๐ ๅบ้ดๆ (้ๅ ๆฅ่ฏข, 10 tests)
โ โโโ range_tree/ ๐ ่ๅดๆ (2D ๆญฃไบค่ๅดๆฅ่ฏข, 8 tests)
โ โโโ r_tree/ ๐ R-Tree (็ฉบ้ด็ดขๅผ, 10 tests)
โ โโโ fibonacci_heap/ ๐ Fibonacci ๅ (O(1) decrease-key, 12 tests)
โโโ graph/
โ โโโ chu_liu/ ๐ Chu-Liu ๆๅฐๆ ๅฝขๅพ (Edmonds, 8 tests)
โ โโโ k_shortest_paths/ ๐ K ๆ็ญ่ทฏ (Yen ็ฎๆณ, 8 tests)
โ โโโ min_cost_flow/ ๐ ๆๅฐ่ดน็จๆต (SSP+SPFA, 9 tests)
โ โโโ tree_isomorphism/ ๐ ๆ ๅๆ (AHU ็ฎๆณ, 7 tests)
โ โโโ push_relabel/ ๐ Push-Relabel ๆๅคงๆต (5 tests)
โ โโโ planar_test/ ๐ ๅนณ้ขๅพๅคๅฎ (5 tests)
โ โโโ isomorphism/ ๐ ๅพๅๆ (VF2 ็ฎๆณ, 5 tests)
โโโ string/
โ โโโ dawg/ ๐ DAWG (ๅ็ผฉๅญๅ
ธ, 10 tests)
โ โโโ sa_is/ ๐ SA-IS ๅ็ผๆฐ็ป (O(n), 17 tests)
โ โโโ bwt/ ๐ Burrows-Wheeler ๅๆข (15 tests)
โ โโโ suffix_balanced_tree/ ๐ ๅ็ผๅนณ่กกๆ (ๅฝๅนถๆๅบ, 8 tests)
โ โโโ unicode_normalization/ ๐ Unicode ่ง่ๅ (NFC/NFD/NFKC/NFKD, 6 tests)
โ โโโ encoding_conversion/ ๐ ็ผ็ ่ฝฌๆข (UTF-8/UTF-16/GBK, 6 tests)
โโโ geometry/
โ โโโ segment_intersection/๐ ้็จ็บฟๆฎตๆฑไบค (Bentley-Ottmann, 10 tests)
โ โโโ point_in_polygon/ ๐ ็นๅจๅค่พนๅฝขๅ
(ๅฐ็บฟๆณ, 8 tests)
โ โโโ polygon_ops/ ๐ ๅค่พนๅฝขๆไฝ (้ข็งฏ/้ๅฟ/่ฃๅช, 10 tests)
โ โโโ bentley_ottmann/ ๐ ๆซๆ็บฟ็บฟๆฎตๆฑไบค (8 tests)
โโโ dp/
โ โโโ aliens_trick/ ๐ Aliens' Trick (ๆๆ ผๆๆฅๆพๅผ, 8 tests)
โ โโโ knapsack_opt/ ๐ ่ๅ
ไผๅ (ๅค้/ไบ็ปด/ๅ่ฐ้ๅ, 10 tests)
โ โโโ matrix_chain/ ๐ ็ฉ้ต้พไน DP (8 tests)
โ โโโ monotone_queue_dp/ ๐ ๅ่ฐ้ๅไผๅ DP (8 tests)
โ โโโ smawk/ ๐ SMAWK ็ฎๆณ (ๅฎๅ
จๅ่ฐ็ฉ้ต่กๆๅฐ, 10 tests)
โ โโโ bitmask_dp/ ๐ ็ถๅ DP (TSP/้ๅ่ฆ็, 10 tests)
โ โโโ convex_hull_trick/ ๐ ๅธๅฃณๆๅทง DP (ๆ็ไผๅ, 8 tests)
โ โโโ divide_conquer_dp/ ๐ ๅๆฒป DP (8 tests)
โ โโโ knuth_opt/ ๐ Knuth ไผๅ DP (8 tests)
โ โโโ plug_dp/ ๐ ๆๅคด DP (่ฝฎๅป็บฟ, 7 tests)
โ โโโ sos_dp/ ๐ SOS DP (ๅญ้ๅ, 8 tests)
โโโ math/
โ โโโ fwht/ ๐ ๅฟซ้ Walsh-Hadamard ๅๆข (7 tests)
โ โโโ numerical_integration/๐ ๆฐๅผ็งฏๅ (ๆขฏๅฝข/Simpson/่ช้ๅบ/Romberg, 9 tests)
โ โโโ ode_solver/ ๐ ODE ๆฑ่งฃๅจ (Euler/RK4/RK45, 8 tests)
โ โโโ interpolation/ ๐ ๆๅผ (Lagrange/Newton, 7 tests)
โ โโโ least_squares/ ๐ ๆๅฐไบไนๆณ (็บฟๆง/ๅค้กนๅผ, 8 tests)
โ โโโ special_functions/ ๐ ็นๆฎๅฝๆฐ (Gamma/Erf/Bessel, 10 tests)
โ โโโ conjugate_gradient/ ๐ ๅ
ฑ่ฝญๆขฏๅบฆๆณ (SPD ็บฟๆง็ณป็ปๆฑ่งฃ, 7 tests)
โ โโโ gmres/ ๐ GMRES (้ๅฏน็งฐ็บฟๆง็ณป็ปๆฑ่งฃ, 6 tests)
โ โโโ lbfgs/ ๐ L-BFGS ๆ็้กฟไผๅๅจ (ๅคง่งๆจกไผๅ, 9 tests)
โ โโโ autodiff/ ๐ ่ชๅจๅพฎๅ (ๅๅๆจกๅผ, ๅๆฐ, 19 tests)
โ โโโ sparse_matrix/ ๐ ็จ็็ฉ้ต (CSR ๆ ผๅผ, 7 tests)
โ โโโ eigenvalue/ ๐ ็นๅพๅผๅ่งฃ (Jacobi ๆนๆณ, 5 tests)
โ โโโ qr_pivoting/ ๐ QR ๅ่งฃ (ๅไธปๅ
, 5 tests)
โ โโโ groebner/ ๐ Grรถbner ๅบ (Buchberger ็ฎๆณ, 5 tests)
โ โโโ polynomial_factor/ ๐ ๅค้กนๅผๅ ๅผๅ่งฃ (5 tests)
โ โโโ ilp/ ๐ ๆดๆฐ็บฟๆง่งๅ (5 tests)
โ โโโ sdp/ ๐ ๅๆญฃๅฎ่งๅ (Jacobi ็นๅพๅผ, 7 tests)
โโโ crypto/
โ โโโ sha256/ ๐ SHA-256 ๅๅธ (10 tests)
โ โโโ sha512/ ๐ SHA-512 ๅๅธ (8 tests)
โ โโโ sha3/ ๐ SHA-3 (Keccak) ๅๅธ (8 tests)
โ โโโ sha1/ ๐ SHA-1 ๅๅธ (10 tests)
โ โโโ blake2/ ๐ BLAKE2 ๅๅธ (8 tests)
โ โโโ blake3/ ๐ BLAKE3 ๅๅธ (8 tests)
โ โโโ hmac/ ๐ HMAC ๆถๆฏ่ฎค่ฏ (7 tests)
โ โโโ chacha20/ ๐ ChaCha20 ๆตๅฏ็ (8 tests)
โ โโโ chacha20_poly1305/ ๐ ChaCha20-Poly1305 AEAD (7 tests)
โ โโโ xchacha20/ ๐ XChaCha20 (HChaCha20 + ChaCha20, 8 tests)
โ โโโ poly1305/ ๐ Poly1305 MAC (7 tests)
โ โโโ hkdf/ ๐ HKDF ๅฏ้ฅๆดพ็ (7 tests)
โ โโโ pbkdf2/ ๐ PBKDF2 ๅฏ็ ๆดพ็ (6 tests)
โ โโโ scrypt/ ๐ scrypt ๅฏ็ ๅๅธ (6 tests)
โ โโโ bcrypt/ ๐ bcrypt ๅฏ็ ๅๅธ (8 tests)
โ โโโ argon2/ ๐ Argon2 ๅฏ็ ๅๅธ (6 tests)
โ โโโ aes/ ๐ AES ๅฏน็งฐๅ ๅฏ (constant-time S-box, 8 tests)
โ โโโ aes_ccm/ ๐ AES-CCM AEAD (7 tests)
โ โโโ rsa/ ๐ RSA ้ๅฏน็งฐๅ ๅฏ (OAEP/PSS, 7 tests)
โ โโโ ecdsa/ ๐ ECDSA P-256 (RFC 6979, 13 tests)
โ โโโ ed25519/ ๐ Ed25519 ็ญพๅ (RFC 8032, 13 tests)
โ โโโ x25519/ ๐ X25519 ๅฏ้ฅไบคๆข (RFC 7748, 8 tests)
โ โโโ secp256k1/ ๐ secp256k1 (Bitcoin/Ethereum, 10 tests)
โ โโโ csprng/ ๐ CSPRNG ๅฎๅ
จ้ๆบๆฐ (6 tests)
โ โโโ base64/ ๐ Base64 ็ผ็ (7 tests)
โ โโโ base32/ ๐ Base32 ็ผ็ (9 tests)
โ โโโ hex/ ๐ Hex ็ผ่งฃ็ (14 tests)
โโโ compression/
โ โโโ huffman/ ๐ Huffman ็ผ็ (8 tests)
โ โโโ lz4/ ๐ LZ4 ๅ็ผฉ (7 tests)
โ โโโ lz77/ ๐ LZ77 ๅ็ผฉ (7 tests)
โ โโโ lzw/ ๐ LZW ๅ็ผฉ (7 tests)
โ โโโ arithmetic_coding/ ๐ ็ฎๆฏ็ผ็ (7 tests)
โ โโโ bwt_compress/ ๐ BWT ๅ็ผฉ (6 tests)
โ โโโ deflate/ ๐ DEFLATE ๅ็ผฉ (RFC 1951, 8 tests)
โ โโโ gzip/ ๐ gzip ๅฎนๅจ (RFC 1952, 7 tests)
โ โโโ zlib/ ๐ zlib ๅฎนๅจ (RFC 1950, 7 tests)
โ โโโ snappy/ ๐ Snappy ๅ็ผฉ (7 tests)
โ โโโ zstd/ ๐ Zstandard ๅ็ผฉ (6 tests)
โ โโโ brotli/ ๐ Brotli ๅ็ผฉ (7 tests)
โโโ ml/
โ โโโ kmeans/ ๐ K-Means++ ่็ฑป (8 tests)
โ โโโ knn/ ๐ K-่ฟ้ป (KD-Tree ๅ ้, 8 tests)
โ โโโ dbscan/ ๐ DBSCAN ๅฏๅบฆ่็ฑป (7 tests)
โ โโโ pca/ ๐ ไธปๆๅๅๆ PCA (8 tests)
โ โโโ svm/ ๐ ๆฏๆๅ้ๆบ SVM (8 tests)
โ โโโ logistic_regression/ ๐ ้ป่พๅๅฝ (8 tests)
โ โโโ decision_tree/ ๐ ๅณ็ญๆ CART (8 tests)
โ โโโ random_forest/ ๐ ้ๆบๆฃฎๆ (ๅ็ฑป+ๅๅฝ+OOB, 8 tests)
โ โโโ gradient_boosting/ ๐ ๆขฏๅบฆๆๅ (GBDT, 7 tests)
โ โโโ adaboost/ ๐ AdaBoost (6 tests)
โ โโโ mlp/ ๐ ๅคๅฑๆ็ฅๆบ MLP (8 tests)
โ โโโ gmm/ ๐ ้ซๆฏๆททๅๆจกๅ GMM (EM, 7 tests)
โ โโโ hierarchical_clustering/ ๐ ๅฑๆฌก่็ฑป (7 tests)
โ โโโ gaussian_process/ ๐ ้ซๆฏ่ฟ็จๅๅฝ (6 tests)
โ โโโ naive_bayes/ ๐ ๆด็ด ่ดๅถๆฏ (8 tests)
โ โโโ model_evaluation/ ๐ ๆจกๅ่ฏไผฐ (accuracy/precision/recall/F1/AUC, 10 tests)
โโโ stats/
โ โโโ descriptive/ ๐ ๆ่ฟฐ็ป่ฎก (9 tests)
โ โโโ linear_regression/ ๐ ็บฟๆงๅๅฝ (8 tests)
โ โโโ hypothesis_testing/ ๐ ๅ่ฎพๆฃ้ช (8 tests)
โ โโโ correlation/ ๐ ็ธๅ
ณ็ณปๆฐ (Pearson/Spearman, 7 tests)
โ โโโ confidence_interval/ ๐ ็ฝฎไฟกๅบ้ด (7 tests)
โ โโโ bootstrap/ ๐ Bootstrap ้้ๆ ท (7 tests)
โ โโโ distributions/ ๐ ๆฆ็ๅๅธ (Normal/Exp/Binomial/Poisson/Beta/t/Chi2/F/Gamma, 38 tests)
โ โโโ anova/ ๐ ๆนๅทฎๅๆ ANOVA (8 tests)
โ โโโ nonparametric/ ๐ ้ๅๆฐๆฃ้ช (Mann-Whitney/Wilcoxon/Kruskal-Wallis, 8 tests)
โโโ serialization/
โ โโโ json/ ๐ JSON ็ผ่งฃ็ (7 tests)
โ โโโ msgpack/ ๐ MessagePack ็ผ่งฃ็ (7 tests)
โ โโโ csv/ ๐ CSV ็ผ่งฃ็ (6 tests)
โ โโโ toml/ ๐ TOML 1.0.0 ่งฃๆๅจ (15 tests)
โ โโโ yaml/ ๐ YAML ่งฃๆๅจ (8 tests)
โ โโโ cbor/ ๐ CBOR ็ผ่งฃ็ (7 tests)
โ โโโ protobuf/ ๐ Protobuf ็ผ่งฃ็ (6 tests)
โโโ time/
โ โโโ chrono/ ๐ ๆฅๆๆถ้ดๅบ (ISO 8601, Duration, ๆถๅบ, 15 tests)
โโโ utils/
โ โโโ (utils) ๐ ๅ
ฑไบซๅทฅๅ
ท (swap/str_cmp/next_pow2/encoding/approx_eq)
โ โโโ prng/ ๐ PRNG (SplitMix64/XorShift64/LCG)
โ โโโ itertools/ ๐ itertools (range/repeat/enumerate/window/chunk/fold)
โ โโโ structured_logging/ ๐ ็ปๆๅๆฅๅฟ (6 tests)
โ โโโ error_chain/ ๐ ้่ฏฏ้พ (5 tests)
โโโ test/
โ โโโ property_test/ ๐ QuickCheck ้ฃๆ ผๅฑๆงๆต่ฏๆกๆถ (้ๆบ่พๅ
ฅ็ๆ + ๅไพ็ผฉๅ)
โ โโโ fuzz/ ๐ Fuzz ๆต่ฏ + ๅฏนๆๆง่พๅ
ฅๆต่ฏ
โ โโโ stress/ ๐ ๅๅๆต่ฏ (ๆๅบ็ฝฎๆข้ช่ฏ, LIS ๅญๅบๅ้ช่ฏ)
โ โโโ test_utils/ ๐ ๅ
ฑไบซๆต่ฏๅทฅๅ
ท (ๆถ้ค str_cmp ้ๅค)
โ โโโ coverage/ ๐ ๆต่ฏ่ฆ็็ๆฅๅ
โโโ finance/
โ โโโ black_scholes/ ๐ Black-Scholes ๆๆๅฎไปท (11 tests)
โ โโโ portfolio_optimization/ ๐ ๆ่ต็ปๅไผๅ (Markowitz/Black-Litterman, 8 tests)
โ โโโ risk_management/ ๐ ้ฃ้ฉ็ฎก็ (VaR/CVaR/ๅๅๆต่ฏ, 8 tests)
โ โโโ greeks/ ๐ Greeks ้ฃ้ฉๆๆๅบฆ (Delta/Gamma/Vega/Theta/Rho, 9 tests)
โ โโโ time_series/ ๐ ๆถ้ดๅบๅๅๆ (ARIMA/GARCH/ADF, 12 tests)
โ โโโ execution/ ๐ ๆง่ก็ฎๆณ (TWAP/VWAP/Implementation Shortfall, 8 tests)
โ โโโ backtest/ ๐ ๅๆตๆกๆถ (ไบไปถ้ฉฑๅจ/็ปฉๆๅๆ, 9 tests)
โโโ docs/
โ โโโ API_STABILITY.md ๐ API ็จณๅฎๆง็ญ็ฅไธ็ๆฌๅๅฒ
โโโ benchmarks/ ๐ ๆง่ฝๅบๅๆต่ฏ (wall-clock + ๅคๆๅบฆ้ช่ฏ)
โโโ .github/workflows/
โ โโโ ci.yml โ
GitHub Actions CI (check + test + prove, Ubuntu/macOS/Windows)
โ โโโ codeql.yml โ
CodeQL ๅฎๅ
จๅๆ
โ โโโ dependency-review.yml โ
ไพ่ตๅฎกๆฅ
โ โโโ nightly.yml โ
ๆฏๆฅๆๅปบ (flaky test ๆฃๆต)
โ โโโ release.yml โ
ๅๅธๆต็จ (checksums + tag)
โโโ CHANGELOG.md ๐ Semantic Versioning changelog
โโโ moon.mod
โโโ LICENSE
โโโ README.mdๅพไพ๏ผโ
= ๅฎๆดๆญฃ็กฎๆง้ช่ฏ | ๐ถ = ๅขๅผบ้ช่ฏ | โ ๏ธ = ้จๅ้ช่ฏ | ๐ = ไป
ๆต่ฏ้ช่ฏ
#ๆต่ฏ็ป่ฎก
| ๅ | ๆต่ฏๆฐ | moon prove | ๆณๅ |
|---|---|---|---|
| binary_search | 8 | โ ๅฎๆดๆญฃ็กฎๆง | โ generic |
| bound_search | 11 | ๐ tested | โ generic |
| linear_search | 8 | โ ๅฎๆดๆญฃ็กฎๆง | โ generic |
| max_element | 7 | โ ๅฎๆดๆญฃ็กฎๆง | โ generic |
| min_element | 7 | โ ๅฎๆดๆญฃ็กฎๆง | โ generic |
| interpolation_search | 11 | ๐ tested | โ |
| exponential_search | 11 | ๐ tested | โ |
| insertion_sort | 12 | โ ๏ธ ้จๅ้ช่ฏ | โ generic |
| selection_sort | 10 | ๐ tested | โ generic |
| merge_sort | 15 | โ ๏ธ ้จๅ้ช่ฏ | โ generic |
| quick_sort | 15 | ๐ tested | โ generic |
| heap_sort | 12 | ๐ tested | โ generic |
| counting_sort | 12 | ๐ tested | โ |
| radix_sort | 11 | ๐ tested | โ |
| is_sorted | 10 | โ ๅฎๆดๆญฃ็กฎๆง | โ generic |
| binary_heap | 17 | โ ๏ธ ้จๅ้ช่ฏ | โ HeapG[T] |
| hash_table | 19 | ๐ tested | โ HashTable[K,V] |
| lru_cache | 8 | ๐ tested | โ |
| bloom_filter | 9 | ๐ tested | โ |
| union_find | 16 | โ ๏ธ ้จๅ้ช่ฏ | โ (pub struct) |
| bst | 19 | ๐ tested | โ |
| avl | 17 | ๐ tested | โ |
| red_black_tree | 23 | โ ๏ธ ้จๅ้ช่ฏ | โ generic |
| btree | 16 | ๐ tested | โ |
| segment_tree | 19 | ๐ tested | โ |
| fenwick | 14 | ๐ tested | โ |
| trie | 17 | ๐ tested | โ String |
| skip_list | 13 | ๐ tested | โ |
| treap | 13 | ๐ tested | โ |
| bfs_dfs | 34 | ๐ tested | โ |
| adj_list | 23 | ๐ tested | โ |
| topological_sort | 12 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| topological_sort_adj | 16 | ๐ tested | โ |
| kruskal | 14 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| prim | 11 | ๐ tested | โ |
| scc | 12 | ๐ tested | โ |
| dijkstra | 11 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| dijkstra_heap | 11 | ๐ tested | โ |
| johnson | 11 | ๐ tested | โ |
| bidirectional_bfs | 13 | ๐ tested | โ |
| a_star | 11 | ๐ tested | โ |
| max_flow | 12 | ๐ tested | โ |
| advanced | 19 | ๐ tested | โ |
| kmp | 17 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| rabin_karp | 25 | ๐ tested | โ |
| suffix_array | 15 | ๐ tested | โ |
| z_function | 19 | ๐ tested | โ |
| manacher | 23 | ๐ tested | โ |
| gcd | 8 | ๐ถ ๅขๅผบ้ช่ฏ | โ |
| fast_power | 12 | ๐ถ ๅขๅผบ้ช่ฏ | โ |
| prime | 18 | ๐ tested | โ |
| miller_rabin | 11 | ๐ tested | โ |
| crt | 20 | ๐ tested | โ |
| array_sum | 7 | ๐ถ ๅขๅผบ้ช่ฏ | โ |
| dp | 21 | ๐ tested | โ |
| lis | 14 | ๐ tested | โ |
| convex_hull | 9 | ๐ tested | โ |
| andrew_hull | 11 | ๐ tested | โ |
| aho_corasick | 9 | ๐ tested | โ |
| min_cost_flow | 9 | ๐ tested | โ |
| two_sat | 8 | ๐ tested | โ |
| splay | 10 | ๐ tested | โ |
| bsgs | 8 | ๐ tested | โ |
| pollard_rho | 10 | ๐ tested | โ |
| kd_tree | 13 | ๐ tested | โ |
| rotating_calipers | 14 | ๐ tested | โ |
| euler_sieve | 11 | ๐ tested | โ |
| sparse_table | 13 | ๐ tested | โ generic |
| lca | 11 | ๐ tested | โ |
| dinic | 8 | ๐ tested | โ |
| closest_pair | 9 | ๐ tested | โ |
| segment_ops | 33 | ๐ tested | โ |
| combinatorics | 15 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| matrix | 12 | โ ๏ธ ้จๅ้ช่ฏ | โ |
| priority_queue | 15 | ๐ tested | โ HeapG[T] |
| monotonic | 21 | ๐ tested | โ |
| interval_dp | 22 | ๐ tested | โ |
| tree_dp | 19 | ๐ tested | โ |
| bridge_articulation | 15 | ๐ tested | โ |
| euler_path | 14 | ๐ tested | โ |
| hungarian | 10 | ๐ tested | โ |
| ntt | 11 | ๐ tested | โ |
| boyer_moore | 14 | ๐ tested | โ |
| lcp_array | 13 | ๐ tested | โ |
| suffix_automaton | 12 | ๐ tested | โ |
| segment_tree_lazy | 9 | ๐ tested | โ |
| suffix_tree | 12 | ๐ tested | โ |
| palindromic_tree | 11 | ๐ tested | โ |
| rolling_hash | 12 | ๐ tested | โ |
| lyndon | 13 | ๐ tested | โ |
| link_cut | 12 | ๐ tested | โ |
| persistent_vector | 9 | ๐ tested | โ |
| hopcroft_karp | 9 | ๐ tested | โ |
| stoer_wagner | 10 | ๐ tested | โ |
| max_clique | 12 | ๐ tested | โ |
| convex_hull_3d | 12 | ๐ tested | โ |
| half_plane_intersection | 9 | ๐ tested | โ |
| matrix_decomp | 16 | ๐ tested | โ |
| newton_method | 23 | ๐ tested | โ |
| berlekamp_massey | 10 | ๐ tested | โ |
| fft | 11 | ๐ tested | โ |
| simplex | 10 | ๐ tested | โ |
| digit_dp | 11 | ๐ tested | โ |
| w_tinylfu | 11 | ๐ tested | โ |
| ttl_cache | 10 | ๐ tested | โ |
| cuckoo_filter | 8 | ๐ tested | โ |
| count_min_sketch | 10 | ๐ tested | โ |
| hyperloglog | 10 | ๐ tested | โ |
| nim_sg | 13 | ๐ tested | โ |
| reservoir_sampling | 8 | ๐ tested | โ |
| int64_utils | 21 | ๐ tested | โ |
| Total | 6432 | 17 ๅ ้่ฟ moon prove๏ผ5 ๅฎๆด, 3 ๅขๅผบ, 9 ้จๅ๏ผ, ๅ ถไฝไป ๆต่ฏ้ช่ฏ | 17 generic |
ๆณจ๏ผไธ่กจไป ๅๅบ้จๅไปฃ่กจๆงๅ ใๅฎๆด 337 ไธชๅ ็ๆต่ฏ็ป่ฎก่ฏท่ฟ่ก moon test ๆฅ็ใ
#ๅ่่ตๆบ
- MoonBit ๅฝขๅผๅ้ช่ฏๆๆกฃ
- moonbit-community/verified โ ๅฎๆนๆ็จ็บง้ช่ฏ็คบไพ
- MoonBit 0.9 ๅๅธๅๅฎข
- Why3 ๆๆกฃ โ Why3 ้ช่ฏๅนณๅฐ
- Z3 SMT Solver โ SMT ๆฑ่งฃๅจ
- Okasaki, "Red-Black Trees in a Functional Setting" โ ็บข้ปๆ ๅฝๆฐๅผๆๅ ฅ็ฎๆณ
- Kahrs, "Red-Black Trees with Types" โ ็บข้ปๆ ๅฝๆฐๅผๅ ้ค็ฎๆณ
#่ฎธๅฏ่ฏ
Apache-2.0
Install
Download zipCore algorithms and data structures for MoonBit โ partially formally verified
moonbitformal-verificationmoon-provealgorithmsdata-structurespartially-verified
0.1.1
Apache-2.0
Updated 18 hours ago
6 downloads