using this semantics in Coq
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 20/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Da chiarire
- Stato di attività
- Ferma
- Ambito
- blockchain, compilers
Direzione di ricerca
L’issue non indica file, test o punti di ingresso. Inizia esaminando i repository KEVM e K alla ricerca di lavori esistenti di traduzione in Coq o di integrazione delle dimostrazioni, quindi determina se un traduttore generico rientra nell’ambito. Il lavoro è completato quando esiste un percorso documentato e concordato per usare KEVM in Coq oppure un piano di implementazione chiaramente definito.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Has anyone explored how to use the KEVM semantics in Coq? Is there a generic K to Coq translator or has someone written a specific translation for KEVM?
I would like to use this semantics to prove correctness of an implementation of an optimized EVM interpretor or jit compliler.
- Lingua principale
- KCL
- Stelle
- 595
- Fork
- 159
- Merge medio
- 4g 3h
- PR unite (30g)
- 1
Preparare l'ambiente
Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·
Tutte le issue di runtimeverification/evm-semantics
Issue simili
-
consensus feature I2 S4 U2
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 85/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
erigontech/erigon#25362 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
paritytech/polkadot-sdk#13579 ·
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 68/100
status-im/nimbus-eth2#9379 ·
I maintainer di solito rispondono entro 1 giorno
-
documentation good first issue
Difficoltà 2/5 1-3 ore Idoneità per principianti 74/100
InfiniteZeroFoundation/DevNet#285 ·
I maintainer di solito rispondono entro 1 giorno