- Timestamp:
- Jun 9, 2011, 1:27:57 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r908 r909 1449 1449 | Some p ⇒ 1450 1450 let cm ≝ load_code_memory (\fst p) in 1451 let pc ≝ sigma 'pap (program_counter ? ps) in1451 let pc ≝ sigma pap (program_counter ? ps) in 1452 1452 Some … 1453 1453 (mk_PreStatus (BitVectorTrie Byte 16) … … 1463 1463 (clock … ps)) ]. 1464 1464 1465 (* 1465 1466 definition write_at_stack_pointer': 1466 1467 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝ … … 1521 1522 cases not_implemented 1522 1523 qed. 1523 1524 *) 1524 1525 (* 1525 1526 lemma execute_code_memory_unchanged: … … 1561 1562 | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w 1562 1563 ]. 1563 #ps #ps' #H whd in ⊢ (mat 1564 ch % with [ _ ⇒ ? | _ ⇒ ? ]) 1564 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 1565 1565 generalize in match (refl … (assembly (code_memory … ps))) 1566 1566 cases (assembly ?) in ⊢ (???% → %) 1567 1567 [ #K whd whd in ⊢ (??%?) <H >K % 1568 1568 | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ] 1569 qed.*) 1570 1571 let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝ 1572 match encoding with 1573 [ nil ⇒ True 1574 | cons hd tl ⇒ 1575 let 〈new_pc, byte〉 ≝ next code_memory pc in 1576 hd = byte ∧ encoding_check' code_memory new_pc tl 1577 ]. 1578 1569 qed. 1570 1579 1571 lemma main_thm: 1580 1572 ∀ticks_of.
Note: See TracChangeset
for help on using the changeset viewer.