Commits

Branch selector

 jh/fix-bytes2int-int2bytes

User selector

All users

Datepicker

All time

Commit History

Commits on Jun 17, 2025

• Enhance inequality simplification rules in `int-simplifications.md` with SMT lemma annotations. Update test cases in `xx.k` to reflect changes and add new assertions for `Bytes2Int` patterns.

  Stevengre

  committed
  cbaaa39

  Copy full SHA for cbaaa39

Commits on Jun 13, 2025

• Set Version: 0.1.106

  rv-auditor

  committed
  cfe95a9

  Copy full SHA for cfe95a9

• Fix unsimplified `bytes2int o int2bytes` patterns.

  Stevengre

  committed
  d51ed6d

  Copy full SHA for d51ed6d

• Add simplification rule for `Bytes2Int &Int 4294967295` (#135)

  Show description for 3804716
  

  Stevengre

  and

  rv-auditor

  authored
  3804716

  Copy full SHA for 3804716

• Add `optimize_kcfg` parameter in `SymTool` (#134)

  Show description for db011d7
  

  3 peopleauthored
  db011d7

  Copy full SHA for db011d7

Commits on Jun 12, 2025

• Simp rule 4 `(A +Int B) &Int 4294967295 <Int A` (#130)

  Show description for c72b80f
  

  3 peopleauthored
  c72b80f

  Copy full SHA for c72b80f

Commits on Jun 11, 2025

• Update dependency: deps/k_release (#127)

  Show description for 0d09047
  

  rv-jenkins

  and

  rv-auditor

  authored
  0d09047

  Copy full SHA for 0d09047

• Add extensible prover implementation (#103)

  Show description for fca8f9f
  

  tothtamas28

  and

  rv-auditor

  authored
  fca8f9f

  Copy full SHA for fca8f9f

• fix version of `uv` in CI (#133)

  Show description for fb931c8
  

  juliankuners

  and

  rv-auditor

  authored
  fb931c8

  Copy full SHA for fb931c8

• Fix version in `uv.lock` (#131)

  Show description for c77e2a5
  

  tothtamas28

  and

  rv-auditor

  authored
  c77e2a5

  Copy full SHA for c77e2a5

Commits on Jun 10, 2025

• Add simp rules for revsersed `substrBytes` concat (#128)

  Show description for 570e0f4
  

  3 peopleauthored
  570e0f4

  Copy full SHA for 570e0f4

• Add simp rules 4 `Bytes2Int o Int2Bytes` and `substrBytes o Int2Bytes` (#124)

  Show description for 2fc0603
  

  4 peopleauthored
  2fc0603

  Copy full SHA for 2fc0603

Commits on Jun 4, 2025

• Migrate from `poetry` to `uv` (#125)

  Show description for 711f12b
  

  tothtamas28

  and

  rv-auditor

  authored
  711f12b

  Copy full SHA for 711f12b

Commits on Jun 3, 2025

• Remove attribute `source_dir` from `SymTools` (#126)

  Show description for 07180df
  

  tothtamas28

  and

  rv-auditor

  authored
  07180df

  Copy full SHA for 07180df

Commits on May 30, 2025

• Add simp rules 4 `&Int` assoc (#123)

  Show description for cf4108d
  

  Stevengre

  and

  rv-auditor

  authored
  cf4108d

  Copy full SHA for cf4108d

Commits on May 29, 2025

• Add property `proof_show` to `SymTools` (#122)

  Show description for c2d312e
  

  tothtamas28

  and

  rv-auditor

  authored
  c2d312e

  Copy full SHA for c2d312e

Commits on May 28, 2025

• Update dependency: deps/k_release (#114)

  Show description for 0949ca5
  

  rv-jenkins

  and

  rv-auditor

  authored
  0949ca5

  Copy full SHA for 0949ca5

• Refactor RISC-V semantics to replace `Word` with `Int` (#121)

  Show description for f680218
  

  3 peopleauthored
  f680218

  Copy full SHA for f680218

Commits on May 27, 2025

• Enable instantiating symbolic config (#117)

  Show description for cba2d2b
  

  tothtamas28

  and

  rv-auditor

  authored
  cba2d2b

  Copy full SHA for cba2d2b

• Write temporary test data into separate folders by default (#120)

  Show description for d411af1
  

  tothtamas28

  and

  rv-auditor

  authored
  d411af1

  Copy full SHA for d411af1

• Inline the `<test>` cell (#119)

  Show description for 759923e
  

  tothtamas28

  and

  rv-auditor

  authored
  759923e

  Copy full SHA for 759923e

Commits on May 26, 2025

• Transform function `branchPC` to effect function `#PC_BRANCH` (#115)

  Show description for 202c19a
  

  3 peopleauthored
  202c19a

  Copy full SHA for 202c19a

• Consolidate ELF file handling under class `ELF` (#116)

  Show description for 25b7057
  

  tothtamas28

  and

  rv-auditor

  authored
  25b7057

  Copy full SHA for 25b7057

Commits on May 22, 2025

• Add simp rules for `Int2Bytes o Bytes2Int` (#111)

  Show description for bb2934c
  

  3 peopleauthored
  bb2934c

  Copy full SHA for bb2934c

• Add simp rules for `Bytes2Int o |Int o Bytes2Int` (#109)

  Show description for 4c53805
  

  3 peopleauthored
  4c53805

  Copy full SHA for 4c53805

Commits on May 21, 2025

• simplify patterns `Bytes2Int o <<Int` & `Bytes2Int o >>Int` & chop (#108)

  Show description for 803850d
  

  3 peopleauthored
  803850d

  Copy full SHA for 803850d

• Add simp rules for `replaceAtBytes` (#112)

  Show description for c157326
  

  3 peopleauthored
  c157326

  Copy full SHA for c157326

• Add simp rules for `substrBytes(A +Bytes B, I, J)` (#110)

  Show description for e2369f6
  

  3 peopleauthored
  e2369f6

  Copy full SHA for e2369f6

• Update dependency: deps/k_release (#113)

  Show description for a5b98f5
  

  3 peopleauthored
  a5b98f5

  Copy full SHA for a5b98f5

Commits on May 20, 2025

• Update dependency: deps/k_release (#99)

  Show description for 81d5723
  

  3 peopleauthored
  81d5723

  Copy full SHA for 81d5723

• Simplify pattern `Bytes2Int o substrBytes &Int 65280` (#105)

  Show description for 66ddeca
  

  Stevengre

  and

  rv-auditor

  authored
  66ddeca

  Copy full SHA for 66ddeca

• Add simp rule to eliminate `SignExtend` (#100)

  Show description for 79bf2fd
  

  Stevengre

  and

  rv-auditor

  authored
  79bf2fd

  Copy full SHA for 79bf2fd

• Tackle unexpected pattern for `pickfront` and `dropfront`. (#98)

  Show description for 4dcaa6f
  

  Stevengre

  and

  rv-auditor

  authored
  4dcaa6f

  Copy full SHA for 4dcaa6f

• Add simp rule for `<<Int o <<Int` (#106)

  Show description for 72ad19b
  

  Stevengre

  and

  rv-auditor

  authored
  72ad19b

  Copy full SHA for 72ad19b

• Avoid ambiguity for Word expressions (#97)

  Show description for 8090120
  

  Stevengre

  and

  rv-auditor

  authored
  8090120

  Copy full SHA for 8090120

Pagination

Previous

Next