issues
search
leanprover
/
LNSym
Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62
stars
18
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Update the gcm_init_v8 proof
#245
pennyannn
opened
2 days ago
0
Bump toolchain 2024 11 01
#244
bollu
opened
6 days ago
0
Progress towards GCMGMultV8 and associated BitVec cleanup
#243
shigoel
closed
3 weeks ago
0
refactor: rephrase the register frame-condition precondition as non-membership in a list of modified registers
#242
alexkeizer
closed
1 week ago
1
feat: light-weight basic quotation macro
#241
alexkeizer
opened
3 weeks ago
1
feat: enable simp_mem to be used in ITP style [8/?]
#240
bollu
closed
6 days ago
0
WIP: Experimental method to aggregate state effects
#239
shigoel
closed
2 hours ago
2
feat: Add fine grained control over mem_omega rewriting [7/?]
#238
bollu
closed
1 week ago
0
feat: Rewrite simp_mem to build a new expression, thereby localizing the effects of rewrites [6/?]
#237
bollu
closed
1 week ago
1
feat: expand `sym_aggregate` search to include equalities `?state.program = ?program`
#236
alexkeizer
closed
3 weeks ago
0
refactor: rename `Tactic.sym.debug` traceclass to avoid confusion with the option of the same name.
#235
alexkeizer
closed
3 weeks ago
0
feat: Track whether simp_mem made progress in the monad state [5/?]
#234
bollu
closed
1 week ago
0
feat: Switch out all of `mem_omega` with MetaM [4/?]
#233
bollu
closed
1 week ago
0
feat: Switch bvOmegaBench to use MetaM [3/?]
#232
bollu
closed
1 week ago
0
chore: Split out the finishing tactic aspect of simp_mem into mem_omega [2/?]
#231
bollu
closed
1 week ago
0
chore: split out simp_mem to Arm/Memory/Common [1/?]
#230
bollu
closed
1 week ago
0
feat: mem_separate_of_mem_separate'
#229
bollu
closed
4 weeks ago
0
chore: do not CSE literals
#228
bollu
closed
4 weeks ago
0
chore: fix proof building in 'mem.read ... = mem.read ...'
#227
bollu
closed
4 weeks ago
0
Determining possibly modified registers statically
#226
shigoel
closed
3 weeks ago
0
Work towards the GCM GMult functional correctness proof
#225
shigoel
closed
4 weeks ago
0
refactor: change memory-effects theorem to a quantifier-free statement
#224
alexkeizer
closed
3 weeks ago
3
feat: add bv_omega_bench to run omega and produce goal states + timing inf.
#223
bollu
closed
4 weeks ago
4
refactor: extract out `MemoryEffects` structure
#222
alexkeizer
closed
4 weeks ago
2
feat: generalize to arbitrary bitvec width `zeroextend_bigger_smaller` and `truncate_of_concat_is_lsb`
#221
luisacicolini
closed
1 month ago
2
chore: make section names more meaningful
#220
alexkeizer
closed
1 month ago
0
BLOCKED: refactor: reimplement initNextStep without evalTactic
#219
alexkeizer
opened
1 month ago
2
chore: bugfixes and benchmark code for the memory based simp_mem
#218
bollu
opened
1 month ago
0
chore: bump toolchain to nightly-2024-10-07
#217
alexkeizer
closed
3 weeks ago
4
Simplify partInstall to use start and len
#216
pennyannn
closed
1 month ago
0
BLOCKED: refactor: replace `rewrite` with `mkEqNDRec`
#215
alexkeizer
opened
1 month ago
2
chore: add better trace nodes to `AxEffects`
#214
alexkeizer
closed
1 month ago
1
feat: use withCurrHeartbeats to reset the heartbeat usage for each step in `sym_n`
#213
alexkeizer
closed
1 month ago
0
BLOCKED: feat: `withInstantiatMainGoal` combinator to eagerly instantiate goal metavariables
#212
alexkeizer
closed
3 weeks ago
1
chore: add more trace nodes, for better profiling data
#211
alexkeizer
closed
1 month ago
2
BLOCKED: feat: intermediate state aggregation through a persistent AxEffects object
#210
alexkeizer
opened
1 month ago
1
feat: attempt to preserve stack alignment proof in AxEffect update
#209
alexkeizer
closed
1 month ago
1
feat: remove toNat lemmas from bitvec_rules
#208
bollu
closed
1 month ago
0
refactor: remove `SymContext.h_sp?`, replacing uses with the corresponding `AxEffects` field
#207
alexkeizer
closed
1 month ago
0
chore: bump up toolchain 29/9/2024
#206
bollu
closed
1 month ago
2
Syntax for stating register and memory frame conditions
#205
shigoel
closed
1 month ago
0
feat: add options for more control over benchmarking and better profiling support
#204
alexkeizer
closed
1 month ago
1
Minor edits to SHA512 sym
#203
shigoel
closed
1 month ago
0
chore: add commented set_option trace.profiler true for easy logging
#202
bollu
closed
1 month ago
0
refactor: use searchLCtx in sym_aggregate
#201
alexkeizer
closed
1 month ago
0
feat: search for reads of *any* register when building an initial `SymContext`
#200
alexkeizer
closed
1 month ago
3
fix: `inferStatePrefix...` should default to `s1` as the first intermediate state.
#199
alexkeizer
closed
1 month ago
2
feat: add combinators for more fine-grained benchmarking
#198
alexkeizer
closed
1 month ago
3
feat: Switch to using bv_decide to decide memory goals instead of bv_omega
#197
bollu
opened
1 month ago
1
chore: fix geomean computation
#196
bollu
closed
1 month ago
0
Next