source: etc/campbell/dev-notes/2012-10-11-measurable-points-and-simulations.txt

Last change on this file was 2394, checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size: 1.8 KB
Line 
1Following Paolo's email to the list, I was thinking a little more about what
2our flat front-end simulations need to guarantee to prove the more detailed
3intensional result.  The rough idea I have is that we specify the measurable
4points we want the detailed result about and get a matching structured trace
5for the 8051 code.  The prefix needs to be preserved, but we don't need to
6know its structure:
7
8            --- ... ---
9            \         /
10    -- ... --\       /- ...
11  init      m         n
12
13However, we need to be able to obtain a number of steps corresponding to m
14in the object code execution, which a general simulation doesn't give us.
15
16The key point as I see it is that we should be able to guarantee that any
17labelled state in a source code execution has a corresponding state in the
18next language along (and hence the object code).  I'm less sure about how we
19state this precisely.
20
21
22Informally, if we have source and target programs p and p', some relation R on
23source and target states, we want something like
24
25∀n,s. exec p n = 〈trace,s〉→
26      labelled s →
27∃n',s'. exec p' n' = 〈trace,s'〉∧
28        R s s'.
29
30Along with R s s' → labelled s → labelled s'.
31
32The definition of simulates that I put in common/Executions.ma doesn't fit this.
33It allows a general m:n relationship between states, so we could lose labelled
34states ‘between the cracks’.  However, it wouldn't be that hard to change the
35definitions to rule out labelled states appear in the middle of an ‘m’, and
36instead having to be explicitly related.  That said, for current purposes we
37probably need something that exposes the actual relation used in the simulation,
38so we probably need something more detailed, anyway.  If that could then be used
39to get a plain proof of functional correctness that would be nice.
Note: See TracBrowser for help on using the repository browser.