@cella-lang/programlogic

A language-generic program logic for the Cella proof checker, as a compiled module pack. A language gives one step and a separation algebra of resources; the package gives the weakest precondition, its soundness, and the structural rules.

No dependencies besides cella-lang's standard modules.

Plugging in a language

• programlogic.Step C V S W: the result of one step: advance c s (a new configuration and state), finish v s (a final value) or fault w (a fault with its reason; for C, undefined behavior with its node and clause).
• programlogic.Language C V S W: { step : C -> S -> Step C V S W }.
• programlogic.SeparationAlgebra S R: resources R with join a b c (a and b are disjoint and together make c), a unit with joinUnit, both directions of associativity (associateRight: from (a b) c to a (b c); associateLeft), and interpret s r (the state s holds the resource r).

The small-step machine of @cella-lang/machine (which the C family and Python run on) plugs in like this, with a statement and its frames as the configuration:

import machine.statement
import programlogic
open machine

def Cfg (S : Type) (R : Type) : Type := Statement S R String * List (Frame S R String)

def exitStep {S : Type} {R : Type} (e : Exit S R String) : programlogic.Step (Cfg S R) (Exit S R String) S String := match e with
  | stopped w => programlogic.fault w
  | normal s => programlogic.finish (normal s) s
  | breakOut s => programlogic.finish (breakOut s) s
  | continueLoop s => programlogic.finish (continueLoop s) s
  | returned v s => programlogic.finish (returned v s) s

def confStep {S : Type} {R : Type} (x : Configuration S R String) : programlogic.Step (Cfg S R) (Exit S R String) S String := match x with
  | running c k s => programlogic.advance (c, k) s
  | halted e => exitStep e

def lang (S : Type) (R : Type) : programlogic.Language (Cfg S R) (Exit S R String) S String :=
  { step := fun c s => confStep (Configuration.stepRun (fst c) (snd c) s) }

With the whole state owned exclusively as the resource, this proves while (x != 0) x = x - 1; (whileLoop with an update that stops on x = 0) safe for every x, and runs do { x = x - 1; } while (x != 0); from x = 0 to its fault.

What you get

• programlogic.Wp L A c Q r: from resource r, running c never reaches a fault, and if it finishes with v, Q v r' holds for the remaining resource. It is WpWithin n for every n, explicitly step-indexed (Appel and McAllester 2001; Ahmed 2006): no guarded fixed point is needed, and a loop rule is proved by induction on the number of steps. The frame is part of the definition (as in Charguéraud's Separation Logic Foundations).
• After a step, the resource is an Owned A frame s X: a record with the resource, the whole resource it makes with the frame, the proof they are joined, that the state held the whole, and that the resource satisfies X.
• programlogic.safeOfWp: Wp L A c Q r -> A.interpret s r -> L.Safe c s, where L.Safe c s is: for every n, L.run n c s has not failed (partial correctness: termination is not required).
• programlogic.wpConsequence (consequence), programlogic.wpFrame (frame: a disjoint resource is carried along unchanged, WithFrame), programlogic.wpWithinOfSucc (one more step implies one fewer).
• Verdicts: a proved Wp is Accept; an input and a number of steps for which run reaches failed w is Reject (by computation, carrying w); otherwise Unknown.