Specifications and abstractions in Coq ====================================== Goal: reason about possible executions. Same as in Butler's view. Lower layer: Code (implementation) Concrete (code-level) states Transition between code-level states, dictated by execution semantics of code Upper layer: Code is the same, but we want to describe its behavior with a "spec" Abstract states: just like Butler's lecture on Monday connected to the code states using an abstraction relation (AR) Transition between abstract-level states, dictated by a specification of what this code should do Goal: any code-level execution corresponds to a spec-level execution. Intuitively matches the "trace-subset" property. Although our Coq formalization doesn't have a notion of traces. So what is a specification? Abstraction for the state Description of transitions for each piece of code ("procedure") Abstraction of states Nested: can continue to abstract at many levels E.g., bare hardware states -> variable-level states -> StatDB-level state Description of transitions pre- and post-conditions precondition may constrain the starting state (or could be just True, if we have no constraints) postcondition describes which final states are acceptable could be non-deterministic: many final states are OK as far as the spec goes postcondition also explicitly refers to the return value same plan for describing transitions (pre and post conditions) works at any level only difference: what type of state you're describing code-level transitions: code-level state abstract-level transitions: abstract state What does it mean to prove that a piece of code satisfies a spec? recall Butler's simulation "commutative diagram" s ======> s' ^ ^^ | AR || V VV c ------> c' horizontal arrows are allowed transitions according to the spec (pre/post conditions) vertical arrows are the abstraction relations between code and spec single lines are given in the theorem: suppose there is a code state "c", which transitions to state "c'" and suppose there is a spec state "s" related to "c" by AR double lines are what you have to prove: show there exists a valid transition from "s" to "s'" according to spec pre/post conditions and show that this same "s'" is related to "c'" using the AR Can stack commutative diagrams in two ways Side-by-side: combine two procedures with a semicolon Sequential composition What are the rules? Postcondition of the first part must imply the precondition of the second part One-above-another: provide an even higher-level specification, more abstraction What are the rules? AR types need to match up Why preconditions? More succinct spec Does not specify what happens if precondition is violated Might be fine, but assuming precondition might make for a simpler postcondition Using procedure with a non-trivial precondition requires proving precondition holds Typically useful for routines used in the middle of some code E.g., in Butler's example of memory from last lecture: in some cases, we know there's a free cache slot. Easier to write a spec that says (precondition) "assuming there's a free cache slot", (postcondition) "the cache will now contain XXX". Example: variables, StatDB StatDB state: list nat Variable state: sum (nat), count (nat) Abstraction relation: |l| = count /\ Sum(l) = sum Code (only one piece of code): add(x): sum += x; count += 1; mean(): return sum/count; Semantics for variables: let's assume they are obvious (will look at Coq code soon) Semantics for StatDB: mean(): PRE: True POST: r = Sum(l) / |l| /\ state' = state add(x): PRE: True POST: state' = state ++ [x] Diagram for mean list l ===========================> list l' ^ ^^ | || V return sum/count VV sum, count ---------------------> sum', count' Proof: Exists state? Yes, l' = l. Exists relation? Yes, same relation. Observe sum' = sum, count' = count, .. Postcondition satisfied? Yes. Diagram for add(x) list l ====================================> list ?? ^ ^^ | || V sum += x count += 1 VV sum, count -----------> [?] ------------> sum', count' Proof: Exists state? Yes, l' = l ++ [x] Exists relation? Yes, because: Observe sum' = sum + x Observe count' = count + 1 Relation matches l' Postcondition satisfied? Yes. What's going on with the middle state, [?] sum? = sum + 1 count? = count No matching abstract state In our lab approach to modeling specs, it doesn't make sense to peek inside the procedure's execution and describe it using the abstract state. Valid AR re-established only at procedure return. Abstraction relation incorporates an invariant i.e., some code states might not have a corresponding abstract states concrete example from above, rather than just symbolic? sum = 2 count = 0 also incorporate history variables, as Butler mentioned many possible lists could correspond to the same sum/count code state Initialization Special kind of procedure Starts with a code-level state Returns a spec-level state (or a special return value indicating it didn't work) One subtle issue in our model: representing that the code is always the same. Abstraction levels can shift, specs can be different, but code is always code For the same piece of code, can write different specs, at different abstraction levels But need to agree that the same code always runs the same way, independent of abstraction We define a basic type for state, called [world] Axiom in Coq, not actually something that can be examined Meant to represent the real state of the machine (and rest of world) where code runs We define a basic type for how code looks like (procedures) Also, mostly opaque in Coq Meant to represent low-level Haskell code, but we won't be reasoning about it directly Except for two special operations: Return a value Connect two procedures together with a semicolon This maps onto what Haskell calls the "IO monad" Finally, we define an opaque semantics for how code runs Again, defined via Axiom Represents how Haskell runs the opaque low-level code But we won't be reasoning about it directly Our typical examples start by assuming there's already an abstraction stack, from [world] to some simple state type, like variables in StatDB example/lab Then we construct one more layer on top of that abstraction (e.g., StatDB). Let's look at code: VariablesAPI. easy to miss detail: inited_any StatDBAPI. inited Spec.Proc. Crash handling largely irrelevant for now; will come back to it. Spec.Abstraction.