Code

Proof conventions 2#1134

Code

Merged

mergify[bot] merged 11 commits intomasterGaloisInc/saw-script:masterfrom proof-conventions2GaloisInc/saw-script:proof-conventions2Copy head branch name to clipboardApr 13, 2021

+552-392

Commits

Commits on Apr 13, 2021

• Make ProofScript into a newtype.

  robdockins

  committed
  4c314b6

  Copy full SHA for 4c314b6

• Rework the runProofScript method.

  Show description for 0bd1faf
  robdockins

  committed
  0bd1faf

  Copy full SHA for 0bd1faf

• Change the user-facing type of prover tactics

  Show description for 34c36d4
  robdockins

  committed
  34c36d4

  Copy full SHA for 34c36d4

• Use new bitblasting primitives intead of old ones slated for removal.

  robdockins

  committed
  20c4e6f

  Copy full SHA for 20c4e6f

• bump saw-core to remove some obsolete code

  robdockins

  committed
  186dba4

  Copy full SHA for 186dba4

• Add a new admit tactic.

  Show description for aa02aef
  robdockins

  committed
  aa02aef

  Copy full SHA for aa02aef

• Haddocs for the CEX and ProofResult types.

  robdockins

  committed
  e057bef

  Copy full SHA for e057bef

• Update caseProofResult to allow the valid branch

  Show description for 7ff1680
  robdockins

  committed
  7ff1680

  Copy full SHA for 7ff1680

• Communicate counterexamples with ExtCns names instead of String.

  robdockins

  committed
  099eeac

  Copy full SHA for 099eeac

• Check Prop more strictly; implement boolToProp.

  Show description for eed686f
  robdockins

  committed
  eed686f

  Copy full SHA for eed686f

• bump saw-core to master

  robdockins

  committed
  84012ac

  Copy full SHA for 84012ac