Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Dec 9, 2024

• SHA512 symbolic simulation effort that leverages presimplified block semantics

  shigoel

  committed
  5c05220

  Copy full SHA for 5c05220

Commits on Nov 15, 2024

• Use AbstractAtoms in PruneUpdates

  shigoel

  committed
  678c2ce

  Copy full SHA for 678c2ce

Commits on Nov 13, 2024

• Fix typo. in prune_updates timeout example

  shigoel

  committed
  8926219

  Copy full SHA for 8926219

• Add reference implementation of prune_updates (#246)

  Show description for 6847ebc
  

  shigoel

  and

  bollu

  authored
  6847ebc

  Copy full SHA for 6847ebc

Commits on Nov 12, 2024

• Update the gcm_init_v8 proof (#245)

  Show description for 16a1dd9
  pennyannn

  authored
  16a1dd9

  Copy full SHA for 16a1dd9

Commits on Nov 1, 2024

• feat: enable simp_mem to be used in ITP style [8/?] (#240)

  Show description for e397f57
  bollu

  authored
  e397f57

  Copy full SHA for e397f57

Commits on Oct 31, 2024

• feat: Add fine grained control over mem_omega rewriting [7/?] (#238)

  Show description for 619ef75
  

  bollu

  and

  shigoel

  authored
  619ef75

  Copy full SHA for 619ef75

• refactor: rephrase the register frame-condition precondition as non-membership in a list of modified registers (#242)

  Show description for a4d2552
  

  alexkeizer

  and

  shigoel

  authored
  a4d2552

  Copy full SHA for a4d2552

• Merge pull request #237 from leanprover/simp-mem-mem-omega-6

  Show description for 5eb5fa9
  bollu

  authored
  5eb5fa9

  Copy full SHA for 5eb5fa9

• chore: cleanup

  bollu

  committed
  aae38de

  Copy full SHA for aae38de

• feat: Rewrite simp_mem to build a new expression, thereby localizing the effects of rewrites [6/?]

  bollu

  committed
  f119628

  Copy full SHA for f119628

• feat: Track whether simp_mem made progress in the monad state [5/?] (#234)

  Show description for 37cb9f5
  bollu

  authored
  37cb9f5

  Copy full SHA for 37cb9f5

• feat: Switch out all of mem_omega with MetaM [4/?] (#233)

  Show description for 49914dd
  bollu

  authored
  49914dd

  Copy full SHA for 49914dd

Commits on Oct 30, 2024

• feat: Switch bvOmegaBench to use MetaM [3/?] (#232)

  Show description for 486bd6e
  bollu

  authored
  486bd6e

  Copy full SHA for 486bd6e

Commits on Oct 29, 2024

• chore: Split out the finishing tactic aspect of simp_mem into mem_omega [2/?] (#231)

  Show description for 25fffe0
  bollu

  authored
  25fffe0

  Copy full SHA for 25fffe0

Commits on Oct 28, 2024

• chore: split out simp_mem to Arm/Memory/Common [1/?] (#230)

  Show description for 3ac8c20
  

  bollu

  and

  shigoel

  authored
  3ac8c20

  Copy full SHA for 3ac8c20

Commits on Oct 17, 2024

• Progress towards GCMGMultV8 and associated BitVec cleanup (#243)

  Show description for 1b67f50
  shigoel

  authored
  1b67f50

  Copy full SHA for 1b67f50

Commits on Oct 16, 2024

• refactor: change memory-effects theorem to a quantifier-free statement (#224)

  Show description for a47a266
  

  3 peopleauthored
  a47a266

  Copy full SHA for a47a266

• WIP: trying out a non-trivial correctness goal for gcm_init_v8 (#173)

  Show description for c7829f1
  

  pennyannn

  and

  shigoel

  authored
  c7829f1

  Copy full SHA for c7829f1

Commits on Oct 14, 2024

• Determining possibly modified registers statically (#226)

  Show description for 807738b
  

  shigoel

  and

  bollu

  authored
  807738b

  Copy full SHA for 807738b

• refactor: rename Tactic.sym.debug traceclass to avoid confusion with the option of the same name. (#235)

  Show description for c9ca372
  

  alexkeizer

  and

  shigoel

  authored
  c9ca372

  Copy full SHA for c9ca372

Commits on Oct 13, 2024

• feat: expand sym_aggregate search to include equalities ?state.program = ?program (#236)

  Show description for 3b8f5f1
  alexkeizer

  authored
  3b8f5f1

  Copy full SHA for 3b8f5f1

Commits on Oct 11, 2024

• chore: bump toolchain to nightly-2024-10-07 (#217)

  Show description for 2e4d59c
  alexkeizer

  authored
  2e4d59c

  Copy full SHA for 2e4d59c

Commits on Oct 10, 2024

• feat: mem_separate_of_mem_separate' (#229)

  Show description for 004e068
  

  bollu

  and

  shigoel

  authored
  004e068

  Copy full SHA for 004e068

• chore: do not CSE literals (#228)

  Show description for 0096556
  

  bollu

  and

  shigoel

  authored
  0096556

  Copy full SHA for 0096556

• chore: fix proof building in 'mem.read ... = mem.read ...' (#227)

  Show description for 8fdbadb
  

  bollu

  and

  shigoel

  authored
  8fdbadb

  Copy full SHA for 8fdbadb

• refactor: extract out MemoryEffects structure (#222)

  Show description for 0ac14c8
  

  alexkeizer

  and

  shigoel

  authored
  0ac14c8

  Copy full SHA for 0ac14c8

Commits on Oct 9, 2024

• feat: replace use of (evalTactic bv_omega) with a manual run of simp followed by (evalTactic omega) (#195)

  Show description for ae0d779
  bollu

  authored
  ae0d779

  Copy full SHA for ae0d779

• feat: add bv_omega_bench to run omega and produce goal states + timing inf. (#223)

  Show description for d11921b
  

  bollu

  and

  shigoel

  authored
  d11921b

  Copy full SHA for d11921b

• Work towards the GCM GMult functional correctness proof (#225)

  Show description for a499a57
  shigoel

  authored
  a499a57

  Copy full SHA for a499a57

Commits on Oct 8, 2024

• chore: make section names more meaningful (#220)

  Show description for 22c4c3e
  alexkeizer

  authored
  22c4c3e

  Copy full SHA for 22c4c3e

• feat: use withCurrHeartbeats to reset the heartbeat usage for each step in sym_n (#213)

  Show description for 139c089
  

  alexkeizer

  and

  shigoel

  authored
  139c089

  Copy full SHA for 139c089

• chore: add more trace nodes, for better profiling data (#211)

  Show description for 85d5239
  

  alexkeizer

  and

  shigoel

  authored
  85d5239

  Copy full SHA for 85d5239

• feat: add options for more control over benchmarking and better profiling support (#204)

  Show description for 55a8638
  

  alexkeizer

  and

  shigoel

  authored
  55a8638

  Copy full SHA for 55a8638

• feat: attempt to preserve stack alignment proof in AxEffect update (#209)

  Show description for 055809c
  

  alexkeizer

  and

  shigoel

  authored
  055809c

  Copy full SHA for 055809c

Pagination

Previous

Next