Isinalin sa Filipino mula sa Summary: Formal Methods (Philipp Kant) ni @maki.mukai
Ito ay isinalin lamang sa Cardano Forum
Si Philipp Kant ay direktor ng Formal Methods sa IOHK. Maaari mong mahanap ang karagdagang mga detalye sa kanyang background at karanasan dito.
- Ang kanyang pangkat ay nakatuon sa pagpapakilala ng pormal na pamamaraan sa metodolohiya ng pagpapa-unlad software
- Ang ideya ng pangkat na ito ay tiyakin na ang mga resulta mula sa mga mananaliksik na kung saan ay nagsusulat ng mga papel at nagpapatunay ng mga aspeto ng protocol sa isang abstract na antas ay maaaring masalin sa isang bagay na maipapatupad sa makina at maaaring mapagana ang software
- Ang IOHK ay natatangi sa paggamit ng pormal na pamamaraan sa teknolohiya ng blockchain
- Ang mga pormal na pamamaraan ay karaniwang ginagamit sa mga industriya tulad ng aerospace o mga produktong medikal: mga sistema kung saan may mataas na halaga o nakakapinsala sa buhay na nakataya
- ang sistema ng blockchain ay may malaking halaga kaya't ito ang dahilan sa likod ng pagpapatupad nito
Sa video na ito, sinimulan ni Dr. Kant ang pagpapakilala sa Cardano at ang Proof-of-Stake protocol at pagkatapos ay humantong ito sa pagtatanghal sa pormal na pamamaraan. Tandaan na ito ay isang buod lamang dahil ang ilang mga seksyon ay mas mahusay na maunawaan sa pamamagitan ng panonood ng pagtatanghal kasama ang kanyang mga inihandang slide (code at mga graph).
Tungkol saan ang PoS?
- Ano ang gusto mong makamit sa isang cryptocurrency?
- desentralisasyon: isang currency na walang sentral na awtoridad, at ito ay nasa kamay ng mga gumagamit
- permission-less: lahat ay dapat na maaaring makasali, walang hadlang sa pagpasok
- isang matatag na ledger
- matiyaga: ang mga transaksyon na inilalagay sa ledger ay dapat manatili roon at hindi matanggal
- liveness: ang isinumite na mga transaksyon ay dapat na matapos sa ledger pagkatapos ng ilang oras
- ang lahat ng mga kailangan na ito ay mahirap matupad nang sabay-sabay - kailangan mo ng isang bagay na matatag na maaasahan ng lahat, ngunit ayaw mo ng isang sentral na katawan na kailangang magpasya at maging source ng tiwala na iyon
Paano ginawa ang tiwala sa Bitcoin Blockchain
- ang mga gumagamit ng Bitcoin ay nagpapadala ng mga transaksyon sa network
- ang mga transaksyon ay nilalagdaan gamit ang private key, kaya walang sino man ang makakagastos ng pera ng ibang tao
- nais ng mga tao na tiyakin na ang mga transaksyon na ipinadala ay kasama at ang mga ipinakitang transaksyon ay hindi mawawala sa ibang pagkakataon
- Ang mga transaksyon na ipinadala sa pinagsama-samang "blocks" na tulad ng mga pahina sa isang ledger
- pagkatapos ay inuutusan sila sa pamamagitan ng paglalagay ng mga blocks sa order: ang bawat block ay bumabase sa nakaraang block sa pamamagitan ng pagsama sa hash ng block na iyon
- Mahalaga ang pag-order dahil kung sinubukan ng isang tao na doblehin ang kanilang pera, kung mayroong isang order ay kinakailangan na pumili ng isang balidong transaksyon
- magkamit ng tiwala sa pamamagitan ng pagkakaroon karapatan ng bawat isa, sa halip na magkaroon ng isang sentral na tao
- sa pamamagitan ng pagkuha sa karapatan, kahit na may iilan na hindi gumaganap sa mga patakaran, ang magiging epekto ay mayroong isang matatag na ledger kung saan nakasama ang mga transaksyon
- pigilan ang mga transaksyon mula sa pagkawala kasama ang pinakamahabang chain rulw dahil ang isang tao ay kailangang magbalik sa mga block nang higit pa mapalalim ang chain upang maoverride ang anumang mga transaksyon
- pagiging perimission-less nang walang mga pagsusuri sa pagkakakilanlan ay nangangahulugang maaaring makapagrehistro nang maraming beses at ito ay isang problema kapag mayroong isang sistema na umaako sa tungkulin
- ito ay tinatawag na atakeng Sybil
- ang solusyon na ginagamit ng Bitcoin para sa problemang ito ay pagdaragdag ng isang gastos para sa pagrehistro
- ang gastos ay nasa anyong arbitrary mathematical puzzle
- ang ginagawa ng Bitcoin ay nagdaragdag ng isang arbitrary string ng data sa block at hash ng block ay may numero na pinangungunahan ng zero
- dahil hindi nababalik ang hash, hindi mo makakalkula kung ano ang mga bilang na ito at dapat subukan at subukang muli
- dapat kang gumastos ng hashing / computing power upang masubukan ang ilang data, makalkula ang hash ng block at kung hindi ito magkasya, kailangan mong subukang muli
- ang gastos na ito ay nagmamahal sa pag-atake sa network dahil kakailanganin mong magkaroon ng higit pang mga computer kaysa sa lahat ng tao sa system
Paano gumagana ang PoW
- mayroong isang randomized na halalan ng pinuno, kung saan para sa bawat CPU na idinagdag sa system, makakakuha ka ng isang boto
- ang pagkakataon na ma-boto ay proporsyonal sa kapangyarihan ng CPU na inilagay mo sa system
- ang mga nagwagi ay maaaring magsulat ng isang block at may mga gantimpala na nauugnay doon dahil sa patakaran ng 'longest chain wins’', mahirap ibalik ang mga dating block (maliban kung mayroon kang higit sa 50% ng CPU system)
- Mga problema sa Bitcoin:
- ang lakas ng hashing ay may malaking pagkonsumo ng enerhiya
- Ang pagkonsumo ng network ng Bitcoin ay maihahambing sa isang maliit na pambansang estado at lahat ay nasa isang medyo mababang rate ng transaksyon (~10 Tx/segundo)
- mahirap masukat ang sistema sa isang bagay na may mas mataas na rate ng transaksyon
- ang format ng tunggalian ay humahantong sa isang winner-takes-all system
- upang ma-maximize ang tsansa sa anumang gantimpala, ang mga tao ay nagtutulungan at bumubuo ng mga pool at ang mga pool na ito ay humantong sa sentralisasyon
Proof of Stake
- iba't ibang pagpili ng pinuno: tinimbang base sa stake!
- para sa bawat pwesto ng oras, ang protocol ay sapalarang pumili ng isang coin at ang may-ari ng coin ay mailalagay sa susunod na block
- upang magkaroon ng mas mataas na posibilidad na mapili, kailangan mong bumili ng higit pa sa pera at magiging mas mahal ito
- ngunit ito ay may karagdagang kalamangan dahil ito ay nakatali sa sistema mismo
- kung ikaw ay isang malaking stakeholder at mayroon kang maraming currency na ito, mayroon kang mas higit na pagkakataon na makontrol ito at tanggalin ang mga transaksyon ngunit hindi mo nais na gawin ito at kung napansin ito ng mga tao, bibigyan nito ang insentibo sa currency na iyon sa pagiging matapat, sa gayon ay makakabuo ng tiwala sa sistema
- ang dahilan na hindi pa ito ginagamit hanggang ngayon ay kailangan mo ng randomness para sa proseso ng halalan
- kailangan mo ng isang malinaw na random number generator → kailangan mong sumang-ayon sa mapagkukunan ng randomness ngunit kung gayon, kung mayroon kang isang sentral na awtoridad para sa random na generator, ang awtoridad na iyon ang kumokontrol sa isang malaking bahagi ng sistema
- ang ibang kadahilanan kaya hindi pa ginagamit ay naisip ng maraming tao na hindi ito ligtas dahil sa posibilidad na ang isang tao ay makahula sa random number generator
- kung paano ito gumagana ay ang mga coin sa system ay naka-linya, ang random na numero ay ginagawa at ang kaukulang nth na coin ay mapipili
- kung mahuhulaan mo ito, maaari mong kang magpadala ng coin sa buong sistema upang subukan at makakuha ng isang distribusyon upang ang iyong mga coin ay mailagay sa pwesto kung saan sila ay mapipili
- kaya ang kailangan mo ay: isang desentralisadong random number generator at isa na hindi nahuhulaan nang maaga
Ouroboros
- Ang isang bunga mula sa mga mananaliksik sa IOHK ay ang protocol ng Ouroboros, ang unang provably secure PoS protocol
- ang pananaliksik na ito ay isinumite para sa peer-review at naaprubahan
- sa paraang ng paggana nito: ang oras ng paghati sa mga slot at ang bawat slot ay may isang block> para sa bawat slot, ang isang stakeholder ay sapalarang maihahalal upang maging pinuno
- para doon, kailangan mo ng randomness
- upang magawa iyon, papangkatin ang mga slot sa epochs at bago magsimula ang isang epoch, ang lahat ng mga stakeholder ay dapat sumang-ayon sa seed para sa susunod na random number generator
- sa madaling salita ang mga stakeholder mismo ay pribado na nagpapaikot ng isang dice at gumawa ng randomness (at hindi ito ipinahayag sa ibang mga partido) at sa dulo, nagpadala sila ng patunay na alam na nila kung ano ang kanilang pinaikot at hindi na nila ito madadaya pa.
- sa sandaling ang stake para sa susunod na epoch ay malinaw na nakasaad, ang lahat ng mga random na numero ay ihahayag at pagsasamahin sa isang tinukoy na paraan at ngayon magkakaroon ka ng isang bagong seed
- ang seed na ito ay isang bagay na ang bawat isa ay may kakayahang maimpluwensyahan ngunit walang makakapaghula dahil batay ito sa maraming mga random na numero na ibinahagi
- ang protocol na ito ay napatunayan na ligtas laban sa sinumang kalaban na may mas mababa sa 50% ng stake (halaga ng Ada sa sistema)
Ouroboros Praos
- pagpapalawak ng protocol na may kinalaman sa tanong na "ano ang mangyayari kapag naantala ang mensahe?"
- dahil ang PoS protocol ay tumatalakay sa mga slot ng oras at oras at mayroong isang block para sa bawat slot...upang gumana ang chain, ang impormasyon ng huling block ay dapat magpalaganap sa buong network bago makuha ng susunod na pinuno ang kanyang gampanin, kung hindi, makakakuha ka ng awtomatikong fork
- sa totoong network, maaari kang magkaroon ng mga pagkaantala sa mensahe (tulad ng mga outage)
- Pinahaba ng Praos ang adversary na modelo upang maisama ang mga pagkaantala sa network
- ito ang kasalukuyang ipinatutupad para sa mga hinaharap na bersyon ng Cardano
Mula sa Papel hanggang sa Pagpapatupad
- ang pagsasalin ng mga papeles ng pananaliksik na nakasulat sa mga pormula sa wikang Ingles at matematika sa isang bagay na maaaring isagawa ng isang makina
- mayroong isang slot sa pagitan ng dalawang ito dahil ang papel ay isinulat para sa pag-unawa ng mga tao at ang mga glosses sa mga detalye na hindi kinakailangan para sa talakayan ngunit kinakailangan para sa pagpapatakbo ng isang protocol
- Publikasyon = mataas na antas ng abstraksyon, anv nakasulat sa simpleng Ingles at matematika na mga formula ay may mga patunay na seguridad
- vs. Code = ay tumatalakay sa lahat ng mga detalye at katumpakan, na nakasulat sa Haskell, kung mayroon kang code maaari mo rin bang ilipat ang mga patunay sa pagpapatupad?
Maliit na Hakbang - walang Malalaking Pagtalo
- ang mga maliliit na hakbang ay magiging mas madali upang matiyak na tama ang bawat hakbang na iyon
- ang unang hakbang ay a ang pagsalin ng algorithm sa isang pormal na wika (nang walang pagdaragdag ng anumang detalye - manatili sa parehong antas ng abstraksyon bilang papel) ngunit ang pagkuha sa isang bagay na maaaring mabasa at bigyang kahulugan ng isang makina
- sa sandaling mayroon kang eksakto ngunit abstrak na piraso, maaari mong simulan ang pagpipino at pagdaragdag ng mga detalye
- ang mga hakbang ay dapat sapat na maliit upang mapatunayan mo at masubukan na ang mga idinagdag na mga hakbang ay tama at huwag baguhin ang protocol sa maling paraan
- kasabay ng bawat hakbang, ginagawa ang mga similasyon at pagsubok
Prosesong Calculi
- ang unang hakbang ay ang pagsasalin sa pormal na wika
- at ano ang dapat na wikang iyon?
- sa blockchain, mayroon kang maraming mga computer na nakikipag-usap at nagsasagawa ng isang ipinamamahaging pagkalkula ng ledger
- Sa agham ng kompyuter, ang proseso ng calculi ay isang magkakaibang pamilya ng mga kaugnay na pamamaraan para sa pormal na pagmomolde ng mga kasabay na sistema
- ang proseso ng calculus na pinili ay tinatawag na Psi Calculus (isang parametric na pamilya ng proseso ng calculi)
Embedded Domain Specific Languages (EDSLs)
- nais na i-embed ang prosesong ito sa wikang Haskell
- maaari mong basahin ang pagsulat sa anumang wika, ngunit mas madaling mangatuwiran kung umaangkop ang wika sa domain
- mga halimbawa nito: Ang Postkrip para sa paglalarawan ng mga pahina ng teksto o graphics, SQL para sa mga database
- para sa isang naka-embed na DSL → lumikha ng wika sa loob ng ibang wika at maaari mong gamitin ang syntax at istruktura ng host ng wika at pagkatapos ay ang programa mismo bilang isang termino ng data sa loob ng wikang iyon
- pinapayagan ng naka-embed na DSL para sa maraming mga interpretasyon
Pag-embed ng Psi sa Haskell
- ipatupad ang Psi Calculus bilang isang EDSL sa Haskell, at pagkatapos ay isulat ang Ouroboros Praos sa wikang ito
-
pagkatapos sa pamamagitan ng pagsulat ng iba't ibang mga tagasalin para sa wika maaari mong:
- gumamit ng mga simulator para sa programa
- o i-export sa isang syntax ng proof of system (tulad ng Isabelle o Coq)
- o magkaroon ng isang tagasalin na nagpapatakbo ng buong bagay at magdagdag ng mga detalye sa at sa huli ay magiging produksyon ng code
Modelling Performance (at Kabiguan)
- ang kailangan natin sa PoS protocol ay isang mahusay na paghawak sa pagsasagawa ng sistema
- bago ang paglulunsad, nakatakda ang mga benchmark
- may mga node na tumatakbo sa iba't ibang mga kontinente at pagtaas ng presyon sa pamamagitan ng pagpapadala ng mga transaksyon, at paghahanap kung saan maaaring mai-tono ang mga parameter upang mapalago ang throughput
- Nais ng IOHK ang paghawak hindi lamang mula sa pag-eksperimento kundi mula sa teorya din kung gaano kahusay ang dapat sa pagpapatakbo sa code na ito
- sa pag-eksperimento, nakakakuha ka ng mga benchmarking data ngunit kailangan mong mas mahusay na maunawaan kung bakit iyon ang kaso o kung ano ang pinakamainam
- pagkatapos ay maaari mong sagutin ang mga katanungan sa protocol tulad ng:
- Gaano katagal bago maitala ang mga transaksyon?
- Gaano katagal aabutin upang makasali sa network?
- Maaari bang magpalaganap ang mga block sa buong network sa isang solong slot?
- Ano ang mga mapagkukunan kinakailangan para sa isang node?
Kahinaan ng Kalidad: ΔQ
- oras laban sa posibilidad ng isang tiyak na oras, ang ilang kaganapan ay nangyari
- sa perpektong sistema, magkakaroon ka ng isang linya na malapit sa 1 sa ilang mga punto
- ang mga tunay na sistema ng mundo ay maaaring mabigo, ay karaniwang ay hindi naaabot ang 1 at napupuspos sa isang mas mababang antas at ang pagkakaiba sa pagitan ng linyang ito at 1 ay ang iyong magiging pagkakataon ng pagkabigo kung maghintay ka ng isang arbitrary na dami ng oras = hindi wastong Cumulative Distribution Function
- ito ay isang bagay na maaaring maging modelo sa Haskell
- ginagawa ito sa pamamagitan ng pagtatakda ng ΔQ bilamh function na tumatagal ng estado ng random number generator
- Ang mga formula ng ΔQ ay maaaring magamit para sa paggaya ngunit para din sa pangangatwiran nito algebraically
- ginagamit ito kapag tinitingnan ang iba't ibang mga sitwasyon tulad ng parallel o sequential composition
Ang Pagpapatupad ng Mataas na Katiyakang Blockchain
- Ang mga cryptocurrency ay nagdadala ng malaking halaga
- kaya iniisip ng IOHK na nararapat na gawin ang mga bagay na may malaking antas ng katiyakan
- pinatunayan ng mga mananaliksik na ang mga bagay tungkol sa protocol ngunit kailangan ding tiyakin na ang mga patunay ay hindi nawawala sa mga pagsasalin
- mayroon ding mga panukala para sa paggamit ng blockchain para sa mga kritikal na imprastraktura tulad ng land deeds
- samakatuwid, kailangan nating magkaroon ng mga sistema na akma para sa hangarin na idinisenyo para sa pagsasagawa habang ito ay bahagyang ligtas