Changeset 1667 for src

Timestamp:

Jan 29, 2012, 10:25:57 PM (9 years ago)

Author:

sacerdot

Message:

Main lemma for the main_thm of AssemblyProof? re-declared as an axiom in
Assembly.ma. However, we need to understand again the role of lookup_labels.

Location:

src/ASM

Files:

• Assembly.ma (modified) (2 diffs)
• AssemblyProof.ma (modified) (2 diffs)

src/ASM/Assembly.ma

@@ -619 +619 @@
   let pc_len ≝ length ? flattened in
    〈pc_len, flattened〉.
- 
+
 definition construct_costs ≝
   λprogram_counter: nat.
@@ -701 +701 @@
  cases abs /2/
 qed.
+
+(*CSC: Main axiom here, needs to be proved soon! *)
+axiom snd_assembly_1_pseudoinstruction_ok:
+ ∀program:pseudo_assembly_program.∀pol: policy program.
+ ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
+  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
+  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
+  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
+   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
+    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
+     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
 
 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.

src/ASM/AssemblyProof.ma

@@ -2031 +2031 @@
 qed.
 
+(*usare snd_assembly_1_pseudoinstruction_ok:
+ ∀program:pseudo_assembly_program.∀pol: policy program.
+ ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
+  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
+  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
+  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
+   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
+    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
+     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
+*)
+
+lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
+ /2/
+qed.
+
 theorem main_thm:
  ∀M,M',cm,ps,pol,lookup_labels.
@@ -2037 +2052 @@
       execute n … (status_of_pseudo_status M … ps pol)
     = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol.
- #M #M' * #preamble #instr_list #ps
- letin ppc ≝ (program_counter ?? ps) 
- #pol #lookup_labels
+ #M #M' * #preamble #instr_list #ps #pol #lookup_labels
  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
- change with (next_internal_pseudo_address_map0 ? (\fst (fetch_pseudo_instruction ? ppc)) ??? = ? → ?)
+ @(pose … (program_counter ?? ps)) #ppc #EQppc
  generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
- letin assembled ≝ (\fst (assembly ? pol))
- letin lookup_labels ≝ (λx.(address_of_word_labels_code_mem instr_list x))
- letin lookup_datalabels ≝ (λx. lookup_def … (construct_datalabels preamble) x (zero 16))
+ @(pose … (\fst (assembly ? pol))) #assembled #EQassembled
+ @(pose … (λx.(address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
+ @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
  whd in match execute_1_pseudo_instruction; normalize nodelta
- @pair_elim #pi #newppc change with (fetch_pseudo_instruction ? ppc = ? → ?) #EQ2
- whd in match ticks_of;
- normalize nodelta change with ppc in match ppc; change with assembled in match assembled;
- change with lookup_labels in match lookup_labels; change with lookup_datalabels in match lookup_datalabels;
- #H1 >EQ2
+ @pair_elim #pi #newppc #H1
+ whd in match ticks_of; normalize nodelta <EQppc #H2 >H1 normalize nodelta;
+ lapply (snd_fetch_pseudo_instruction instr_list ppc) >H1 #EQnewppc >EQnewppc
+ lapply (snd_assembly_1_pseudoinstruction_ok … EQlookup_labels EQlookup_datalabels)
  inversion pi
   [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?);