Changeset 1905


Ignore:
Timestamp:
Apr 26, 2012, 5:15:06 PM (7 years ago)
Author:
boender
Message:
  • plugging gap in assembly proof
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1887 r1905  
    99(**************************************** START OF POLICY ABSTRACTION ********************)
    1010
    11 (* definition of & operations on jump length *)
     11(* definition of & operations on jump length
    1212inductive jump_length: Type[0] ≝
    1313  | short_jump: jump_length
    1414  | medium_jump: jump_length
    15   | long_jump: jump_length.
     15  | long_jump: jump_length. *)
    1616
    1717definition assembly_preinstruction ≝
     
    418418qed.
    419419
    420 definition expand_relative_jump_internal_safe:
    421  Word → jump_length → Word → ([[relative]] → preinstruction [[relative]]) →
    422  option (list instruction)
     420definition expand_relative_jump_internal:
     421 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
     422 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     423 list instruction
    423424 ≝
    424   λlookup_address,jmp_len.λpc,i.
    425   match jmp_len with
    426   [ short_jump ⇒
    427      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    428      let 〈upper, lower〉 ≝ split ? 8 8 result in
    429      if eq_bv ? upper (zero 8) then
    430       let address ≝ RELATIVE lower in
    431        Some ? [ RealInstruction (i address) ]
    432      else
    433        None ?
    434   | medium_jump ⇒ None …
    435   | long_jump ⇒
    436     Some ?
     425  λlookup_labels.λsigma.λlbl.λpc,i.
     426   let lookup_address ≝ sigma (lookup_labels lbl) in
     427   let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     428   let 〈upper, lower〉 ≝ split ? 8 8 result in
     429   if eq_bv ? upper (zero 8) then
     430     let address ≝ RELATIVE lower in
     431       [ RealInstruction (i address) ]
     432   else
    437433    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
    438434      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
    439435      LJMP (ADDR16 lookup_address)
    440     ]
    441   ].
     436    ].
    442437  @ I
    443438qed.
    444439
    445 definition rel_jump_length_ok ≝
     440(*definition rel_jump_length_ok ≝
    446441 λlookup_address:Word.
    447442 λpc:Word.
     
    456451coercion eject_rel_jump_length nocomposites:
    457452 ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝
    458  eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.
    459 
    460 definition expand_relative_jump_internal:
    461  ∀lookup_address:Word. ∀pc:Word. rel_jump_length_ok lookup_address pc →
    462   ([[relative]] → preinstruction [[relative]]) →
     453 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.*)
     454
     455(*definition expand_relative_jump_internal:
     456 ∀lookup_address:Word. ∀pc:Word. ([[relative]] → preinstruction [[relative]]) →
    463457 list instruction
    464 ≝ λlookup_address,pc,jump_len,i.
    465    match expand_relative_jump_internal_safe lookup_address jump_len pc i
     458≝ λlookup_address,pc,i.
     459   match expand_relative_jump_internal_safe lookup_address pc i
    466460   return λres. res ≠ None ? → ?
    467461   with
     
    469463   | Some res ⇒ λ_.res ] (pi2 … jump_len i).
    470464 cases abs /2/
    471 qed.
    472 
    473 definition expand_relative_jump_safe: ∀lookup_labels:Identifier → Word.Word → jump_length → preinstruction Identifier → option (list instruction) ≝
    474   λlookup_labels.
     465qed.*)
     466
     467definition expand_relative_jump:
     468  ∀lookup_labels.∀sigma.
     469  Word → (*jump_length →*)
     470  preinstruction Identifier → list instruction ≝
     471  λlookup_labels: Identifier → Word.
     472  λsigma:Word → Word.
    475473  λpc: Word.
    476   λjmp_len: jump_length.
     474  (*λjmp_len: jump_length.*)
    477475  λi: preinstruction Identifier.
    478476  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
    479477  match i with
    480   [ JC jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JC ?)
    481   | JNC jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNC ?)
    482   | JB baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JB ? baddr)
    483   | JZ jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JZ ?)
    484   | JNZ jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNZ ?)
    485   | JBC baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JBC ? baddr)
    486   | JNB baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNB ? baddr)
    487   | CJNE addr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (CJNE ? addr)
    488   | DJNZ addr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (DJNZ ? addr)
    489   | ADD arg1 arg2 ⇒ Some … [ ADD ? arg1 arg2 ]
    490   | ADDC arg1 arg2 ⇒ Some … [ ADDC ? arg1 arg2 ]
    491   | SUBB arg1 arg2 ⇒ Some … [ SUBB ? arg1 arg2 ]
    492   | INC arg ⇒ Some … [ INC ? arg ]
    493   | DEC arg ⇒ Some … [ DEC ? arg ]
    494   | MUL arg1 arg2 ⇒ Some … [ MUL ? arg1 arg2 ]
    495   | DIV arg1 arg2 ⇒  Some … [ DIV ? arg1 arg2 ]
    496   | DA arg ⇒ Some … [ DA ? arg ]
    497   | ANL arg ⇒ Some … [ ANL ? arg ]
    498   | ORL arg ⇒ Some … [ ORL ? arg ]
    499   | XRL arg ⇒ Some … [ XRL ? arg ]
    500   | CLR arg ⇒ Some … [ CLR ? arg ]
    501   | CPL arg ⇒ Some … [ CPL ? arg ]
    502   | RL arg ⇒ Some … [ RL ? arg ]
    503   | RR arg ⇒ Some … [ RR ? arg ]
    504   | RLC arg ⇒ Some … [ RLC ? arg ]
    505   | RRC arg ⇒ Some … [ RRC ? arg ]
    506   | SWAP arg ⇒ Some … [ SWAP ? arg ]
    507   | MOV arg ⇒ Some … [ MOV ? arg ]
    508   | MOVX arg ⇒ Some … [ MOVX ? arg ]
    509   | SETB arg ⇒ Some … [ SETB ? arg ]
    510   | PUSH arg ⇒ Some … [ PUSH ? arg ]
    511   | POP arg ⇒ Some … [ POP ? arg ]
    512   | XCH arg1 arg2 ⇒ Some … [ XCH ? arg1 arg2 ]
    513   | XCHD arg1 arg2 ⇒ Some … [ XCHD ? arg1 arg2 ]
    514   | RET ⇒ Some … [ RET ? ]
    515   | RETI ⇒ Some … [ RETI ? ]
    516   | NOP ⇒ Some … [ RealInstruction (NOP ?) ]
     478  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JC ?)
     479  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNC ?)
     480  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JB ? baddr)
     481  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JZ ?)
     482  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNZ ?)
     483  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JBC ? baddr)
     484  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (JNB ? baddr)
     485  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (CJNE ? addr)
     486  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels sigma jmp pc (DJNZ ? addr)
     487  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
     488  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
     489  | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
     490  | INC arg ⇒ [ INC ? arg ]
     491  | DEC arg ⇒ [ DEC ? arg ]
     492  | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
     493  | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
     494  | DA arg ⇒ [ DA ? arg ]
     495  | ANL arg ⇒ [ ANL ? arg ]
     496  | ORL arg ⇒ [ ORL ? arg ]
     497  | XRL arg ⇒ [ XRL ? arg ]
     498  | CLR arg ⇒ [ CLR ? arg ]
     499  | CPL arg ⇒ [ CPL ? arg ]
     500  | RL arg ⇒ [ RL ? arg ]
     501  | RR arg ⇒ [ RR ? arg ]
     502  | RLC arg ⇒ [ RLC ? arg ]
     503  | RRC arg ⇒ [ RRC ? arg ]
     504  | SWAP arg ⇒ [ SWAP ? arg ]
     505  | MOV arg ⇒ [ MOV ? arg ]
     506  | MOVX arg ⇒ [ MOVX ? arg ]
     507  | SETB arg ⇒ [ SETB ? arg ]
     508  | PUSH arg ⇒ [ PUSH ? arg ]
     509  | POP arg ⇒ [ POP ? arg ]
     510  | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
     511  | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
     512  | RET ⇒ [ RET ? ]
     513  | RETI ⇒ [ RETI ? ]
     514  | NOP ⇒ [ RealInstruction (NOP ?) ]
    517515  ].
    518516
    519 definition expand_pseudo_instruction_safe:
    520  ∀lookup_labels,pc. jump_length → ? → pseudo_instruction → option (list instruction) ≝
    521   λlookup_labels.
     517definition expand_pseudo_instruction:
     518 ∀lookup_labels.∀sigma.Word → ? → pseudo_instruction → list instruction ≝
     519  λlookup_labels:Identifier → Word.
     520  λsigma:Word → Word.
    522521  λpc.
    523   λjmp_len.
    524   λlookup_datalabels.
     522  λlookup_datalabels:Identifier → Word.
    525523  λi.
    526524  match i with
    527   [ Cost cost ⇒ Some ? [ ]
    528   | Comment comment ⇒ Some ? [ ]
     525  [ Cost cost ⇒ [ ]
     526  | Comment comment ⇒ [ ]
    529527  | Call call ⇒
    530     match jmp_len with
    531     [ short_jump ⇒ None ?
    532     | medium_jump ⇒
    533       let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
    534       let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
    535       if eq_bv ? ignore fst_5 then
    536         let address ≝ ADDR11 address in
    537           Some ? ([ ACALL address ])
    538       else
    539         None ?
    540     | long_jump ⇒
     528    let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
     529    let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
     530    if eq_bv ? ignore fst_5 then
     531      let address ≝ ADDR11 address in
     532        [ ACALL address ]
     533    else
    541534      let address ≝ ADDR16 (lookup_labels call) in
    542         Some ? [ LCALL address ]
    543     ]
     535        [ LCALL address ]
    544536  | Mov d trgt ⇒
    545537    let address ≝ DATA16 (lookup_datalabels trgt) in
    546       Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    547   | Instruction instr ⇒ expand_relative_jump_safe lookup_labels pc jmp_len instr
     538      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
     539  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma pc instr
    548540  | Jmp jmp ⇒
    549     match jmp_len with
    550     [ short_jump ⇒
    551       let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in
    552       let 〈upper, lower〉 ≝ split ? 8 8 result in
    553       if eq_bv ? upper (zero 8) then
    554         let address ≝ RELATIVE lower in
    555           Some ? [ SJMP address ]
    556       else
    557         None ?
    558     | medium_jump ⇒
     541    let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) false in
     542    let 〈upper, lower〉 ≝ split ? 8 8 result in
     543    if eq_bv ? upper (zero 8) then
     544      let address ≝ RELATIVE lower in
     545        [ SJMP address ]
     546    else
    559547      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
    560548      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    561549      if eq_bv ? fst_5_addr fst_5_pc then
    562550        let address ≝ ADDR11 rest_addr in
    563           Some ? ([ AJMP address ])
    564       else
    565         None ?
    566     | long_jump ⇒
     551          [ AJMP address ]
     552      else   
    567553        let address ≝ ADDR16 (lookup_labels jmp) in
    568         Some ? [ LJMP address ]
    569     ]
     554        [ LJMP address ]
    570555  ].
    571556  @ I
    572557qed.
    573558
     559(*
     560(*X?
    574561definition jump_length_ok ≝
    575562 λlookup_labels:Identifier → Word.
     
    578565  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
    579566  ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.
     567*)
    580568
    581569lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.
     
    598586 cases abs /2/
    599587qed.
    600 
     588*)
     589(*X?
    601590definition policy_type ≝
    602591 λlookup_labels:Identifier → Word.
    603592 ∀pc:Word. jump_length_ok lookup_labels pc.
    604 
    605 definition policy_type2 ≝
    606  ∀lookup_labels.policy_type lookup_labels.
     593*)
     594
     595(*definition policy_type2 ≝
     596 λprogram.
     597  Σpol:Word → jump_length.
     598   let lookup_labels ≝
     599    (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) in
     600   ∀pc:Word. let jump_len ≝ pol pc in
     601    ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.*)
    607602 
    608603definition assembly_1_pseudoinstruction ≝
    609604  λlookup_labels.
    610   λjump_expansion: policy_type lookup_labels.
     605  λsigma.
    611606  (*λppc: Word.*)
    612607  λpc: Word.
    613608  λlookup_datalabels.
    614609  λi.
    615   let expansion ≝ jump_expansion pc in
    616   let pseudos ≝ expand_pseudo_instruction lookup_labels pc expansion lookup_datalabels i in
     610  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma pc lookup_datalabels i in
    617611  let mapped ≝ map ? ? assembly1 pseudos in
    618612  let flattened ≝ flatten ? mapped in
     
    621615
    622616definition construct_costs ≝
     617  (*X?*)λlookup_labels.
     618  λsigma.
    623619  λprogram_counter: nat.
    624   λjump_expansion: policy_type (λx.bitvector_of_nat ? program_counter).
    625620  λpseudo_program_counter: nat.
    626621  λcosts: BitVectorTrie costlabel 16.
     
    635630    let lookup_datalabels ≝ λx.zero ? in
    636631    let pc_delta_assembled ≝
    637       assembly_1_pseudoinstruction (λx.pc_bv)
    638        jump_expansion (*ppc_bv*) pc_bv lookup_datalabels i in
     632      assembly_1_pseudoinstruction (*X?(λx.pc_bv)*) lookup_labels
     633       sigma (*ppc_bv*) pc_bv lookup_datalabels i in
    639634    let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
    640635     〈pc_delta + program_counter, costs〉
     
    671666qed.
    672667
     668(*
    673669(* This establishes the correspondence between pseudo program counters and
    674670   program counters. It is at the heart of the proof. *)
    675671(*CSC: code taken from build_maps *)
    676 definition sigma00: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
     672definition sigma00:
     673 ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
    677674 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
    678675  let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     
    686683   bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
    687684   bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
    688    (\fst
    689     (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi)))))
    690  ) ≝
    691  λjump_expansion: policy_type2.
     685   (\fst (assembly_1_pseudoinstruction lookup_labels(*X?(λx.pc_x)*) (jump_expansion (*?(λx.pc_x)*)) pc_x
     686     (λx.zero ?) pi)))))
     687 ) ≝
     688 (*?*)λlookup_labels.
     689 λjump_expansion(*X?: policy_type2*).
    692690 λl:list labelled_instruction.
    693691 λacc.
     
    704702       bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
    705703       bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
    706        (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi))))))
     704       (\fst (assembly_1_pseudoinstruction (*X?(λx.pc_x)*)lookup_labels (jump_expansion (*X?(λx.pc_x)*)) pc_x
     705        (λx.zero ?) pi))))))
    707706    )
    708707   l
     
    711710     let 〈program_counter, sigma_map〉 ≝ pc_map in
    712711     let 〈label, i〉 ≝ i in
    713       let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in
     712      let 〈pc,ignore〉 ≝ construct_costs lookup_labels program_counter (jump_expansion (*X?(λx.bitvector_of_nat ? program_counter)*)) ppc (Stub …) i in
    714713         〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉
    715714   ) acc.
     
    813812      None ?
    814813    else
    815       Some ? (λx. lookup … x sigma_map (zero …)).
     814      Some ? (λx. lookup … x sigma_map (zero …)). *)
    816815
    817816(* stuff about policy *)
    818817
    819 definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
    820 
    821 definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.
    822 
    823 lemma eject_policy: ∀p. policy p → policy_type2.
     818(*definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….*)
     819
     820(*definition policy ≝ λp. Σjump_expansion:policy_type2. policy_ok jump_expansion p.*)
     821
     822(*lemma eject_policy: ∀p. policy p → policy_type2.
    824823 #p #pol @(pi1 … pol)
    825824qed.
     
    833832   | Some r ⇒ λ_.r] (pi2 … policy).
    834833 cases abs /2 by /
     834qed.*)
     835
     836example half_add_SO:
     837 ∀pc.
     838 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     839 cases daemon.
    835840qed.
    836841
    837842(*CSC: Main axiom here, needs to be proved soon! *)
    838 lemma snd_assembly_1_pseudoinstruction_ok:
     843(*lemma snd_assembly_1_pseudoinstruction_ok:
    839844 ∀program:pseudo_assembly_program.∀pol: policy program.
    840845 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
    841846  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
    842847  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     848  (nat_of_bitvector 16 ppc) < |\snd program| →
    843849  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    844850   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    845851    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
    846852     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    847  #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl
    848  whd in match (sigma ???); whd in match (sigma program pol (\snd (half_add ???)));
    849  whd in match (sigma_safe program pol); whd in match (sigma0 program pol);
    850  lapply (refl ? (pi1 ?? (sigma00 pol (\snd program)
    851   «〈0, 〈0, (insert (BitVector 16) 16 (bitvector_of_nat 16 0) (bitvector_of_nat 16 0) (Stub (BitVector 16) 16))〉〉,?»)))
    852  [ @conj
    853    [ / by refl/
    854    | #H >lookup_insert_hit @conj
    855      [ @refl
    856      | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
    857      ]
    858    ]
    859  | (* here we go *) cases daemon
    860  ]
    861 qed.
     853 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl #Hppc
     854 lapply (refl … (sigma0 program pol)) whd in match (sigma0 ??) in ⊢ (??%? → ?);
     855 cases (sigma00 ???) #x #Hpmap #EQ
     856 whd in match (sigma ???);
     857 whd in match (sigma program pol (\snd (half_add ???)));
     858 whd in match sigma_safe; normalize nodelta
     859 (*Problem1: backtracking cases (sigma0 program pol)*)
     860 generalize in match (pi2 ???); whd in match policy_ok; normalize nodelta
     861 whd in match sigma_safe; normalize nodelta <EQ cases x in Hpmap EQ; -x #final_ppc #x
     862 cases x -x #final_pc #smap normalize nodelta #Hpmap #EQ #Heq #Hfetch cases (gtb final_pc (2^16)) in Heq;
     863 normalize nodelta
     864 [ #abs @⊥ @(absurd ?? abs) @refl
     865 | #_ lapply (proj1 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) #Hpmap1
     866   lapply ((proj2 ?? ((proj2 ?? Hpmap) (proj1 ?? Hpmap))) (nat_of_bitvector 16 ppc) Hppc) #Hpmap2 -Hpmap
     867   <(bitvector_of_nat_nat_of_bitvector 16 ppc) >half_add_SO
     868   
     869   >(Hpmap2 ? (refl …)) @eq_f @eq_f2 [%]
     870   >bitvector_of_nat_nat_of_bitvector
     871   >Hfetch lapply Hfetch lapply pi
     872
     873   
     874   whd in match assembly_1_pseudoinstruction; normalize nodelta
    862875 
    863 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     876qed.*)
     877
     878
     879(*example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    864880 cases daemon.
    865 qed.
     881qed.*)
    866882
    867883axiom fetch_pseudo_instruction_split:
     
    11171133
    11181134definition build_maps0:
    1119  ∀pseudo_program.∀pol:policy pseudo_program.
     1135 ∀pseudo_program:pseudo_assembly_program.∀sigma:Word → Word.
    11201136  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
    11211137   let 〈labels, costs〉 ≝ res in
    11221138    ∀id. occurs_exactly_once ?? id (\snd pseudo_program) →
    1123      lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
     1139     lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
    11241140  λpseudo_program.
    1125   λpol:policy pseudo_program.
     1141  λsigma.
    11261142    let result ≝
    11271143      foldl_strong
     
    11321148            let 〈pc',costs〉 ≝ pc_costs in
    11331149              And ( And (
    1134               And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
     1150              And (bitvector_of_nat ? pc' = sigma (bitvector_of_nat ? ppc')) (*∧*)
    11351151                (ppc' = length … pre)) (*∧ *)
    1136                 (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)) (*∧*)
     1152                (*(tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)*) True) (*∧*)
    11371153                (∀id. occurs_exactly_once ?? id pre →
    1138                   lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
     1154                  lookup_def … labels id (zero …) = sigma (address_of_word_labels_code_mem pre id)))
    11391155                (\snd pseudo_program)
    11401156        (λprefix,i,tl,prf,t.
     
    11511167            ]
    11521168          in
    1153             let construct ≝ construct_costs pc (pol (λx.bitvector_of_nat ? pc)) ppc costs i' in
     1169            let construct ≝ construct_costs (λid.lookup_def … labels id (zero ?)) sigma
     1170              pc ppc costs i' in
    11541171              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
    11551172    in
     
    11811198
    11821199definition build_maps:
    1183  ∀pseudo_program. policy pseudo_program →
     1200 ∀pseudo_program.∀sigma.
    11841201  (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)
    1185  ≝ λpseudo_program,pol. build_maps0 pseudo_program pol.
     1202 ≝ λpseudo_program,sigma. build_maps0 pseudo_program sigma.
    11861203
    11871204theorem build_maps_ok:
    1188  ∀pseudo_program.∀pol:policy pseudo_program.
    1189    let 〈labels, costs〉 ≝ build_maps pseudo_program pol in
     1205 ∀pseudo_program.∀sigma:Word → Word.
     1206   let 〈labels, costs〉 ≝ build_maps pseudo_program sigma in
    11901207    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    1191      lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id).
    1192  #pseudo_program #pol @(pi2 … (build_maps0 … pol))
     1208     lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id).
     1209 #pseudo_program #sigma @(pi2 … (build_maps0 … sigma))
    11931210qed.
    11941211
    11951212definition assembly:
    1196  ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
     1213 ∀p:pseudo_assembly_program.∀sigma:Word → Word.list Byte × (BitVectorTrie costlabel 16) ≝
    11971214  λp.let 〈preamble, instr_list〉 ≝ p in
    1198    λpol.
    1199     let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
     1215   λsigma.
     1216    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 sigma in
    12001217    let datalabels ≝ construct_datalabels preamble in
    12011218    let lookup_labels ≝ λx. lookup_def … labels x (zero ?) in
     
    12101227          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
    12111228          let 〈len,assembledi〉 ≝
    1212            assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc' lookup_datalabels pi in
     1229           assembly_1_pseudoinstruction lookup_labels sigma ppc' lookup_datalabels pi in
    12131230           True)
    12141231      instr_list
     
    12161233        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
    12171234        let 〈ppc, code〉 ≝ ppc_code in
    1218         let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels (\snd hd) in
     1235        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels (\snd hd) in
    12191236        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    12201237        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
Note: See TracChangeset for help on using the changeset viewer.