wp-framework

Rv64 WP Framework Guide

This guide explains the Rv64 weakest-precondition layer added under EvmAsm/Rv64/WP/. It is meant for proof authors who already know the separation-logic cpsTripleWithin style, but have not used the WP certificate mechanism before.

The short version: write the program and final postcondition, describe the control-flow shape, and let the WP layer build the precondition by composing certificates backwards. The final certificate still produces the usual total-correctness Hoare triple.

Imports

For ordinary users, import the CFG constructors and tactic surface:

import EvmAsm.Rv64.WP.CFG
import EvmAsm.Rv64.Tactics.WP

Most examples also need the existing block and frame tactics:

import EvmAsm.Rv64.Tactics.RunBlock
import EvmAsm.Rv64.Tactics.XPerm

Mental model

The main object is:

WP.CFG.Cert entry exit_ cr post

Read this as: starting at entry, the code requirement cr reaches exit_ within a generated step budget and establishes post.

A certificate stores the weakest-precondition result:

cfg.pre    -- Assertion generated by the WP calculus
cfg.sound  -- cpsTripleWithin cfg.nSteps entry exit_ cr cfg.pre post

So a top-level proof usually has this shape:

def cfg : WP.CFG.Cert entry exit_ cr post := ...

theorem spec :
    cpsTripleWithin cfg.nSteps entry exit_ cr cfg.pre post := by
  wp_rv64 cfg

wp_rv64 cfg is just the user-facing way to use cfg.sound.

Basic workflow

1. Define the public postcondition first.

   Keep outcomes in the postcondition. Do not put success, failure, decoded result, or branch choices in the precondition. A decoding routine should usually expose a disjunction such as "success with value" or "failure with status", with static guards carried inside the relevant disjuncts.

2. Synthesize straight-line leaf blocks from the postcondition when possible.

   For a single-exit leaf whose CodeReq is a concrete CodeReq.singleton, CodeReq.union, or CodeReq.ofProg tree, prefer wp_rv64_leaf_synth. The tactic works backwards from the requested postcondition, resolves registered @[spec_gen_rv64] instruction specs, and leaves the computed assertion as cfg.pre.