Changeset 848


Ignore:
Timestamp:
May 26, 2011, 6:26:57 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r847 r848  
    1818qed.
    1919
    20 (*coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
     20coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
    2121
    2222lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
     
    5555       Some … pc ].
    5656
    57 definition sigma: pseudo_assembly_program → option (Word → Word) ≝       
     57definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
    5858 λinstr_list.
    5959  match sigma0 instr_list with
     
    6767        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
    6868
    69 axiom policy_ok: ∀p. sigma p ≠ None ….
     69axiom policy_ok: ∀p. sigma_safe p ≠ None ….
     70
     71definition sigma: pseudo_assembly_program → Word → Word ≝
     72 λp.
     73  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
     74   [ None ⇒ λabs. ⊥
     75   | Some r ⇒ λ_.r] (policy_ok p).
     76 cases abs //
     77qed.
     78
     79(*
     80definition build_maps' ≝
     81  λpseudo_program.
     82  let 〈preamble,instr_list〉 ≝ pseudo_program in
     83  let result ≝
     84   foldl
     85    ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))
     86    (option Identifier × pseudo_instruction)
     87    (λt,i.
     88      let 〈labels, pc_costs〉 ≝ t in
     89      let 〈program_counter, costs〉 ≝ pc_costs in
     90       let 〈label, i'〉 ≝ i in
     91       let labels ≝
     92         match label with
     93         [ None ⇒ labels
     94         | Some label ⇒
     95           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     96             insert ? ? label program_counter_bv labels
     97         ]
     98       in
     99         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
     100         [ None ⇒
     101            let dummy ≝ 〈labels,pc_costs〉 in
     102             dummy
     103         | Some construct ⇒ 〈labels, construct〉
     104         ]
     105    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
     106  in
     107   let 〈labels, pc_costs〉 ≝ result in
     108   let 〈pc, costs〉 ≝ pc_costs in
     109    〈labels, costs〉.
     110
     111(*
     112notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     113 with precedence 10
     114for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     115*)
     116
     117lemma build_maps_ok:
     118 ∀p:pseudo_assembly_program.
     119  let 〈labels,costs〉 ≝ build_maps' p in
     120   ∀pc.
     121    (nat_of_bitvector … pc) < length … (\snd p) →
     122     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
     123 #p cases p #preamble #instr_list
     124  elim instr_list
     125   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
     126   | #hd #tl #IH
     127    whd in ⊢ (match % with [ _ ⇒ ?])
     128   ]
     129qed.
     130*)
     131
     132(*
     133lemma list_elim_rev:
     134 ∀A:Type[0].∀P:list A → Prop.
     135  P [ ] → (∀n,l. length l = n → P l → 
     136  P [ ] → (∀l,a. P l → P (l@[a])) →
     137   ∀l. P l.
     138 #A #P
     139qed.*)
     140
     141lemma length_append:
     142 ∀A.∀l1,l2:list A.
     143  |l1 @ l2| = |l1| + |l2|.
     144 #A #l1 elim l1
     145  [ //
     146  | #hd #tl #IH #l2 normalize <IH //]
     147qed.
     148
     149lemma rev_preserves_length:
     150 ∀A.∀l. length … (rev A l) = length … l.
     151  #A #l elim l
     152   [ %
     153   | #hd #tl #IH normalize >length_append normalize /2/ ]
     154qed.
     155
     156lemma rev_append:
     157 ∀A.∀l1,l2.
     158  rev A (l1@l2) = rev A l2 @ rev A l1.
     159 #A #l1 elim l1 normalize //
     160qed.
     161 
     162lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
     163 #A #l elim l
     164  [ //
     165  | #hd #tl #IH normalize >rev_append normalize // ]
     166qed.
     167
     168lemma split_len_Sn:
     169 ∀A:Type[0].∀l:list A.∀len.
     170  length … l = S len →
     171   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
     172 #A #l elim l
     173  [ normalize #len #abs destruct
     174  | #hd #tl #IH #len
     175    generalize in match (rev_rev … tl)
     176    cases (rev A tl) in ⊢ (??%? → ?)
     177     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
     178     | #a #l' #H <H normalize #EQ
     179      %[@(hd::rev … l')] %[@a] % //
     180      >length_append in EQ #EQ normalize in EQ; normalize;
     181      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
     182qed.
     183
     184lemma list_elim_rev:
     185 ∀A:Type[0].∀P:list A → Type[0].
     186  P [ ] → (∀l,a. P l → P (l@[a])) →
     187   ∀l. P l.
     188 #A #P #H1 #H2 #l
     189 generalize in match (refl … (length … l))
     190 generalize in ⊢ (???% → ?) #n generalize in match l
     191 elim n
     192  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
     193  | #m #IH #L #EQ
     194    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
     195qed.
    70196
    71197axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
    72 
    73 (*
     198axiom prefix_of_append:
     199 ∀A:Type[0].∀l,l1,l2:list A.
     200  is_prefix … l l1 → is_prefix … l (l1@l2).
     201
    74202definition build_maps' ≝
    75203  λpseudo_program.
     
    82210    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    83211          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    84            is_prefix ? instr_list_prefix' instr_list
     212           is_prefix ? instr_list_prefix' instr_list
    85213           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
    86214    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
     
    89217     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    90218          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    91            is_prefix ? instr_list_prefix' instr_list
     219           is_prefix ? instr_list_prefix' instr_list
    92220           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
    93221      let 〈labels, pc_costs〉 ≝ t in
     
    103231       in
    104232         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
    105          [ None ⇒ 〈labels,pc_costs〉 (*assert_false*)
     233         [ None ⇒
     234            let dummy ≝ 〈labels,pc_costs〉 in
     235              dummy
    106236         | Some construct ⇒ 〈labels, construct〉
    107237         ]
    108     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 (\snd ?(*instr_list*))
     238    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
    109239  in
    110240   let 〈labels, pc_costs〉 ≝ result in
    111241   let 〈pc, costs〉 ≝ pc_costs in
    112242    〈labels, costs〉.
    113  [ cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
     243 [4: @(list_elim_rev ?
     244       (λinstr_list. list (
     245        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
     246          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
     247           is_prefix ? instr_list_prefix' instr_list →
     248           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
     249       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
     250      [ @[ ]
     251      | #l' #a #limage %2
     252        [ %[@a] #PREFIX #PREFIX_OK
     253        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
     254             THE INDUCTION HYPOTHESIS INSTEAD *)
     255          elim limage
     256           [ %1
     257           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
     258             @K1 @(prefix_of_append ???? K3)
     259           ] 
     260        ]
     261       
     262       
     263     
     264 
     265  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
    114266     % [@ (LIST_PREFIX @ [i])] %
    115267      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
     
    118270 | (* assert false case *)
    119271 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
    120  |
    121 *)     
     272 |   
    122273
    123274let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
Note: See TracChangeset for help on using the changeset viewer.