Code

[do not merge] Metriclightbulb#435

Code

Draft

samuelgruetter wants to merge 24 commits intomastermit-plv/bedrock2:masterfrom metriclightbulbmit-plv/bedrock2:metriclightbulbCopy head branch name to clipboard

+2,810-494

Commits

Commits on Sep 16, 2024

• metrics versions of SPI proofs

  tckmn

  committed
  fd852ae

  Copy full SHA for fd852ae

• fix naming

  tckmn

  committed
  21c90e8

  Copy full SHA for 21c90e8

Commits on Sep 27, 2024

• metrics versions of LAN9250 and lightbulb

  tckmn

  committed
  1ecca9d

  Copy full SHA for 1ecca9d

• examples metrics proof for spi_write

  tckmn

  committed
  b487977

  Copy full SHA for b487977

Commits on Sep 29, 2024

• slightly clean up metric lan9250

  tckmn

  committed
  ddb6225

  Copy full SHA for ddb6225

Commits on Oct 2, 2024

• strengthen metrics statement

  Show description for d626eff
  tckmn

  committed
  d626eff

  Copy full SHA for d626eff

• finish spi metrics

  Show description for 78926d5
  tckmn

  committed
  78926d5

  Copy full SHA for 78926d5

Commits on Oct 3, 2024

• clean up spi metrics

  tckmn

  committed
  1fe5bd8

  Copy full SHA for 1fe5bd8

Commits on Nov 6, 2024

• MetricLightbulb skeleton

  andres-erbsen

  committed
  a122633

  Copy full SHA for a122633

Commits on Nov 8, 2024

• attempt lan9250_tx

  andres-erbsen

  committed
  0e36b33

  Copy full SHA for 0e36b33

Commits on Nov 12, 2024

• wip

  andres-erbsen

  committed
  aab339c

  Copy full SHA for aab339c

• new event-loop lemma with metrics WIP

  andres-erbsen

  committed
  93092eb

  Copy full SHA for 93092eb

Commits on Nov 13, 2024

• metric_lightbulb_correct first passing version

  andres-erbsen

  committed
  4fa46e0

  Copy full SHA for 4fa46e0

• check in theorem statement

  andres-erbsen

  committed
  9dcb030

  Copy full SHA for 9dcb030

• git mv end2end/src/end2end/MetricLightbulbInvariant.v compiler/src/compiler/

  andres-erbsen

  committed
  9b2358b

  Copy full SHA for 9b2358b

• still trying to get it to build...

  andres-erbsen

  committed
  f618e36

  Copy full SHA for f618e36

Commits on Nov 14, 2024

• prove mem_available_to_seplog admit/"hypothesis"

  samuelgruetter

  committed
  cbd05dd

  Copy full SHA for cbd05dd

• temporarily exclude end2end build target

  Show description for b6c1c1e
  samuelgruetter

  committed
  b6c1c1e

  Copy full SHA for b6c1c1e

• compat for Coq 8.18 is easy

  samuelgruetter

  committed
  2cdebfe

  Copy full SHA for 2cdebfe

• wip prettifying end-to-end metrics theorem

  samuelgruetter

  committed
  7c80fde

  Copy full SHA for 7c80fde

• wip proving prettified spec

  andres-erbsen

  committed
  4dea9bf

  Copy full SHA for 4dea9bf

• metrics for lan9250_recv_no_packet

  andres-erbsen

  committed
  0595cf9

  Copy full SHA for 0595cf9

• fix admits introduced by prettification, more prettification, DONE!

  samuelgruetter

  committed
  0ad32f6

  Copy full SHA for 0ad32f6

• Compute (loop_cost 1520 0).

  samuelgruetter

  committed
  5416e5b

  Copy full SHA for 5416e5b