Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / leanprover/lnsym issues and pull requests
#101 - Add ELFLoader test for AES-GCM assembly routines
Pull Request -
State: closed - Opened by pennyannn 3 months ago
- 3 comments
#101 - Add ELFLoader test for AES-GCM assembly routines
Pull Request -
State: closed - Opened by pennyannn 3 months ago
- 3 comments
#100 - feat: add hard theorems from Isabelle
Pull Request -
State: closed - Opened by bollu 3 months ago
- 4 comments
#100 - feat: add hard theorems from Isabelle
Pull Request -
State: closed - Opened by bollu 3 months ago
- 4 comments
#99 - VCG scaffolding for the MemCpy proof
Pull Request -
State: closed - Opened by shigoel 3 months ago
- 1 comment
#99 - VCG scaffolding for the MemCpy proof
Pull Request -
State: closed - Opened by shigoel 3 months ago
- 1 comment
#98 - feat: introduce CosimM to store platform features in a cache
Pull Request -
State: closed - Opened by bollu 3 months ago
- 2 comments
#98 - feat: introduce CosimM to store platform features in a cache
Pull Request -
State: closed - Opened by bollu 3 months ago
- 2 comments
#97 - Cache Target Triple Information for Random Instruction Generation
Issue -
State: closed - Opened by bollu 3 months ago
#97 - Cache Target Triple Information for Random Instruction Generation
Issue -
State: closed - Opened by bollu 3 months ago
#95 - Respect Apple's ABI for cosimulations
Pull Request -
State: closed - Opened by shigoel 3 months ago
- 3 comments
#95 - Respect Apple's ABI for cosimulations
Pull Request -
State: closed - Opened by shigoel 3 months ago
- 3 comments
#94 - chore: remove old versions of the sym tactic, and rename the new `sym1_n` tactic to `sym_n`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#94 - chore: remove old versions of the sym tactic, and rename the new `sym1_n` tactic to `sym_n`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#93 - feat: copy `#time` command from Mathlib
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#93 - feat: copy `#time` command from Mathlib
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#92 - Rework step theorem generation to be faster and cache intermediate results to the environment
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#92 - Rework step theorem generation to be faster and cache intermediate results to the environment
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#91 - Prove the partial correctness of a small program with a loop
Pull Request -
State: closed - Opened by shigoel 4 months ago
- 6 comments
#91 - Prove the partial correctness of a small program with a loop
Pull Request -
State: closed - Opened by shigoel 4 months ago
- 6 comments
#90 - feat: Proof automation for simplifying reads of known reads [3/3]
Pull Request -
State: closed - Opened by bollu 4 months ago
- 3 comments
#90 - feat: Proof automation for simplifying reads of known reads [3/3]
Pull Request -
State: closed - Opened by bollu 4 months ago
- 3 comments
#89 - Better bitvec reduction
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#89 - Better bitvec reduction
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#88 - refactor: make `stepiTac` directly construct an application of the right stepi-theorem
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#88 - refactor: make `stepiTac` directly construct an application of the right stepi-theorem
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#87 - fix: use simprocs in step-theorem generation
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#87 - fix: use simprocs in step-theorem generation
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#86 - refactor: assorted cleanups of `Sym`/`SymContext`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#86 - refactor: assorted cleanups of `Sym`/`SymContext`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#85 - Added bit twiddling hacks proofs using bv_decide
Pull Request -
State: closed - Opened by nwetzler 4 months ago
#85 - Added bit twiddling hacks proofs using bv_decide
Pull Request -
State: closed - Opened by nwetzler 4 months ago
#84 - Reflect decode inst
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 2 comments
#84 - Reflect decode inst
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 2 comments
#83 - feat: spawn tasks for cosimulation to provide (theoretically) $nproc parallelism
Pull Request -
State: closed - Opened by bollu 4 months ago
- 5 comments
#83 - feat: spawn tasks for cosimulation to provide (theoretically) $nproc parallelism
Pull Request -
State: closed - Opened by bollu 4 months ago
- 5 comments
#82 - Switch back to using leanprover/lean-action once MacOS runner is fixed
Issue -
State: closed - Opened by bollu 4 months ago
#82 - Switch back to using leanprover/lean-action once MacOS runner is fixed
Issue -
State: closed - Opened by bollu 4 months ago
#81 - feat: new definitions for memory separation
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#81 - feat: new definitions for memory separation
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#80 - feat: add simproc to simplify fetch_inst through reflection
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 4 comments
#80 - feat: add simproc to simplify fetch_inst through reflection
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 4 comments
#79 - feat: print progress bar of #instructions and #samples in cosim
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#79 - feat: print progress bar of #instructions and #samples in cosim
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#78 - feat: Aarch64 runner
Pull Request -
State: closed - Opened by bollu 4 months ago
- 3 comments
#78 - feat: Aarch64 runner
Pull Request -
State: closed - Opened by bollu 4 months ago
- 3 comments
#77 - Modify cosim scripts to work on M* Apple machines
Pull Request -
State: closed - Opened by shigoel 4 months ago
- 1 comment
#77 - Modify cosim scripts to work on M* Apple machines
Pull Request -
State: closed - Opened by shigoel 4 months ago
- 1 comment
#76 - refactor: generate `stepi` theorems in the relevant program's namespace
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#76 - refactor: generate `stepi` theorems in the relevant program's namespace
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#75 - feat: make sym_n search for h_err and h_sp, or introduce new goals if they are not present
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 2 comments
#75 - feat: make sym_n search for h_err and h_sp, or introduce new goals if they are not present
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 2 comments
#74 - feat: New definitions for the memory model
Pull Request -
State: closed - Opened by bollu 4 months ago
- 4 comments
#74 - feat: New definitions for the memory model
Pull Request -
State: closed - Opened by bollu 4 months ago
- 4 comments
#73 - feat: add extractLsByte(s) API for memory.
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#73 - feat: add extractLsByte(s) API for memory.
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#72 - refactor: rename `Program.min`/`max` to `min?`/`max?` to reflect it returns an option, and introduce `min`, `min!`, `max`, `max!` wrappers around them with the usual meanings
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#72 - refactor: rename `Program.min`/`max` to `min?`/`max?` to reflect it returns an option, and introduce `min`, `min!`, `max`, `max!` wrappers around them with the usual meanings
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#71 - Files reorganization
Pull Request -
State: closed - Opened by shigoel 4 months ago
#71 - Files reorganization
Pull Request -
State: closed - Opened by shigoel 4 months ago
#70 - chore: move memory into a semarate Arm/Memory/ subdirectory
Pull Request -
State: closed - Opened by bollu 4 months ago
#70 - chore: move memory into a semarate Arm/Memory/ subdirectory
Pull Request -
State: closed - Opened by bollu 4 months ago
#69 - feat: introduce `sym1_n` tactic as a more intelligent version of `sym1_i_n`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#69 - feat: introduce `sym1_n` tactic as a more intelligent version of `sym1_i_n`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 3 comments
#68 - Adding Popcount32 proof
Pull Request -
State: closed - Opened by nwetzler 4 months ago
#68 - Adding Popcount32 proof
Pull Request -
State: closed - Opened by nwetzler 4 months ago
#67 - Adding MADD (32- and 64-bit) (alias MUL) to instructions
Pull Request -
State: closed - Opened by nwetzler 4 months ago
- 3 comments
#67 - Adding MADD (32- and 64-bit) (alias MUL) to instructions
Pull Request -
State: closed - Opened by nwetzler 4 months ago
- 3 comments
#66 - Program proofs using assertional verification methods
Pull Request -
State: closed - Opened by shigoel 4 months ago
#66 - Program proofs using assertional verification methods
Pull Request -
State: closed - Opened by shigoel 4 months ago
#65 - feat: Common Subpexpression Elimination, v1
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#65 - feat: Common Subpexpression Elimination, v1
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#64 - chore: docs and tracing for `sym1_i_n` tactic
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#64 - chore: docs and tracing for `sym1_i_n` tactic
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#63 - Update aes_hw_ctr32_encrypt_blocks
Pull Request -
State: closed - Opened by pennyannn 4 months ago
#63 - Update aes_hw_ctr32_encrypt_blocks
Pull Request -
State: closed - Opened by pennyannn 4 months ago
#62 - chore: Test a fix for ELFSage's stack overflow [DONTMERGE]
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#62 - chore: Test a fix for ELFSage's stack overflow [DONTMERGE]
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#61 - fix: read the full 128 bits of an SFP register in cosimulation
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#61 - fix: read the full 128 bits of an SFP register in cosimulation
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#60 - feat: full symbolic evaluation of `gcm_gmult_v8_program`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#60 - feat: full symbolic evaluation of `gcm_gmult_v8_program`
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
- 1 comment
#59 - Remove definitions that have been incorporated into ELFSage
Pull Request -
State: closed - Opened by shigoel 4 months ago
#59 - Remove definitions that have been incorporated into ELFSage
Pull Request -
State: closed - Opened by shigoel 4 months ago
#58 - chore: install cadical in CI
Pull Request -
State: closed - Opened by bollu 4 months ago
#58 - chore: install cadical in CI
Pull Request -
State: closed - Opened by bollu 4 months ago
#57 - chore: update toolchain to nightly-2024-08-02
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#57 - chore: update toolchain to nightly-2024-08-02
Pull Request -
State: closed - Opened by alexkeizer 4 months ago
#56 - Implement a decision procedure for memory reads/write via omega
Pull Request -
State: closed - Opened by bollu 4 months ago
- 9 comments
#56 - Implement a decision procedure for memory reads/write via omega
Pull Request -
State: closed - Opened by bollu 4 months ago
- 9 comments
#55 - Experiment: Use r for accessing the program field, which solves program being public.
Issue -
State: open - Opened by bollu 4 months ago
#55 - Experiment: Use r for accessing the program field, which solves program being public.
Issue -
State: open - Opened by bollu 4 months ago
#54 - Update AES-GCM programs and their tests
Pull Request -
State: closed - Opened by pennyannn 4 months ago
#54 - Update AES-GCM programs and their tests
Pull Request -
State: closed - Opened by pennyannn 4 months ago
#53 - Added Stack Pointer (SP) Alignment to symbolic simulation tactic
Pull Request -
State: closed - Opened by nwetzler 4 months ago
- 2 comments
#53 - Added Stack Pointer (SP) Alignment to symbolic simulation tactic
Pull Request -
State: closed - Opened by nwetzler 4 months ago
- 2 comments
#52 - feat: add documentation generation to CI
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#52 - feat: add documentation generation to CI
Pull Request -
State: closed - Opened by bollu 4 months ago
- 2 comments
#51 - chore: Make ArmState fields private to ensure that every field access is written in terms of r/w and read/write_mem_bytes
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment
#51 - chore: Make ArmState fields private to ensure that every field access is written in terms of r/w and read/write_mem_bytes
Pull Request -
State: closed - Opened by bollu 4 months ago
- 1 comment