issues Search Results · repo:runtimeverification/evm-semantics language:Python
Filter by
0 results
(68 ms)0 results
inruntimeverification/evm-semantics (press backspace or delete to remove)This PR reduce time consumption for Test PR / Proofs: Summarization (pull_request) from 4 hours to 10 minutes just by
changing the max_depth from 1000 to 1.
I think it should be a problem in Haskell Backend ...
bug
enhancement
haskell backend
Stevengre
- 1
- Opened 14 days ago
- #2719
What is an opcode summary
For this opcode, the backend can rewrite one step to execute it. It could be several rules.
Why we need summaries
It s important to provide summaries for all EVM opcodes, because: ...
enhancement
- 2
- Opened on Feb 13
- #2705
I tried building the semantics on my Ubuntu 24.04.1 laptop and during the blockchain plugin step
poetry -C kevm-pyk run kdist --verbose build evm-semantics.plugin
I was consistently getting errors of ...
bug
JuanCoRo
- Opened on Jan 13
- #2678
Maybe you can try:
kup install k.openssl.secp256k1 --version v$(cat deps/k_release)
Because the llvm-kompile will need to link the secp256k1 libiary.
- Opened on Jan 7
- #2677
The sum-to-n-foundry-spec.k file contains a circular proof of the usual sum of the first n integers. Currently, at the
critical point, the branching that happens is unexpected to me and appears to require ...
bug
PetarMax
- 7
- Opened on Sep 10, 2024
- #2617
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 ...
aa755
- 2
- Opened on Aug 5, 2024
- #2552
Now that we support symbolic parameters in constructors, we need lemmas to simplify expressions such as `
#dasmOpCode ( b `\xc0`@R`\x01`\x01`\xf8\x1b\x03`\x80R4\x80\x15a\x00\x1bW`\x00\x80\xfd[P`@Qa\x01^8\x03\x80a\x01^\x839\x81\x01`@\x81\x90Ra\x00:\x91a\x00BV[`\xa0Ra\x00[V[`\x00` ...
palinatolmach
- Opened on Jun 11, 2024
- #2476
The two attributes klabel(_) and symbol will eventually be deprecated. The K code should be updated to use the symbol(_)
attribute instead.
enhancement
anvacaru
- 1
- Opened on Jun 4, 2024
- #2462
Consider e.g.:
https://github.com/runtimeverification/evm-semantics/blob/97be05c231969628712e4564797dc7ff3cb8485a/kevm-pyk/src/kevm_pyk/kevm.py#L552
Find the corresponding production:
https://github.com/runtimeverification/evm-semantics/blob/97be05c231969628712e4564797dc7ff3cb8485a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md?plain=1#L26 ...
enhancement
good first issue
tothtamas28
- Opened on May 31, 2024
- #2456
As a follow-up to https://github.com/runtimeverification/evm-semantics/pull/2417, @tothtamas28 suggest we should do the
following:
As I see it, tests basically require an interface that takes a Target ...
geo2a
- Opened on May 9, 2024
- #2419
Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Press the /
key to activate the search input again and adjust your query.Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Restrict your search to the title by using the in:title qualifier.