Changeset 2342 for Papers

Sep 26, 2012, 2:43:19 PM (7 years ago)

simplified statements

1 edited


  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2341 r2342  
    375375    $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16).
    376376      policy is correct for program $\rightarrow$
    377       $\mid$program$\mid$ < $2^{16}$ $\rightarrow$
    378       $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$
    379       policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$
    380       policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$ $\wedge$
    381       $\forall$ppc: pseudo\_program\_counter such that ppc < $2^{16}$.
     377      $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$
     378      (policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$
     379      (policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$)) $\wedge$
     380      $\forall$ppc: pseudo_program_counter. ppc < $2^{16}$ $\rightarrow$
    382381        let pseudo_instr := fetch from program at ppc in
    383382        let assembled_i := assemble pseudo_instr in
    384383          $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$
    385             $\forall$n: nat such that n < $\mid$assembled_i$\mid$.
    386             $\exists$k: nat.
     384            $\forall$n: nat. n < $\mid$assembled_i$\mid$ $\rightarrow$ $\exists$k: nat.
    387385              nth assembled_i n = nth assembled (policy ppc + k).
     387[dpm: update]
    389388In plain words, the type of \texttt{assembly} states the following.
    390389Suppose we are given a policy that is correct for the program we are assembling, and suppose the program to be assembled is fully addressable by a 16-bit word.
    404403 $\forall$code_memory: BitVectorTrie Byte 16.
    405404 $\forall$assembled: list Byte.
    406   assembled = assembly1 i $\rightarrow$
    407   let len := length $\ldots$ assembled in
    408   let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ len) in
    409    encoding_check code_memory pc pc_plus_len assembled $\rightarrow$
    410    let $\langle$instr, pc', ticks$\rangle$ := fetch code_memory pc in
     405  assembled = assemble i $\rightarrow$
     406  let len := $\mid$assembled$\mid$ in
     407  let pc_plus_len := pc + len in
     408   encoding_check pc pc_plus_len assembled $\rightarrow$
     409   let $\langle$instr, pc', ticks$\rangle$ := fetch pc in
    411410    instr = i $\wedge$ ticks = (ticks_of_instruction instr) $\wedge$ pc' = pc_plus_len.
    421420lemma fetch_assembly_pseudo:
    422421 $\forall$program: pseudo_assembly_program.
    423  $\forall$sigma: Word $\rightarrow$ Word.
    424  $\forall$policy: Word $\rightarrow$ bool.
     422 $\forall$policy.
    425423 $\forall$ppc.
    426424 $\forall$code_memory.
    427425 let $\langle$preamble, instr_list$\rangle$ := program in
    428426 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in
    429  let pc := sigma ppc in
    430  let instrs := expand_pseudo_instruction $\ldots$ sigma policy ppc $\ldots$ pi in
    431  let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$ pi in
    432  let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ l) in
     427 let pc := policy ppc in
     428 let instrs := expand_pseudo_instructio sigma policy ppc pi in
     429 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction sigma policy ppc pi in
     430 let pc_plus_len := pc + l in
    433431  encoding_check code_memory pc pc_plus_len a $\rightarrow$
    434432   fetch_many code_memory pc_plus_len pc instructions.
    448446lemma fetch_assembly_pseudo2:
    449447 $\forall$program.
    450  $\forall$sigma.
     448 $\mid$snd program$\mid$ $\leq$ $2^{16}$ $\rightarrow$
    451449 $\forall$policy.
    452  $\forall$sigma_meets_specification.
    453  $\forall$ppc.
     450 policy is correct for program $\rightarrow$
     451 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$
    454452  let $\langle$preamble, instr_list$\rangle$ := program in
    455453  let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in
    456   let $\langle$assembled, costs'$\rangle$ := $\pi_1$ $\ldots$ (assembly program sigma policy) in
     454  let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in
    457455  let cmem := load_code_memory assembled in
    458456  let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in
    459   let instructions := expand_pseudo_instruction $\ldots$ sigma ppc $\ldots$ pi in
    460     fetch_many cmem (sigma newppc) (sigma ppc) instructions.
     457  let instructions := expand_pseudo_instruction policy ppc pi in
     458    fetch_many cmem (policy newppc) (policy ppc) instructions.
    506504We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM:
     506definition address_entry := upper_lower $\times$ Byte.
    508508definition internal_pseudo_address_map :=
    509   list ((BitVector 8) $\times$ (bool $\times$ Word)) $\times$ (option (bool $\times$ Word)).
    510 \end{lstlisting}
     509  (BitVectorTrie address_entry 7) $\times$ (BitVectorTrie address_entry 7)
     510    $\times$ (option address_entry).
     512[dpm update]
    511513The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set.
    512514Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes.
    521523The function is currently axiomatised, and an associated set of axioms prescribe the behaviour of the function:
    523 axiom low_internal_ram_of_pseudo_low_internal_ram:
    524  internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7.
     525definition low_internal_ram_of_pseudo_low_internal_ram:
     526 internal_pseudo_address_map $\rightarrow$ policy $\rightarrow$ BitVectorTrie Byte 7
     527  $\rightarrow$ BitVectorTrie Byte 7.
    531534definition status_of_pseudo_status:
    532535 internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap.
    533  $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool.
    534   Status (code_memory_of_pseudo_assembly_program pap sigma policy)
     536 $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap sigma policy)
    539541It thus decides the membership of a strict subset of the set of well behaved programs.
    541 definition next_internal_pseudo_address_map: internal_pseudo_address_map
    542  $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
    543 \end{lstlisting}
     543definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$
     544 $\forall$cm. (Identifier $\rightarrow$ PseudoStatus cm $\rightarrow$ Word) $\rightarrow$ $\forall$s: PseudoStatus cm.
     545   program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map
     547[dpm change]
    544548Note, if we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
    549553definition ticks_of0:
    550  pseudo_assembly_program $\rightarrow$ (Word $\rightarrow$ Word) $\rightarrow$ (Word $\rightarrow$ bool) $\rightarrow$ Word $\rightarrow$
    551    pseudo_instruction $\rightarrow$ nat $\times$ nat := $\ldots$
     554 pseudo_assembly_program $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ $\forall$policy. Word $\rightarrow$
     555   pseudo_instruction $\rightarrow$ nat $\times$ nat
    553557An additional function, \texttt{ticks\_of}, is merely a wrapper around this function.
    559563 $\forall$M, M': internal_pseudo_address_map.
    560564 $\forall$program: pseudo_assembly_program.
    561  let $\langle$preamble, instr_list$\rangle$ := program in
    562  $\forall$is_well_labelled: is_well_labelled_p instr_list.
    563  $\forall$sigma: Word $\rightarrow$ Word.
    564  $\forall$policy: Word $\rightarrow$ bool.
    565  $\forall$sigma_meets_specification.
    566  $\forall$ps: PseudoStatus program.
    567  $\forall$program_counter_in_bounds.
    568   next_internal_pseudo_address_map M program ps = Some $\ldots$ M' $\rightarrow$
    569   $\exists$n. execute n $\ldots$ (status_of_pseudo_status M $\ldots$ ps sigma policy) =
    570    status_of_pseudo_status M' $\ldots$ (execute_1_pseudo_instruction
    571      (ticks_of program sigma policy) program ps) sigma policy.
    572 \end{lstlisting}
     565 $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$.
     566 let maps := create_label_cost_map program in
     567 let addr_of := ... in
     568 program is well labelled $\rightarrow$
     569 $\forall$policy. policy is correct for program.
     570 $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$.
     571  next_internal_pseudo_address_map M program ... = Some M' $\rightarrow$
     572   $\exists$n. execute n (status_of_pseudo_status M ps policy) =
     573    status_of_pseudo_status M'
     574      (execute_1_pseudo_instruction program
     575       (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy.
     577[dpm change]
    573578The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}.
    574579Further, we explicitly require proof that our policy is correct and the pseudo program counter lies within the bounds of the program.
Note: See TracChangeset for help on using the changeset viewer.