Updated on 2022-06-10 10:15:38 UTC
refreshed every 30 minutes

Everybody's actions on nomadic-labs/mi-cho-coq (118)

Resource Action Who and why
nomadic-labs/mi-cho-coq!118
Arvid@dexter lemmas and refactorings
Blocking nomadic-labs/mi-cho-coq!100
Reply to thread @arvidnlarvidnl is the original author
Add a merge-team reviewer @arvidnlarvidnl is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq#47
Verify Dexter/CPMM
smart-contract verification
Blocking nomadic-labs/mi-cho-coq#56
Solve issue @arvidnlarvidnl is assigned
nomadic-labs/mi-cho-coq!137
FA1.2 verification v2
formalisation
Act @ksojakovaksojakova is assigned
Fix CI @rafoo_rafoo_ pushed recently and triggered last pipeline
Add a merge-team reviewer @rafoo_rafoo_ pushed recently
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!70
Certification of the specialised multisig
smart-contract verification
Close or reply to thread @rafoo_rafoo_ is the thread author
Add a merge-team reviewer @rafoo_rafoo_ is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!151
Fix #66 and #67
bug test
Review or approve @clarus1clarus1 is assigned
Add a merge-team reviewer @rafoo_rafoo_ is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!62
Functional proof of guestbook contract and simple lifetime property
smart-contract verification
Close or reply to thread @rafoo_rafoo_ is the thread author
Reply to thread @arvidnlarvidnl is the original author
Add a merge-team reviewer @arvidnlarvidnl is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!59
Add specialized multisig source
doc smart-contract verification
Close or reply to thread @rafoo_rafoo_ is the thread author
Reply to thread @rafoo_rafoo_ pushed recently
Add a merge-team reviewer @rafoo_rafoo_ pushed recently
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!98
Dexter 1.1 verification
Close or reply to thread @arvidnlarvidnl is the thread author
Fix CI @rafoo_rafoo_ is the original author and triggered last pipeline
Add a merge-team reviewer @rafoo_rafoo_ is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!113
Replace String.string_dec by String.eqb in Dexter 2
Fix CI @clarus1clarus1 is the original author and triggered last pipeline
Add a merge-team reviewer @clarus1clarus1 is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!149
Kristina@ctez
Fix CI @ksojakovaksojakova is the original author and triggered last pipeline
Add a merge-team reviewer @ksojakovaksojakova is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!152
[README] fix broken link to Michelson spec
Fix CI @asaueasaue is the original author and triggered last pipeline
Add a merge-team reviewer @asaueasaue is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!155
Adding support for 8.14
Fix CI @emarzionemarzion is the original author and triggered last pipeline
Add a merge-team reviewer @emarzionemarzion is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
Wait for pipeline @emarzionemarzion is the original author
nomadic-labs/mi-cho-coq!100
Dexter 2 verification (Dexter/FA1.2LQT, Dexter 1.5)
dexter2 smart-contract verification
Blocked by nomadic-labs/mi-cho-coq!118
Unblock @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!57
Integrate the output of coq-of-ocaml with the interpreter
coq-of-ocaml 🐓
Add a merge-team reviewer @clarus1clarus1 is the original author
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq!71
Dexter verification
smart-contract verification
Add a merge-team reviewer @arvidnlarvidnl @colin.gcolin.g pushed recently
Help add merge-team reviewers @davdumasdavdumas @jgonlabsjgonlabs @klakplokklakplok @MBourgoinMBourgoin @nguyencharles.nlabsnguyencharles.nlabs @OanaLPOanaLP @onurbonurb @pirbopirbo @raphael-proustraphael-proust @romain.nlromain.nl @SamREyeSamREye @vbotbolvbotbol is a dispatcher
nomadic-labs/mi-cho-coq#37
Simplification of the formula produced by eval_precond for `COMPARE; EQ`
smart-contract verification Todo
Complete task @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#51
Verify Dexter 2 (Dexter/FA1.2LQT, Dexter 1.5)
smart-contract verification
Complete task @arvidnlarvidnl @colin.gcolin.g @ksojakovaksojakova @tomjacktomjack is assigned
nomadic-labs/mi-cho-coq#1
nomadic-labs/mi-cho-coq#1
formalisation gas Todo
Solve issue @julien.tjulien.t is assigned
nomadic-labs/mi-cho-coq#2
nomadic-labs/mi-cho-coq#2
Todo
Solve issue @arvidnlarvidnl is assigned
nomadic-labs/mi-cho-coq#3
nomadic-labs/mi-cho-coq#3
coq-of-ocaml 🐓 Doing
Solve issue @clarus1clarus1 is assigned
nomadic-labs/mi-cho-coq#20
Verify the dexter contract
Doing smart-contract verification
Solve issue @arvidnlarvidnl @onurbonurb @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#22
nomadic-labs/mi-cho-coq#22
Done smart-contract verification
Solve issue @onurbonurb is assigned
nomadic-labs/mi-cho-coq#23
nomadic-labs/mi-cho-coq#23
Todo
Solve issue @julien.tjulien.t is assigned
nomadic-labs/mi-cho-coq#25
TZT support
Doing test
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#30
Delay monad
formalisation Todo
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#38
Support type assertions using `CAST`
formalisation Todo
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#39
Simplify the optimizer proof
optimizer Todo
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#40
Formalize the FA1.2 specification and verify an implementation
formalisation smart-contract verification
Solve issue @arvidnlarvidnl @ksojakovaksojakova is assigned
nomadic-labs/mi-cho-coq#45
Formalize the FA2 specification and verify implementations
formalisation smart-contract verification
Solve issue @arvidnlarvidnl @ksojakovaksojakova is assigned
nomadic-labs/mi-cho-coq#46
Specify and verify Dexter/FA2
formalisation smart-contract verification
Solve issue @arvidnlarvidnl @ksojakovaksojakova is assigned
nomadic-labs/mi-cho-coq#57
Generate and publish HTML documentation
beginner build ci
Solve issue @yrgyrg is assigned
nomadic-labs/mi-cho-coq#58
Simplify usage of set and map modules
framework
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#63
Bug regarding lambdas as part of data
bug framework
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#66
The typing rule for comb UPDATE is wrong
bug
Solve issue @rafoo_rafoo_ is assigned
nomadic-labs/mi-cho-coq#56
Adapt Dexter2 development for liquidity baking
dexter2 smart-contract verification
Blocked by nomadic-labs/mi-cho-coq#47
Unblock @yrgyrg is assigned
nomadic-labs/mi-cho-coq#62
Follow-up from "[README] add a description for the vesting contract"
Complete task @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#24
Modelize the blockchain and lifetime properties of contracts
Doing
Solve issue @arvidnlarvidnl opened issue and no one is assigned
nomadic-labs/mi-cho-coq#29
Formalize big maps
beginner formalisation Todo
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#32
nomadic-labs/mi-cho-coq#32
optimizer Todo
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#33
Documentation on generic_multisig
Solve issue @krixtrkrixtr opened issue and no one is assigned
nomadic-labs/mi-cho-coq#41
More lemmas for smart contract verification
Solve issue @arvidnlarvidnl opened issue and no one is assigned
nomadic-labs/mi-cho-coq#43
nomadic-labs/mi-cho-coq#43
doc
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#44
Link to the academical papers in the README
Solve issue @francoisfrancois opened issue and no one is assigned
nomadic-labs/mi-cho-coq#48
Describe vesting contract in README when dev is merged into master
Solve issue @arvidnlarvidnl opened issue and no one is assigned
nomadic-labs/mi-cho-coq#50
Make the CI Great Again -- brainstorming on how to improve the current situation
ci
Solve issue @arvidnlarvidnl opened issue and no one is assigned
nomadic-labs/mi-cho-coq#52
Make it easier to correlate smart contract verification developments with contract scripts
Solve issue @arvidnlarvidnl opened issue and no one is assigned
nomadic-labs/mi-cho-coq#59
Formalize serialization (PACK and UNPACK)
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#60
Concert integration
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#61
Move big proofs in a separate repo
Solve issue @onurbonurb opened issue and no one is assigned
nomadic-labs/mi-cho-coq#64
Types in OCaml and not in Mi-Cho-Coq
Solve issue @clarus1clarus1 opened issue and no one is assigned
nomadic-labs/mi-cho-coq#67
Numbers should be allowed as input syntax for BLS12-381 field elements.
bug
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq#68
Representation of BLS12-381
Solve issue @rafoo_rafoo_ opened issue and no one is assigned
nomadic-labs/mi-cho-coq!147
Draft: Update manager.tz
UnWIP @nuget.orgnuget.org is the original author
nomadic-labs/mi-cho-coq!153
Draft: Formalize the FA2 specification and verify implementations
Act @ksojakovaksojakova is assigned
Close or reply to thread @asaueasaue is the thread author
Close or reply to thread @asaueasaue is the thread author
UnWIP @asaueasaue pushed recently
nomadic-labs/mi-cho-coq!6
WIP: Documentation of the proof of the multisig contract
doc smart-contract verification
Reply to thread @rafoo_rafoo_ is the original author
Reply to thread @rafoo_rafoo_ is the original author
Reply to thread @rafoo_rafoo_ is the original author
Reply to thread @rafoo_rafoo_ is the original author
Reply to thread @rafoo_rafoo_ is the original author
Close or reply to thread @onurbonurb is the thread author
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!103
WIP: Optimize Michelson lexical analysis
dexter2
Reply to thread @yrgyrg is the original author
Reply to thread @yrgyrg is the original author
UnWIP @yrgyrg is the original author
nomadic-labs/mi-cho-coq!99
Draft: [dexter/fa2] add a hackish version of fa2 def/spec
smart-contract verification
Fix CI @arvidnlarvidnl is the original author and triggered last pipeline
UnWIP @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!143
WIP: typeclass for comparability
framework
Fix CI @rafoo_rafoo_ is the original author and triggered last pipeline
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!124
Draft: Adapt Dexter2 proofs for CPMM2
dexter2 smart-contract verification
Complete task @arvidnlarvidnl is the original author
UnWIP @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!119
Draft: [ci] add cache opam directory
ci
Close or reply to thread @rafoo_rafoo_ is the thread author
UnWIP @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!65
WIP: Michocoq Syntax: notation to ease annotations
Fix CI @julien.tjulien.t is the original author and triggered last pipeline
UnWIP @julien.tjulien.t is the original author
nomadic-labs/mi-cho-coq!67
WIP: Tzt support
Doing formalisation test
Fix CI @rafoo_rafoo_ is the original author and triggered last pipeline
Complete task @rafoo_rafoo_ is the original author
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!121
Draft: Arvid@re organize contracts coq
Complete task @arvidnlarvidnl is the original author
UnWIP @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!28
WIP: Model crypto nonces generated when operations are forged
formalisation
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!52
WIP: Beginning of import of the evaluation function
coq-of-ocaml 🐓
UnWIP @clarus1clarus1 is the original author
nomadic-labs/mi-cho-coq!92
WIP: Add admin-lambda contract
UnWIP @michaeljkleinmichaeljklein is the original author
nomadic-labs/mi-cho-coq!95
Draft: Dexter/CPMM verification
smart-contract verification
UnWIP @arvidnlarvidnl is the original author
nomadic-labs/mi-cho-coq!144
Draft: michelson2micheline (micheline2michelson x) = Return x
framework
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!148
Draft: [michocoq] use instruction instead of instruction_seq for the code part of scripts
UnWIP @rafoo_rafoo_ is the original author
nomadic-labs/mi-cho-coq!156
Draft: make Mi-cho-coq maps more usable
UnWIP @ksojakovaksojakova is the original author