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 |