Changeset 2051 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 12, 2012, 5:49:02 PM (8 years ago)
Author:
mulligan
Message:

Finished the Jmp case in the main theorem.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2048 r2051  
    2020  λpc_plus_jmp_length.λaddr.(*λinstr.*)
    2121  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    22   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
     22  let 〈upper, lower〉 ≝ vsplit ? 9 7 result in
    2323    if get_index' ? 2 0 flags then
    24       〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉
     24      〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉
    2525    else
    26       〈eq_bv 8 upper (zero 8), zero 8〉.
     26      〈eq_bv 9 upper (zero …), false:::lower〉.
    2727 
    2828definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
Note: See TracChangeset for help on using the changeset viewer.