formal-land coq-of-rust issues

formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

GNU Affero General Public License v3.0

418 stars 14 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

suggestion: definition of 'binop_int'

#621 clarus opened 1 week ago
0
move-sui: add simulation for the cast_u8 instruction

#620 clarus opened 1 week ago
0
Draft: Complete interpreter instructions to the end

#619 Mushow closed 1 week ago
0
Draft: Implement IntegerValue module for arithmetic operations in the interpreter

#618 Mushow closed 2 weeks ago
0
move-sui: fix remaining tests

#617 clarus closed 2 weeks ago
0
Complete interpreter instructions at the end

#616 clarus opened 2 weeks ago
0
move-sui: More simulations for verify

#615 clarus closed 2 weeks ago
0
Implementation of the VMControlFlowGraph's new function

#614 Mushow closed 2 weeks ago
0
Draft: experiments around stack semantics

#613 clarus opened 4 weeks ago
0
Misc problems for `interpreter` simulation

#612 InfiniteEchoes opened 1 month ago
3
Add an example of test in Coq for the type-checker

#611 clarus closed 3 weeks ago
0
Move - Simulations - Porting the type-checker's tests

#610 clarus closed 2 weeks ago
2
clean: remove the old move/ folder to avoid confusion

#609 clarus closed 1 month ago
0
Draft: add links generation from JSON and Python

#608 clarus opened 1 month ago
0
`interpreter` simulation, part 2

#607 InfiniteEchoes closed 1 month ago
1
Upgrade to rustc nightly-2024-08-26

#606 clarus closed 1 month ago
0
Move - Translations - Add to the CI

#605 clarus closed 2 months ago
1
Add handling of polymorphic constants

#604 clarus closed 2 months ago
1
Add definition of links

#603 clarus closed 1 month ago
0
Add translation of the Move code in the CI

#602 clarus closed 2 months ago
1
Proposal: monad with `coerce`?

#601 InfiniteEchoes opened 2 months ago
3
`interpreter` simulation, Part 1

#600 InfiniteEchoes closed 1 month ago
0
[Duplicated]Move - Simulations - Interpreter

#599 InfiniteEchoes closed 2 months ago
1
Move - Simulations - `loader`

#598 InfiniteEchoes opened 2 months ago
0
Move - Simulations - Type

#597 InfiniteEchoes opened 2 months ago
0
Move - Simulations - Locals

#596 InfiniteEchoes opened 2 months ago
0
move: simulate the 'verify' function

#595 clarus closed 2 months ago
0
Move - Simulations - Verifier - verify function

#594 clarus closed 2 months ago
0
Move - Simulations - Interpreter

#593 clarus opened 2 months ago
2
Like "`verify_instr` simulation" PR with rebase

#592 clarus closed 2 months ago
1
Specialized monadic operations for `StatePanic` monad with `Result` return type

#591 olympichek closed 2 months ago
0
`verify_instr` simulation

#590 InfiniteEchoes closed 2 months ago
1
WSL build instruction, part 2

#589 InfiniteEchoes closed 2 months ago
0
Add build Instructions for Windows environment with WSL

#588 InfiniteEchoes closed 2 months ago
0
More on `type_safety`, Part 4

#587 InfiniteEchoes closed 2 months ago
0
Add more generic `panic_any` operation to the `StatePanic` monad

#586 olympichek closed 2 months ago
0
Misc updates

#585 InfiniteEchoes closed 2 months ago
0
More on `type_safety`, part 3

#584 InfiniteEchoes closed 2 months ago
0
Move `AbstractStack` Tests

#583 olympichek closed 3 months ago
1
Move - Simulations - Verifier - Meter trait

#582 InfiniteEchoes closed 2 months ago
0
Simulations for `AbstractStack` type and methods #2

#581 olympichek closed 3 months ago
0
Simulation on `type_safety` and general `Move-sui`, part 2

#580 InfiniteEchoes closed 3 months ago
0
Various updates of monads and lenses for simulations

#579 olympichek closed 4 months ago
2
`type_safety` simulation with other dependencies

#578 InfiniteEchoes closed 3 months ago
0
Simulations for `AbstractStack` type

#577 olympichek closed 3 months ago
0
Initial draft for `move-sui`'s `Bytecode` type

#576 InfiniteEchoes closed 4 months ago
0
Move - Simulations - Verifier - verify_instr function

#575 clarus closed 2 months ago
0
Move - Simulations - Verifier - call function

#574 clarus closed 2 months ago
1
Move - Simulations - Verifier - borrow functions

#573 clarus closed 3 months ago
1
Move - Simulations - Verifier - TypeSafetyChecker

#572 clarus closed 3 months ago
1