Code

main PE soundness theorems#402

Code

Draft

cdisselkoen wants to merge 10 commits intomaincedar-policy/cedar-spec:mainfrom

cdisselkoen/pe-soundnesscedar-policy/cedar-spec:cdisselkoen/pe-soundnessCopy head branch name to clipboard

Commits

Commits on Jul 30, 2024

• main PE soundness theorems

  Show description for 431a6b8
  cdisselkoen

  committed
  431a6b8

  Copy full SHA for 431a6b8

Commits on Jul 31, 2024

• resolve one sorry

  Show description for 32e3e0b
  cdisselkoen

  committed
  32e3e0b

  Copy full SHA for 32e3e0b

Commits on Aug 12, 2024

• address some sorrys in ReevaluateValue.lean

  Show description for b56d2c6
  cdisselkoen

  committed
  b56d2c6

  Copy full SHA for b56d2c6

• finish another proof

  Show description for 72fa287
  cdisselkoen

  committed
  72fa287

  Copy full SHA for 72fa287

• whoops remove bad import

  Show description for 5b3a76c
  cdisselkoen

  committed
  5b3a76c

  Copy full SHA for 5b3a76c

Commits on Aug 14, 2024

• fill in another case

  Show description for 7872751
  cdisselkoen

  committed
  7872751

  Copy full SHA for 7872751

Commits on Aug 22, 2024

• Merge remote-tracking branch 'origin/main' into cdisselkoen/pe-soundness

  cdisselkoen

  committed
  daae656

  Copy full SHA for daae656

• Merge remote-tracking branch 'origin/main' into cdisselkoen/pe-soundness

  Show description for d667d98
  cdisselkoen

  committed
  d667d98

  Copy full SHA for d667d98

Commits on Aug 26, 2024

• tweak

  Show description for c3c802b
  cdisselkoen

  committed
  c3c802b

  Copy full SHA for c3c802b

Commits on Sep 13, 2024

• fill in some more sorrys

  Show description for 5f2d831
  cdisselkoen

  committed
  5f2d831

  Copy full SHA for 5f2d831