Changeset 845


Ignore:
Timestamp:
May 25, 2011, 6:09:38 PM (8 years ago)
Author:
sacerdot
Message:

Nightmare...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r841 r845  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
     3
     4(* RUSSEL **)
     5
     6include "basics/jmeq.ma".
     7
     8definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     9definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
     10
     11coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
     12coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
     13
     14axiom VOID: Type[0].
     15axiom assert_false: VOID.
     16definition bigbang: ∀A:Type[0].∀P:A → Prop. False → VOID → Σx:A.P x.
     17 #A #P #abs cases abs
     18qed.
     19
     20(*coercion bigbang : ∀A.∀P:A → Prop.False → ∀v:VOID.Σx:A.P x ≝ bigbang on _v:VOID to Σx:?.?.*)
     21
     22lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
     23 #A #P #p cases p #w #q @q
     24qed.
     25
     26(* END RUSSELL **)
    327
    428(* This establishes the correspondence between pseudo program counters and
    529   program counters. It is at the heart of the proof. *)
    630(*CSC: code taken from build_maps *)
    7 definition sigma: pseudo_assembly_program → option (Word → Word) ≝
     31definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    832 λinstr_list.
    9   let result ≝ foldl ??
     33  foldl ??
    1034    (λt. λi.
    1135       match t with
     
    2044              let 〈pc,ignore〉 ≝ pc_ignore in
    2145              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    22        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
    23   match result with
     46       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
     47       
     48definition tech_pc_sigma0: pseudo_assembly_program → option nat ≝
     49 λinstr_list.
     50  match sigma0 instr_list with
     51   [ None ⇒ None …
     52   | Some result ⇒
     53      let 〈ppc,pc_sigma_map〉 ≝ result in
     54      let 〈pc, sigma_map〉 ≝ pc_sigma_map in
     55       Some … pc ].
     56
     57definition sigma: pseudo_assembly_program → option (Word → Word) ≝       
     58 λinstr_list.
     59  match sigma0 instr_list with
    2460  [ None ⇒ None ?
    2561  | Some result ⇒
     
    3066      else
    3167        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
     68
     69axiom policy_ok: ∀p. sigma p ≠ None ….
     70
     71axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
     72
     73definition build_maps' ≝
     74  λpseudo_program.
     75  let 〈preamble,instr_list〉 ≝ pseudo_program in
     76  let result ≝
     77   foldl
     78    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
     79          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
     80           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
     81    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
     82          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
     83           is_prefix ? instr_list_prefix' instr_list ∧
     84           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
     85    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
     86          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
     87           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
     88     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
     89          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
     90           is_prefix ? instr_list_prefix' instr_list ∧
     91           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
     92      let 〈labels, pc_costs〉 ≝ t in
     93      let 〈program_counter, costs〉 ≝ pc_costs in
     94       let 〈label, i'〉 ≝ i in
     95       let labels ≝
     96         match label with
     97         [ None ⇒ labels
     98         | Some label ⇒
     99           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     100             insert ? ? label program_counter_bv labels
     101         ]
     102       in
     103         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
     104         [ None ⇒ 〈labels,pc_costs〉 (*assert_false*)
     105         | Some construct ⇒ 〈labels, construct〉
     106         ]
     107    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 (\snd ?(*instr_list*))
     108  in
     109   let 〈labels, pc_costs〉 ≝ result in
     110   let 〈pc, costs〉 ≝ pc_costs in
     111    〈labels, costs〉.
     112 [ cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
     113     % [@ (LIST_PREFIX @ [i])] %
     114      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
     115      | (* DOABLE IN PRINCIPLE *)
     116      ]
     117 | (* assert false case *)
     118 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
     119 |
     120     
     121
    32122
    33123
     
    109199           (clock … ps)) ].
    110200           
    111 (* RUSSEL **)
    112 
    113 include "basics/jmeq.ma".
    114 
    115 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
    116 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
    117 
    118 coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
    119 coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    120 
    121 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
    122  #A #P #p cases p #w #q @q
    123 qed.
    124 
    125 (* END RUSSELL **)
    126 
    127201definition write_at_stack_pointer':
    128202 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
Note: See TracChangeset for help on using the changeset viewer.