Commits

Branch selector

 main

User selector

meng-xu-cs

Datepicker

All time

Commit History

Commits on Nov 24, 2021

• [move-prover][tests] add inconsistency flag to df and stdlib only

  Show description for 8ed611a
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  8ed611a

  Copy full SHA for 8ed611a

Commits on Nov 23, 2021

• [move-prover] better architecture for simplification pipeline

  Show description for f4a0b8e
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  f4a0b8e

  Copy full SHA for f4a0b8e

• [move-prover] combine simplify tests and no_opaque tests

  Show description for 05bb3fc
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  05bb3fc

  Copy full SHA for 05bb3fc

• [move-prover][tests] test the simplifier pipeline

  

  meng-xu-cs

  authored and

  bors-libra

  committed
  5e1d148

  Copy full SHA for 5e1d148

• [move-model] do model-level simplification in move-model

  Show description for 6e95a55
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  6e95a55

  Copy full SHA for 6e95a55

Commits on Nov 18, 2021

• [move-prover] include the experimental code in df for verification

  Show description for 6a43b96
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  6a43b96

  Copy full SHA for 6a43b96

• [move-prover] create a choice boogie function on unique ExpData

  Show description for 566a655
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  566a655

  Copy full SHA for 566a655

• [move-prover] update cvc4 to cvc5 as boogie solver option

  Show description for a992689
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  a992689

  Copy full SHA for a992689

Commits on Nov 10, 2021

• [move-vm] separate error code for vector ops

  Show description for 1a8bbb8
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  1a8bbb8

  Copy full SHA for 1a8bbb8

• [move-prover] record information when ghost type params are created

  Show description for c7dc142
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  c7dc142

  Copy full SHA for c7dc142

• [move-prover] refactor the way entrypoint assumptions are collected

  Show description for 2406f36
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  2406f36

  Copy full SHA for 2406f36

• [move-prover] hold-off the warning on uninstantiated invariants

  

  meng-xu-cs

  authored and

  bors-libra

  committed
  2f62265

  Copy full SHA for 2f62265

• [move-prover] parenthesis the ITE expression when translating to boogie

  Show description for bc9436e
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  bc9436e

  Copy full SHA for bc9436e

Commits on Nov 4, 2021

• [move-model] test case for type checks in built-ins

  Show description for 449301d
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  449301d

  Copy full SHA for 449301d

• [move-model] allow extra checks in type instantiations for built-ins

  Show description for eddae7e
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  eddae7e

  Copy full SHA for eddae7e

• [move-prover] disable aptos-labs#9545 temporarily and catch warnings in testsuite

  Show description for 71a806e
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  71a806e

  Copy full SHA for 71a806e

Commits on Oct 27, 2021

• [move-prover] add a test case for warnings on uninstanted invariants

  Show description for e6ce2a8
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  e6ce2a8

  Copy full SHA for e6ce2a8

• [move-prover] warn if unable to instantiate a generic global invariant

  Show description for 78a6671
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  78a6671

  Copy full SHA for 78a6671

Commits on Oct 21, 2021

• [move-prover][spec-flatten] add an option to use ExpDisplay for debug

  Show description for 727a4e2
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  727a4e2

  Copy full SHA for 727a4e2

• [move-prover][spec-flatten] unroll function call, lambda, and block exp

  Show description for 99cbb52
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  99cbb52

  Copy full SHA for 99cbb52

• [move-prover][spec-flatten] convert the tool into a pipeline architecture

  Show description for 4edc5e4
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  4edc5e4

  Copy full SHA for 4edc5e4

Commits on Oct 19, 2021

• [move-file-format] use version number 4 for vector bytecode

  Show description for cf0d89a
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  cf0d89a

  Copy full SHA for cf0d89a

• [move-binary-format] remove the version check in visibility loading

  Show description for 7b394b1
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  7b394b1

  Copy full SHA for 7b394b1

Commits on Oct 16, 2021

• [move-file-format] allow the deserializer to recognize version 4

  Show description for d2cf63f
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  d2cf63f

  Copy full SHA for d2cf63f

Commits on Oct 14, 2021

• [move-prover] type dependent code test cases

  Show description for ba17245
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  ba17245

  Copy full SHA for ba17245

Commits on Oct 13, 2021

• [move-prover][paper] break url in bib

  Show description for a9a3a8b
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  a9a3a8b

  Copy full SHA for a9a3a8b

• [move-prover][paper] elaborated the memory model a bit

  Show description for ac9c4de
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  ac9c4de

  Copy full SHA for ac9c4de

Commits on Oct 11, 2021

• [move-prover][report] readability pass on the report

  Show description for 203396d
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  203396d

  Copy full SHA for 203396d

Commits on Oct 8, 2021

• [move-prover][spec-flatten] use prettydoc to format the code

  Show description for 41b2573
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  41b2573

  Copy full SHA for 41b2573

• [move-prover][spec-flatten] dump the flattened spec

  

  meng-xu-cs

  authored and

  bors-libra

  committed
  274d138

  Copy full SHA for 274d138

Commits on Oct 5, 2021

• [move][doc] phantom types

  Show description for 9c8d6c5
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  9c8d6c5

  Copy full SHA for 9c8d6c5

Commits on Sep 29, 2021

• [move-prover][spec-flatten] leverage the function-only scope

  Show description for 90dd711
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  90dd711

  Copy full SHA for 90dd711

• [move-prover][spec-flatten] prover-assisted aborts_if trimming

  Show description for 095c570
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  095c570

  Copy full SHA for 095c570

• [move-prover][spec-flatten] set up the prover workflow as a function

  Show description for 5ba9085
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  5ba9085

  Copy full SHA for 5ba9085

• [move-prover][spec-flatten] skeleton of the spec flatten tool

  Show description for e219995
  

  meng-xu-cs

  authored and

  bors-libra

  committed
  e219995

  Copy full SHA for e219995

Pagination

Previous

Next