Changeset 2318


Ignore:
Timestamp:
Sep 3, 2012, 12:42:47 PM (7 years ago)
Author:
boender
Message:
  • now it compiles
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2317 r2318  
    635635 [ <plus_n_O #_ @le_n
    636636 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
    637    lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H)
     637   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (λx.zero 16) (i+n) H)
    638638   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
    639639   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
     
    680680   cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
    681681   #lbl #ins % ]
    682   lapply (Hfpol3 (nat_of_bitvector ? ppc) ppc_ok) >bitvector_of_nat_inverse_nat_of_bitvector
     682  lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok)
     683  [2: >bitvector_of_nat_inverse_nat_of_bitvector
    683684  inversion (lookup_opt ????) normalize nodelta [ #Hl #abs cases abs ]
    684685  * #pc #jl #Hl normalize nodelta
     
    721722          [2: >Hcompact in HSpc; #X @X
    722723          | #ppc' #ppc_ok' #Hppc'
    723                 (* S ppc < ppc' < |\snd program| *)
    724                 (* lookup S ppc = 2^16 *)
    725                 (* lookup |\snd program| = 2^16 *)
    726                 (* lookup ppc' = 2^16 → instruction size = 0 *)
    727                 lapply (Hfpol3 (nat_of_bitvector ? ppc') ppc_ok')
     724            (* S ppc < ppc' < |\snd program| *)
     725            (* lookup S ppc = 2^16 *)
     726            (* lookup |\snd program| = 2^16 *)
     727            (* lookup ppc' = 2^16 → instruction size = 0 *)
     728            lapply (Hfpol3 ? (nat_of_bitvector ? ppc') ppc_ok')
     729            [2: >bitvector_of_nat_inverse_nat_of_bitvector
     730            inversion (lookup_opt ????) normalize nodelta
     731            [ #_ #abs cases abs
     732            | * #xpc #xjl #XEQ normalize nodelta
     733              inversion (lookup_opt ????) normalize nodelta
     734              [ #_ #abs cases abs
     735              | * #Sxpc #Sxjl #SXEQ normalize nodelta
     736                #Hpcompact
     737                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
     738                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
     739                lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
     740                <Hfpol2 >Hfpc #Hle2
     741                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
    728742                >bitvector_of_nat_inverse_nat_of_bitvector
    729                 inversion (lookup_opt ????) normalize nodelta
    730                 [ #_ #abs cases abs
    731                 | * #xpc #xjl #XEQ normalize nodelta
    732                   inversion (lookup_opt ????) normalize nodelta
    733                   [ #_ #abs cases abs
    734                   | * #Sxpc #Sxjl #SXEQ normalize nodelta
    735                     #Hpcompact
    736                     lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
    737                     >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    738                     lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
    739                     <Hfpol2 >Hfpc #Hle2
    740                     lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
    741                     >bitvector_of_nat_inverse_nat_of_bitvector
    742                     >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
    743                     lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
    744                     >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
    745                     lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
    746                     <Hfpol2 >Hfpc #Hle2
    747                     lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
    748                     >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
    749                     >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
    750                     @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
    751                     normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
    752                     cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
    753                     #lbl #ins normalize nodelta #X @sym_eq @X
    754                   ]
    755                 ]
     743                >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
     744                lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
     745                >(lookup_opt_lookup_hit … SHL 〈0,short_jump〉) >HSpc #Hle1
     746                lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
     747                <Hfpol2 >Hfpc #Hle2
     748                lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
     749                >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
     750                >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
     751                @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
     752                normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
     753                cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
     754                #lbl #ins normalize nodelta #X @sym_eq @X
     755              ]
     756            ] ]
    756757          ]
    757758        ]
     
    761762        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
    762763        <plus_O_n whd in match instruction_size; normalize nodelta
    763         inversion (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)
     764        inversion (assembly_1_pseudoinstruction ??? ppc ??)
    764765        #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
    765766        #Hli >Hli
    766         lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
    767         [5: >Hass / by / ]
     767        lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc ??)
     768        [6: >Hass / by / ]
    768769      ]
    769770    ]
    770   ]
    771 ]
    772 qed.
     771  ] ]
     772]
     773qed.
  • src/ASM/PolicyFront.ma

    r2316 r2318  
    182182definition sigma_compact ≝
    183183 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    184  ∀n.n < |program| →
     184 ∀datalabels.∀n.n < |program| →
    185185  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    186186  [ None ⇒ False
     
    190190    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    191191       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    192          (λx.zero ?)
     192         datalabels
    193193         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    194194         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
     
    615615  sigma_compact program (create_label_map program) sigma.
    616616  #program cases program -program #program #Hprogram #old_sigma #sigma
    617   #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #i #Hi
     617  #Hpc_equal #Hjump_equal #Hjumps #Hsafe #Hcp_unsafe #dlbl #i #Hi
    618618  lapply (Hcp_unsafe i Hi) -Hcp_unsafe lapply (Hsafe i Hi) -Hsafe
    619619  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
Note: See TracChangeset for help on using the changeset viewer.