Ignore:
Timestamp:
Jul 18, 2012, 3:57:09 PM (8 years ago)
Author:
boender
Message:
  • finished proof of sigma specification
  • added some stuff to Util, as usual
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2152 r2211  
    122122   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in
    123123   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in
    124      (*opc ≤ pc ∧*) jmpleq oj j.
     124     jmpleq oj j.
    125125     
    126126(* this is the instruction size as determined by the jump length given *)
     
    407407       (∀i.i ≤ |program| → ∃pc.
    408408         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    409        (\fst p < 2^16)         
     409       (\fst p 2^16)         
    410410    ] ≝
    411411  λprogram.λlabels.
     
    425425   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
    426426  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
    427   if geb (\fst (pi1 ?? final_policy)) 2^16 then
     427  if gtb (\fst (pi1 ?? final_policy)) 2^16 then
    428428    None ?
    429429  else
     
    431431[ / by I/
    432432| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    433   @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    434 | @conj [ @conj [ @conj [ @conj (*[@conj
    435   [ (* out_of_program_none *)
    436     #i #Hi2 >append_length <commutative_plus @conj
    437     [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
    438       cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    439       [ >lookup_opt_insert_miss
    440         [ (* USE[pass]: out_of_program_none → *)
    441           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
    442           @le_S_to_le @le_S_to_le @Hi
    443         | @bitvector_of_nat_abs
    444           [ @Hi2
    445           | @(transitive_lt … Hi2) @le_S_to_le @Hi
    446           | @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    447           ]
    448         ]
    449       | >lookup_opt_insert_miss
    450         [ <Hi
    451           (* USE[pass]: out_of_program_none → *)
    452           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
    453           [ >Hi @Hi2
    454           | @le_S @le_n
    455           ]
    456         | @bitvector_of_nat_abs
    457           [ @Hi2
    458           | @(transitive_lt … Hi2) <Hi @le_n
    459           | @sym_neq @lt_to_not_eq <Hi @le_n
    460           ]
    461         ]
    462       ]
    463     | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf
    464       normalize nodelta cases (decidable_eq_nat i (S (|prefix|)))
    465       [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H)
    466       | #Hi >lookup_opt_insert_miss
    467         [ #Hl
    468           (* USE[pass]: out_of_program_none ← *)
    469           elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
    470           [ #Hi3 @Hi3
    471           | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
    472           ]
    473         | @bitvector_of_nat_abs
    474           [ @Hi2
    475           | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length
    476             <plus_n_Sm @le_S_S @le_plus_n_r
    477           | @Hi
    478           ]
    479         ]
    480       ]
    481     ]
    482   | *)
     433  @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
     434| @conj [ @conj [ @conj [ @conj
    483435  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    484436    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
     
    594546    ]
    595547  ]
    596 | @conj [ @conj [ @conj [ @conj (*[ @conj
    597   [ #i cases i
    598     [ #Hi2 @conj
    599       [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
    600       | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl)
    601       ]
    602     | -i #i #Hi2 @conj
    603       [ #Hi >lookup_opt_insert_miss
    604         [ / by refl/
    605         | @bitvector_of_nat_abs
    606           [ @Hi2
    607           | / by /
    608           | @sym_neq @lt_to_not_eq / by /
    609           ]
    610         ]
    611       | #_ @le_S_S @le_O_n
    612       ]
    613     ] *)
     548| @conj [ @conj [ @conj [ @conj
    614549  [ #i cases i
    615550    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
Note: See TracChangeset for help on using the changeset viewer.