Code

Wp is really exec#364

Code

Open

samuelgruetter wants to merge 16 commits intomastermit-plv/bedrock2:masterfrom wp_is_really_execmit-plv/bedrock2:wp_is_really_execCopy head branch name to clipboard

+1,232-757

Commits

Commits on Jul 26, 2023

• define a WP.cmd' in terms of exec, might soon replace WP.cmd

  Show description for 9f6b294
  samuelgruetter

  committed
  9f6b294

• dead simple call based on map.get

  samuelgruetter

  committed
  aa6b219

• convert from "fs everywhere" to "env everywhere"

  samuelgruetter

  committed
  18d9e85

Commits on Jul 28, 2023

• instead of unfold1_cmd_goal, eapply lemma_corresponding_to_command

  Show description for b83d340
  samuelgruetter

  committed
  b83d340

Commits on Jul 29, 2023

• wip "env everywhere" approach

  samuelgruetter

  committed
  069a89d

Commits on Jul 31, 2023

• make WeakestPrecondition.cmd complete wrt exec

  Show description for 88c5d5e
  samuelgruetter

  committed
  88c5d5e

Commits on Aug 1, 2023

• hardcode env implementation in bedrock2.Semantics,

  Show description for 8fa2cc3
  samuelgruetter

  committed
  8fa2cc3

Commits on Aug 2, 2023

• add back program/Proper_program because it's used by rupicola

  samuelgruetter

  committed
  a20ca4d

• cp Semantics.v MetricSemantics.v

  samuelgruetter

  committed
  54e32e1

Commits on Aug 3, 2023

• bedrock2.Semantics is now metrics-free, and metrics are in MetricSemantics

  samuelgruetter

  committed
  4eed032

Commits on Aug 4, 2023

• refinement lemmas for induction over command syntax

  samuelgruetter

  committed
  c0efbad

Commits on Aug 6, 2023

• delete WP.v (opaque Module), only LAN9250 needed fixing

  samuelgruetter

  committed
  6faf7a0

• LiveVerif: wp_cmd is exec instead of WeakestPrecondition.cmd

  samuelgruetter

  committed
  fb4def2

• wip making WeakestPrecondition.cmd an alias of Semantics.exec

  samuelgruetter

  committed
  218ece4

• port more examples from wp to exec

  

  andres-erbsen

  authored and

  samuelgruetter

  committed
  d94f626

• memmove, memequal, LAN9250 still don't work

  samuelgruetter

  committed
  5062f79