rocq/theories/Symbolic.v
Symbolic execution of the model's step, for proofs that a program never panics from assertions at its points (Cycle.v).
A program proof states what holds at each point of its function, as facts about the temporaries of the environment: the word a name holds, and a range for an integer. It then shows that one step from any configuration where the facts hold reaches a point where its facts hold, or ends without a failure (Panics.v's never_panics_by_invariant). That step is computed here with the environment, the memory and the fuel left abstract: the reduction stops where it needs a value it does not have, the facts supply it, and an integer comparison is decided by linear arithmetic over the facts' ranges, or split into its two answers when the facts do not decide it.
Cycle.v and Buffer.v take each step by its rule from StepRules.v (take_step): the step itself is never reduced, only its rule's premises, with the same facts, wraps and comparisons.
Decisions
| Decision | Why |
|---|---|
integer arithmetic stays folded on an unknown (simplnomatch, set by each program file, since Rocq exports no such setting) | unfolded, 65552 + x becomes a match on the bits of x as deep as 65552 is long, which neither a fact nor arithmetic can read; on numbers it still computes |
the step is reduced by cbn, not cbv | cbn leaves a function stuck on an unknown value folded (i mod 4294967296, lookupx e), where a fact can be rewritten; cbv unfolds it into a term no fact matches, and does not finish on a remainder of a variable |
| linear arithmetic decides comparisons, with remainders and quotients by constants turned into equations | the bounds a check compares are sums and multiples of the facts' integers; lia alone does not know mod or rem |
| a remainder of a value proved in range is the value, and any other remainder an unknown in range | the model wraps every result to its class; where the facts bound it, the wrap is the identity, and dropping it keeps the terms small; where they do not, as for the input, the range is all a step needs, and each wrap or comparison is then tried once |
| an undecided comparison is split, both answers kept | the input is unknown: the comparison with it goes either way, and the facts after it say which |
Facts about an environment
Looking k up after put k' v answers v if k is k', and otherwise what it answered before.
Explore proof 11 tactics
Initial goal
intros A k k′ v ps
unfold put
simpl
destruct name_eqbk k′ eqn: E ; reflexivity |
induction ps as | k0 v0 ps IH ; simpl ; reflexivity |
destruct name_eqbk′ k0 eqn: E0 ; simpl
2 open–apply term_eqb_eq in E0
2 opensubst k0
2 openrewrite E
2 openexact IH
–destruct name_eqbk k0 ; reflexivity | exact IH
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Looking k up after put k answers its new value.
Explore proof 3 tactics
Initial goal
intros A k v ps
rewrite lookup_after_put , term_eqb_refl
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
Looking k up after put of another name answers what it answered before.
Explore proof 3 tactics
Initial goal
intros A k k′ v ps H
rewrite lookup_after_put , H
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
A store of bytes changes no object's region.
Explore proof 1 tactics
Initial goal
reflexivity
No remaining goals.
Qed
✓ Proof checked and closed by Rocq.
Source script
The name x holds an integer word of e that P allows.
Any integer.
Arithmetic
The goal has a remainder or quotient in it.
Replace each remainder x mod m by a literal m with a new variable in [0, m), everywhere. Cheaper for lia than the division equations Z.to_euclidean_division_equations gives, and enough wherever the remainder's bounds are all an argument needs.
The arithmetic oracle: linear arithmetic over the integers, with the powers of two the model's classes use as numbers, and where the goal divides, with remainders and quotients by constants first turned into equations. Facts about environments and memory are set aside first; they say nothing arithmetic. So are the bodies of local definitions (a function, or a program's computed runs), which the rewriting in every hypothesis below would otherwise walk.
arith without the division equations: for the side goals that may well be false (dropping a wrap, deciding a comparison), where a failing attempt should cost little.
Fails unless the term t has an if in it.
Fails unless the term t has a remainder in it.
Drop the wraps in E, innermost first, once what each wraps holds no other wrap and no undecided comparison: a remainder or quotient of a nonnegative value is Euclid's, and a wrap that arithmetic over the context, without E, proves is the identity goes. A wrap it does not, of the input say, becomes an unknown known to lie between 0 and the modulus. So each wrap is tried once.
Decide the integer comparisons in E: true or false where arithmetic over the context proves it, and otherwise split into its two answers at once, each kept as a fact, so that no comparison is tried twice. A comparison whose operands hold another comparison waits until that one is decided.
The step
Rewrite in E every fact in the context that names a temporary of an environment, the region of an object in a memory, or a block or the return class of the function, which a proof keeps abstract (block_fact) so that its whole body is not carried through every step.
Reduce E as far as the facts and arithmetic allow: cbn, keeping a load's and a store's bytes folded, then the definitions cbn leaves folded (stuck on an unknown, such as an access check on the memory's regions, or building a record), the facts and the fields they supply, the wraps and the comparisons, until nothing changes.
Compute E, an equation r = step g c, to a result: reduce it, in every case of the comparisons the facts leave open.
Facts after a step
Take apart the facts in the context: conjunctions, existentials, and each case of a disjunction.
Prove a fact about the configuration after a step: look each name up through the step's puts to the facts before it, each object's region through the stores, which change none, and through a new object's, and the ranges as facts or by arithmetic.
The function, kept abstract
The block l of the function fn, computed once as b, and the fact H that the abstract f, equal to fn by Hf, has it: the step finds a block through H instead of reducing f's body.
A step by its rule
Instead of reducing step with the function and the memory inside it, take_step names the instruction at the frame's point, rewrites the step with its rule from StepRules.v, and proves the rule's premises one by one (premise). Each premise is small: a temporary's value, an op on those words, an access check, a block of the function. The words the premises compute become the rule's result, and a comparison of the input that the facts do not decide is split there (split_compares).
Rewrite in the goal every fact in the context that names a temporary of an environment or the region of an object.
Replace each environment put k v e of the goal, e a variable, by a new variable, with what each name looks up to in it.
Drop each wrap in the goal that arithmetic over the context proves is the identity, and turn a remainder or quotient of a nonnegative value into Euclid's. A wrap it does not drop stays.
Decide each integer comparison in the goal that arithmetic over the context decides; leave the others.
Decide each integer comparison in the goal, splitting the goal in its two answers where the facts do not decide it, each kept as a fact. A comparison whose operands hold another waits for it. The split is a case, which looks at the goal alone, not at the definitions in the context (a program's computed runs, say).
Prove a premise lhs = rhs whose right side the proof leaves open: compute lhs by cbn, with the facts, the wraps and the comparisons the facts decide, then take rhs to be what it computed.
Prove that an access check passes: through the capability of an object, read-only or not, whose region a fact gives, at an address arithmetic shows in its bounds and aligned (any address is, to 1).
Prove one premise of a rule from StepRules.v: by computation for the op's classes, by a fact or computation for a block (a block_fact) and the return class, by the lemma of the op for a check, a load and a store, with access_ok after it, and otherwise by compute_premise.
Rewrite the step in the goal, at a frame that is not doomed, by the rule of its point: entering a block (out of fuel or not, the fuel split), an allocation, any other let, a flight, a raw store, a goto, a branch, or a return of an invocation with no caller.
Take the step in the goal by its rule (step_by_rule), then the jump's target, and split where the step compared the input.