Ignore:
Timestamp:
Jun 10, 2011, 6:36:55 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r937 r938  
    17611761    | Comment comment ⇒ 〈0, 0〉
    17621762    | Cost cost ⇒ 〈0, 0〉
    1763     | Jmp jmp ⇒ 〈0, 2〉
    1764     | Call call ⇒ 〈0, 2〉
    1765     | Mov dptr tgt ⇒ 〈0, 2〉
     1763    | Jmp jmp ⇒ 〈2, 2〉
     1764    | Call call ⇒ 〈2, 2〉
     1765    | Mov dptr tgt ⇒ 〈2, 2〉
    17661766    ].
    17671767  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
     
    19841984    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    19851985    #H2 >(eq_bv_to_eq … H2) >EQ %
    1986   |4: (* Jmp *)
     1986  |4: (* Jmp *) #label
     1987      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
     1988       [3: (* long *) #H1 #H2 #EQ %[@1]
     1989           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     1990           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     1991           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     1992           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     1993           >H2b >(eq_instruction_to_eq … H2a)
     1994           generalize in match EQ; -EQ;
     1995           (*whd in ⊢ (???% → ??%?);*)
     1996           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1997           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
     1998       | (* short *)
     1999       | (* medium *)
     2000       ] *)
    19872001  |5: (* Call *)
    19882002  |6: (* Mov *)
Note: See TracChangeset for help on using the changeset viewer.