nomadic-labs/mi-cho-coq!118 Arvid@dexter lemmas and refactorings Blocking
nomadic-labs/mi-cho-coq!100
|
Reply to thread
|
arvidnl
is the original author |
Add a merge-team reviewer
|
arvidnl
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq#47 Verify Dexter/CPMM smart-contract verification
Blocking
nomadic-labs/mi-cho-coq#56
|
Solve issue
|
arvidnl
is assigned |
nomadic-labs/mi-cho-coq!137 FA1.2 verification v2 formalisation
|
Act
|
ksojakova
is assigned |
Fix CI
|
rafoo_
pushed recently and triggered last pipeline |
Add a merge-team reviewer
|
rafoo_
pushed recently |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!70 Certification of the specialised multisig smart-contract verification
|
Close or reply to thread
|
rafoo_
is the thread author |
Add a merge-team reviewer
|
rafoo_
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!151 Fix #66 and #67 bug
test
|
Review or approve
|
clarus1
is assigned |
Add a merge-team reviewer
|
rafoo_
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
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_
is the thread author |
Reply to thread
|
arvidnl
is the original author |
Add a merge-team reviewer
|
arvidnl
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!59 Add specialized multisig source doc
smart-contract verification
|
Close or reply to thread
|
rafoo_
is the thread author |
Reply to thread
|
rafoo_
pushed recently |
Add a merge-team reviewer
|
rafoo_
pushed recently |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!98 Dexter 1.1 verification
|
Close or reply to thread
|
arvidnl
is the thread author |
Fix CI
|
rafoo_
is the original author and triggered last pipeline |
Add a merge-team reviewer
|
rafoo_
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!113 Replace String.string_dec by String.eqb in Dexter 2
|
Fix CI
|
clarus1
is the original author and triggered last pipeline |
Add a merge-team reviewer
|
clarus1
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!149 Kristina@ctez
|
Fix CI
|
ksojakova
is the original author and triggered last pipeline |
Add a merge-team reviewer
|
ksojakova
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!152 [README] fix broken link to Michelson spec
|
Fix CI
|
asaue
is the original author and triggered last pipeline |
Add a merge-team reviewer
|
asaue
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!155 Adding support for 8.14
|
Fix CI
|
emarzion
is the original author and triggered last pipeline |
Add a merge-team reviewer
|
emarzion
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
Wait for pipeline
|
emarzion
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
|
arvidnl
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
|
clarus1
is the original author |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
is a dispatcher |
nomadic-labs/mi-cho-coq!71 Dexter verification smart-contract verification
|
Add a merge-team reviewer
|
arvidnl
colin.g
pushed recently |
Help add merge-team reviewers
|
davdumas
jgonlabs
klakplok
MBourgoin
nguyencharles.nlabs
OanaLP
onurb
pirbo
raphael-proust
romain.nl
SamREye
vbotbol
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_
is assigned |
nomadic-labs/mi-cho-coq#51 Verify Dexter 2 (Dexter/FA1.2LQT, Dexter 1.5) smart-contract verification
|
Complete task
|
arvidnl
colin.g
ksojakova
tomjack
is assigned |
nomadic-labs/mi-cho-coq#1 nomadic-labs/mi-cho-coq#1 formalisation
gas
Todo
|
Solve issue
|
julien.t
is assigned |
nomadic-labs/mi-cho-coq#2 nomadic-labs/mi-cho-coq#2 Todo
|
Solve issue
|
arvidnl
is assigned |
nomadic-labs/mi-cho-coq#3 nomadic-labs/mi-cho-coq#3 coq-of-ocaml 🐓
Doing
|
Solve issue
|
clarus1
is assigned |
nomadic-labs/mi-cho-coq#20 Verify the dexter contract Doing
smart-contract verification
|
Solve issue
|
arvidnl
onurb
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#22 nomadic-labs/mi-cho-coq#22 Done
smart-contract verification
|
Solve issue
|
onurb
is assigned |
nomadic-labs/mi-cho-coq#23 nomadic-labs/mi-cho-coq#23 Todo
|
Solve issue
|
julien.t
is assigned |
nomadic-labs/mi-cho-coq#25 TZT support Doing
test
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#30 Delay monad formalisation
Todo
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#38 Support type assertions using `CAST` formalisation
Todo
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#39 Simplify the optimizer proof optimizer
Todo
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#40 Formalize the FA1.2 specification and verify an implementation formalisation
smart-contract verification
|
Solve issue
|
arvidnl
ksojakova
is assigned |
nomadic-labs/mi-cho-coq#45 Formalize the FA2 specification and verify implementations formalisation
smart-contract verification
|
Solve issue
|
arvidnl
ksojakova
is assigned |
nomadic-labs/mi-cho-coq#46 Specify and verify Dexter/FA2 formalisation
smart-contract verification
|
Solve issue
|
arvidnl
ksojakova
is assigned |
nomadic-labs/mi-cho-coq#57 Generate and publish HTML documentation beginner
build
ci
|
Solve issue
|
yrg
is assigned |
nomadic-labs/mi-cho-coq#58 Simplify usage of set and map modules framework
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#63 Bug regarding lambdas as part of data bug
framework
|
Solve issue
|
rafoo_
is assigned |
nomadic-labs/mi-cho-coq#66 The typing rule for comb UPDATE is wrong bug
|
Solve issue
|
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
|
yrg
is assigned |
nomadic-labs/mi-cho-coq#62 Follow-up from "[README] add a description for the vesting contract"
|
Complete task
|
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
|
arvidnl
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#29 Formalize big maps beginner
formalisation
Todo
|
Solve issue
|
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_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#33 Documentation on generic_multisig
|
Solve issue
|
krixtr
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#41 More lemmas for smart contract verification
|
Solve issue
|
arvidnl
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#43 nomadic-labs/mi-cho-coq#43 doc
|
Solve issue
|
rafoo_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#44 Link to the academical papers in the README
|
Solve issue
|
francois
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
|
arvidnl
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
|
arvidnl
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
|
arvidnl
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#59 Formalize serialization (PACK and UNPACK)
|
Solve issue
|
rafoo_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#60 Concert integration
|
Solve issue
|
rafoo_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#61 Move big proofs in a separate repo
|
Solve issue
|
onurb
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#64 Types in OCaml and not in Mi-Cho-Coq
|
Solve issue
|
clarus1
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_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq#68 Representation of BLS12-381
|
Solve issue
|
rafoo_
opened issue and no one is assigned |
nomadic-labs/mi-cho-coq!147 Draft: Update manager.tz
|
UnWIP
|
nuget.org
is the original author |
nomadic-labs/mi-cho-coq!153 Draft: Formalize the FA2 specification and verify implementations
|
Act
|
ksojakova
is assigned |
Close or reply to thread
|
asaue
is the thread author |
Close or reply to thread
|
asaue
is the thread author |
UnWIP
|
asaue
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_
is the original author |
Reply to thread
|
rafoo_
is the original author |
Reply to thread
|
rafoo_
is the original author |
Reply to thread
|
rafoo_
is the original author |
Reply to thread
|
rafoo_
is the original author |
Close or reply to thread
|
onurb
is the thread author |
UnWIP
|
rafoo_
is the original author |
nomadic-labs/mi-cho-coq!103 WIP: Optimize Michelson lexical analysis dexter2
|
Reply to thread
|
yrg
is the original author |
Reply to thread
|
yrg
is the original author |
UnWIP
|
yrg
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
|
arvidnl
is the original author and triggered last pipeline |
UnWIP
|
arvidnl
is the original author |
nomadic-labs/mi-cho-coq!143 WIP: typeclass for comparability framework
|
Fix CI
|
rafoo_
is the original author and triggered last pipeline |
UnWIP
|
rafoo_
is the original author |
nomadic-labs/mi-cho-coq!124 Draft: Adapt Dexter2 proofs for CPMM2 dexter2
smart-contract verification
|
Complete task
|
arvidnl
is the original author |
UnWIP
|
arvidnl
is the original author |
nomadic-labs/mi-cho-coq!119 Draft: [ci] add cache opam directory ci
|
Close or reply to thread
|
rafoo_
is the thread author |
UnWIP
|
arvidnl
is the original author |
nomadic-labs/mi-cho-coq!65 WIP: Michocoq Syntax: notation to ease annotations
|
Fix CI
|
julien.t
is the original author and triggered last pipeline |
UnWIP
|
julien.t
is the original author |
nomadic-labs/mi-cho-coq!67 WIP: Tzt support Doing
formalisation
test
|
Fix CI
|
rafoo_
is the original author and triggered last pipeline |
Complete task
|
rafoo_
is the original author |
UnWIP
|
rafoo_
is the original author |
nomadic-labs/mi-cho-coq!121 Draft: Arvid@re organize contracts coq
|
Complete task
|
arvidnl
is the original author |
UnWIP
|
arvidnl
is the original author |
nomadic-labs/mi-cho-coq!28 WIP: Model crypto nonces generated when operations are forged formalisation
|
UnWIP
|
rafoo_
is the original author |
nomadic-labs/mi-cho-coq!52 WIP: Beginning of import of the evaluation function coq-of-ocaml 🐓
|
UnWIP
|
clarus1
is the original author |
nomadic-labs/mi-cho-coq!92 WIP: Add admin-lambda contract
|
UnWIP
|
michaeljklein
is the original author |
nomadic-labs/mi-cho-coq!95 Draft: Dexter/CPMM verification smart-contract verification
|
UnWIP
|
arvidnl
is the original author |
nomadic-labs/mi-cho-coq!144 Draft: michelson2micheline (micheline2michelson x) = Return x framework
|
UnWIP
|
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_
is the original author |
nomadic-labs/mi-cho-coq!156 Draft: make Mi-cho-coq maps more usable
|
UnWIP
|
ksojakova
is the original author |