Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Mar 24, 2024

• Prove Byte_odd_has_inverse

  thaliaarchi

  committedMar 24, 2024
  e62288b

  Copy full SHA for e62288b

• Change from N to Z

  thaliaarchi

  committedMar 24, 2024
  6e84dae

  Copy full SHA for 6e84dae

• Prove N_odd_has_inverse the dumb way

  thaliaarchi

  committedMar 24, 2024
  6e53545

  Copy full SHA for 6e53545

Commits on Feb 18, 2023

• Create abstract_vm type

  thaliaarchi

  committedFeb 18, 2023
  0e2c0ef

  Copy full SHA for 0e2c0ef

• Create bounded vm and byte types with relations

  thaliaarchi

  committedFeb 18, 2023
  8f89aaf

  Copy full SHA for 8f89aaf

Commits on Feb 17, 2023

• Append relir

  thaliaarchi

  committedFeb 17, 2023
  3e0012c

  Copy full SHA for 3e0012c

• Only consider odd equivalence to 1

  thaliaarchi

  committedFeb 17, 2023
  c914483

  Copy full SHA for c914483

Commits on Feb 14, 2023

• Simplify with ltac and compute inverse

  thaliaarchi

  committedFeb 14, 2023
  bd359da

  Copy full SHA for bd359da

Commits on Feb 13, 2023

• Prove that all odd integers have inverses (mod 256)

  thaliaarchi

  committedFeb 13, 2023
  71317d2

  Copy full SHA for 71317d2

• Move source files to theories

  thaliaarchi

  committedFeb 13, 2023
  43785f5

  Copy full SHA for 43785f5

Commits on Feb 1, 2023

• Move relation variables from forall to constructors

  thaliaarchi

  committedFeb 1, 2023
  3341805

  Copy full SHA for 3341805

Commits on Jan 23, 2023

• Regenerate Makefile.coq on dependency change

  thaliaarchi

  committedJan 23, 2023
  68eff4a

  Copy full SHA for 68eff4a

Commits on Dec 28, 2022

• Lower AST to RelIR

  thaliaarchi

  committedDec 28, 2022
  d793f44

  Copy full SHA for d793f44

• Specify RelIR execute semantics

  thaliaarchi

  committedDec 28, 2022
  fdeaab1

  Copy full SHA for fdeaab1

• Create offset-based VM

  thaliaarchi

  committedDec 28, 2022
  abb2d78

  Copy full SHA for abb2d78

• Prove normalize idempotency

  thaliaarchi

  committedDec 28, 2022
  88fe6f2

  Copy full SHA for 88fe6f2

Commits on Dec 27, 2022

• Prove that normalize is normalized

  thaliaarchi

  committedDec 27, 2022
  c7f2aa2

  Copy full SHA for c7f2aa2

• Compare ending states for equality

  thaliaarchi

  committedDec 27, 2022
  6a35c53

  Copy full SHA for 6a35c53

Commits on Dec 26, 2022

• Avoid proof state mixed into VM.shift_left

  thaliaarchi

  committedDec 26, 2022
  7882266

  Copy full SHA for 7882266

Commits on Dec 25, 2022

• Represent VM as record with proof of normalization

  thaliaarchi

  committedDec 25, 2022
  c32a149

  Copy full SHA for c32a149

• Define RelIR

  thaliaarchi

  committedDec 25, 2022
  1a0d2c9

  Copy full SHA for 1a0d2c9

• Rename ComIR definitions

  thaliaarchi

  committedDec 25, 2022
  18ba2a1

  Copy full SHA for 18ba2a1

• Rename IR to ComIR "combined IR"

  thaliaarchi

  committedDec 25, 2022
  4e244dc

  Copy full SHA for 4e244dc

Commits on Dec 24, 2022

• Update byte usages

  thaliaarchi

  committedDec 24, 2022
  178b917

  Copy full SHA for 178b917

• Use byte type from CompCert

  thaliaarchi

  committedDec 24, 2022
  79ee7da

  Copy full SHA for 79ee7da

Commits on Dec 23, 2022

• Define more operations on byte

  thaliaarchi

  committedDec 23, 2022
  fbba3c0

  Copy full SHA for fbba3c0

• Remove generated Makefile

  thaliaarchi

  committedDec 23, 2022
  7af816e

  Copy full SHA for 7af816e

Commits on Dec 22, 2022

• Prove correctness of IR.combine, except for VM normalization

  thaliaarchi

  committedDec 22, 2022
  974317a

  Copy full SHA for 974317a

Commits on Dec 21, 2022

• Lower loops of odd adds to MConst 0

  thaliaarchi

  committedDec 21, 2022
  0f2e0f0

  Copy full SHA for 0f2e0f0

• Create MIR with constant assignment

  thaliaarchi

  committedDec 21, 2022
  f8b0e73

  Copy full SHA for f8b0e73

• Prove lex inverse and state theorems for parse and Ook! inverses

  thaliaarchi

  committedDec 21, 2022
  b924e22

  Copy full SHA for b924e22

• Prove lower_ast_sound bidirectionally

  thaliaarchi

  committedDec 21, 2022
  7d7e8bb

  Copy full SHA for 7d7e8bb

• Prove correctness of cons_add

  thaliaarchi

  committedDec 21, 2022
  e5b3636

  Copy full SHA for e5b3636

• Fix IR cons definitions

  thaliaarchi

  committedDec 21, 2022
  74f2abc

  Copy full SHA for 74f2abc

Commits on Dec 20, 2022

• Make VM.move_left compose and prove more properties of repeat_apply

  thaliaarchi

  committedDec 20, 2022
  51660dc

  Copy full SHA for 51660dc

Pagination

Previous

Next