Changeset 985


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (8 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r832 r985  
    1 include "common/AST.ma".
     1include "ASM/BitVector.ma".
     2
     3definition Identifier ≝ Word.
    24
    35inductive addressing_mode: Type[0] ≝
  • src/ASM/Assembly.ma

    r982 r985  
    44include "ASM/Fetch.ma".
    55include "ASM/Status.ma".
    6 include "ASM/FoldStuff.ma".
    76
    87definition assembly_preinstruction ≝
     
    680679    ].
    681680 
    682 definition construct_datalabels ≝
    683   λpreamble.
    684     \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
    685     λt. λpreamble.
    686       let 〈datalabels, addr〉 ≝ t in
    687       let 〈name, size〉 ≝ preamble in
    688       let addr_16 ≝ bitvector_of_nat 16 addr in
    689         〈insert ? ? name addr_16 datalabels, addr + size〉)
    690           〈(Stub ? ?), 0〉 preamble).
    691 
    692681definition construct_costs ≝
    693682  λprogram.
     
    717706  ].
    718707
    719 definition build_maps ≝
    720   λinstr_list.
    721   let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ?
    722     (λt. λi.
    723        let 〈label, i〉 ≝ i in
     708(* This establishes the correspondence between pseudo program counters and
     709   program counters. It is at the heart of the proof. *)
     710(*CSC: code taken from build_maps *)
     711definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     712 λinstr_list.λl:list labelled_instruction.
     713  foldl ??
     714   (λt,i.
    724715       match t with
    725716       [ None ⇒ None ?
    726        | Some t ⇒
    727          let 〈labels, pc_ppc_costs〉 ≝ t in
    728          let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in
    729          let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in
    730          let labels ≝
    731            match label with
    732            [ None ⇒ labels
    733            | Some label ⇒
    734              let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    735                insert ? ? label program_counter_bv labels
    736            ]
    737          in
    738            match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with
     717       | Some ppc_pc_map ⇒
     718         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     719         let 〈program_counter, sigma_map〉 ≝ pc_map in
     720         let 〈label, i〉 ≝ i in
     721          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    739722           [ None ⇒ None ?
    740            | Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉〉
    741            ]
    742        ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in
    743   match result with
     723           | Some pc_ignore ⇒
     724              let 〈pc,ignore〉 ≝ pc_ignore in
     725              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
     726       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
     727
     728definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
     729 ≝ λprog.sigma00 prog (\snd prog).
     730
     731definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
     732 λprogram,instr_list.
     733  match sigma00 program instr_list with
     734   [ None ⇒ None …
     735   | Some result ⇒
     736      let 〈ppc,pc_sigma_map〉 ≝ result in
     737      let 〈pc,map〉 ≝ pc_sigma_map in
     738       Some … 〈ppc,pc〉 ].
     739
     740definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
     741 λinstr_list.
     742  match sigma0 instr_list with
    744743  [ None ⇒ None ?
    745744  | Some result ⇒
    746     let 〈labels, pc_ppc_costs〉 ≝ result in
    747     let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in
    748     let 〈ppc, costs〉 ≝ ppc_costs in
     745    let 〈ppc,pc_sigma_map〉 ≝ result in
     746    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    749747      if gtb pc (2^16) then
    750748        None ?
    751749      else
    752         Some ? 〈labels, costs〉
    753   ].
     750        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
     751
     752(* stuff about policy *)
     753
     754axiom policy_ok: ∀p. sigma_safe p ≠ None ….
     755
     756definition sigma: pseudo_assembly_program → Word → Word ≝
     757 λp.
     758  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
     759   [ None ⇒ λabs. ⊥
     760   | Some r ⇒ λ_.r] (policy_ok p).
     761 cases abs //
     762qed.
     763
     764example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     765 cases daemon.
     766qed.
     767
     768axiom construct_costs_sigma:
     769 ∀p,ppc,pc,pc',costs,costs',i.
     770  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
     771   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
     772    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
     773
     774axiom tech_pc_sigma00_append_Some:
     775 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
     776  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     777   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     778    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
     779
     780axiom tech_pc_sigma00_append_None:
     781 ∀program,prefix,i,ppc,pc,costs.
     782  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     783   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     784    → False.
     785
     786definition build_maps ≝
     787  λpseudo_program.
     788  let result ≝
     789   foldl_strong
     790    (option Identifier × pseudo_instruction)
     791    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
     792      let 〈labels,ppc_pc_costs〉 ≝ res in
     793      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
     794      let 〈pc',costs〉 ≝ pc_costs in
     795       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
     796       ppc' = length … pre ∧
     797       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
     798       ∀id. occurs_exactly_once id pre →
     799        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
     800    (\snd pseudo_program)
     801    (λprefix,i,tl,prf,t.
     802      let 〈labels, ppc_pc_costs〉 ≝ t in
     803      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     804      let 〈pc,costs〉 ≝ pc_costs in
     805       let 〈label, i'〉 ≝ i in
     806       let labels ≝
     807         match label with
     808         [ None ⇒ labels
     809         | Some label ⇒
     810           let program_counter_bv ≝ bitvector_of_nat ? pc in
     811             insert ? ? label program_counter_bv labels
     812         ]
     813       in
     814         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
     815         [ None ⇒
     816            let dummy ≝ 〈labels,ppc_pc_costs〉 in
     817             dummy
     818         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
     819         ]
     820    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
     821  in
     822   let 〈labels, ppc_pc_costs〉 ≝ result in
     823   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
     824   let 〈pc, costs〉 ≝ pc_costs in
     825    〈labels, costs〉.
     826 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     827 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     828   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
     829   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     830   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
     831   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
     832   | #id normalize nodelta; -labels1; cases label; normalize nodelta
     833     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
     834     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
     835       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
     836        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
     837          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
     838        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
     839          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
     840 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
     841   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
     842qed.
     843
     844(*
     845lemma build_maps_ok:
     846 ∀p:pseudo_assembly_program.
     847  let 〈labels,costs〉 ≝ build_maps' p in
     848   ∀pc.
     849    (nat_of_bitvector … pc) < length … (\snd p) →
     850     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
     851 #p cases p #preamble #instr_list
     852  elim instr_list
     853   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
     854   | #hd #tl #IH
     855    whd in ⊢ (match % with [ _ ⇒ ?])
     856   ]
     857qed.
     858*)
    754859
    755860definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    756861  λp.
    757862    let 〈preamble, instr_list〉 ≝ p in
    758       match build_maps p with
     863    let 〈labels,costs〉 ≝ build_maps p in
     864    let datalabels ≝ construct_datalabels preamble in
     865    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     866    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
     867    let result ≝ foldr ? ? (λx. λy.
     868        match y with
     869        [ None ⇒ None ?
     870        | Some lst ⇒
     871          let 〈pc, ppc_y〉 ≝ lst in
     872          let 〈ppc, y〉 ≝ ppc_y in
     873          let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
     874          match x with
     875          [ None ⇒ None ?
     876          | Some x ⇒
     877            let 〈pc_delta, program〉 ≝ x in
     878            let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
     879            let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     880              Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
     881          ]
     882        ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
     883    in
     884      match result with
    759885      [ None ⇒ None ?
    760       | Some labels_costs ⇒
    761         let datalabels ≝ construct_datalabels preamble in
    762         let 〈labels,costs〉 ≝ labels_costs in
    763         let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    764         let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    765         let result ≝ foldr ? ? (λx. λy.
    766             match y with
    767             [ None ⇒ None ?
    768             | Some lst ⇒
    769               let 〈pc, ppc_y〉 ≝ lst in
    770               let 〈ppc, y〉 ≝ ppc_y in
    771               let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
    772               match x with
    773               [ None ⇒ None ?
    774               | Some x ⇒
    775                 let 〈pc_delta, program〉 ≝ x in
    776                 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    777                 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
    778                   Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
    779               ]
    780             ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
    781         in
    782           match result with
    783           [ None ⇒ None ?
    784           | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)
    785           ]
    786       ].
     886      | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)].
    787887
    788888definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  • src/ASM/AssemblyProof.ma

    r982 r985  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
    3 
    43
    54definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
     
    3433qed.
    3534
    36 lemma eq_b_eq:
    37   ∀b, c.
    38     eq_b b c = true → b = c.
    39   #b #c
    40   cases b
    41   cases c
    42   normalize //
    43 qed.
    44 
    45 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    46  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    47  #n #hd #tl #abs @⊥ //
    48 qed.
    49 
    50 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    51  ∃hd.∃tl.v ≃ VCons bool n hd tl.
    52  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    53  [ #abs @⊥ //
    54  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    55 qed.
    56 
    57 lemma eq_bv_eq:
    58   ∀n, v, q.
    59     eq_bv n v q = true → v = q.
    60   #n #v #q generalize in match v
    61   elim q
    62   [ #v #h @BitVector_O
    63   | #n #hd #tl #ih #v' #h
    64     cases (BitVector_Sn ? v')
    65     #hd' * #tl' #jmeq >jmeq in h;
    66     #new_h
    67     change in new_h with ((andb ? ?) = ?);
    68     cases(conjunction_true … new_h)
    69     #eq_heads #eq_tails
    70     whd in eq_heads:(??(??(%))?);
    71     cases(eq_b_eq … eq_heads)
    72     whd in eq_tails:(??(?????(%))?);
    73     change in eq_tails with (eq_bv ??? = ?);
    74     <(ih tl') //
    75   ]
    76 qed.
    77 
    7835lemma bool_eq_internal_eq:
    7936  ∀b, c.
     
    8744    | normalize //
    8845    ]
    89   ]
    90 qed.
    91 
    92 lemma eq_bv_refl:
    93   ∀n,v. eq_bv n v v = true.
    94   #n #v
    95   elim v
    96   [ //
    97   | #n #hd #tl #ih
    98     normalize
    99     cases hd
    100     [ normalize
    101       @ ih
    102     | normalize
    103       @ ih
    104     ]
    105   ]
    106 qed.
    107 
    108 lemma eq_eq_bv:
    109   ∀n, v, q.
    110     v = q → eq_bv n v q = true.
    111   #n #v
    112   elim v
    113   [ #q #h <h normalize %
    114   | #n #hd #tl #ih #q #h >h //
    11546  ]
    11647qed.
     
    623554qed.
    624555*)
    625 (*
    626 lemma test:
    627   let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in
    628       (let assembled ≝ assembly1 i in
    629       let code_memory ≝ load_code_memory assembled in
    630       let fetched ≝ fetch code_memory ? in
    631       let 〈instr_pc, ticks〉 ≝ fetched in
    632         eq_instruction (\fst instr_pc)) i = true.
    633  [2: @ zero
    634  | normalize
    635  ]*)
    636 
    637 lemma BitVectorTrie_O:
    638  ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
    639  #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    640   [ #w #_ %1 %[@w] %
    641   | #n #l #r #abs @⊥ //
    642   | #n #EQ %2 >EQ %]
    643 qed.
    644 
    645 lemma BitVectorTrie_Sn:
    646  ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    647  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    648   [ #m #abs @⊥ //
    649   | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    650   | #m #EQ %2 // ]
    651 qed.
    652 
    653 lemma lookup_prepare_trie_for_insertion_hit:
    654  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
    655   lookup … b (prepare_trie_for_insertion … b v) a = v.
    656  #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
    657 qed.
    658  
    659 lemma lookup_insert_hit:
    660  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
    661   lookup … b (insert … b v t) a = v.
    662  #A #a #v #n #b elim b -b -n //
    663  #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
    664   [ * #l * #r #JMEQ >JMEQ cases hd normalize //
    665   | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
    666 qed.
    667 
    668 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    669 
    670 lemma lookup_prepare_trie_for_insertion_miss:
    671  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
    672   (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
    673  #A #a #v #n #c elim c
    674   [ #b >(BitVector_O … b) normalize #abs @⊥ //
    675   | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    676     cases hd cases hd' normalize
    677     [2,3: #_ cases tl' //
    678     |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
    679 qed.
    680  
    681 lemma lookup_insert_miss:
    682  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    683   (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
    684  #A #a #v #n #c elim c -c -n
    685   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
    686   | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    687     #t cases(BitVectorTrie_Sn … t)
    688     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    689      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    690     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    691      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    692      [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    693 qed.
    694556
    695557definition load_code_memory_aux ≝
     
    702564  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    703565
    704 axiom half_add_SO:
     566example half_add_SO:
    705567 ∀pc.
    706568 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     569 cases daemon.
     570qed.
    707571
    708572(*
     
    724588qed.
    725589*)
    726 
    727 
    728 
    729590
    730591(*
     
    817678qed.
    818679
    819 axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
    820 
    821680axiom eq_instruction_to_eq: ∀i1,i2. eq_instruction i1 i2 = true → i1 = i2.
    822681
     
    840699    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    841700    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
    842     cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try % //
    843     [ @eqb_true_to_eq <(eq_instruction_to_eq … K1) // | >(eq_bv_to_eq … K3) @IH @H2 ]
    844 qed.
    845 
    846 (* This establishes the correspondence between pseudo program counters and
    847    program counters. It is at the heart of the proof. *)
    848 (*CSC: code taken from build_maps *)
    849 definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    850  λinstr_list.λl:list labelled_instruction.
    851   foldl ??
    852    (λt,i.
    853        match t with
    854        [ None ⇒ None ?
    855        | Some ppc_pc_map ⇒
    856          let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    857          let 〈program_counter, sigma_map〉 ≝ pc_map in
    858          let 〈label, i〉 ≝ i in
    859           match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    860            [ None ⇒ None ?
    861            | Some pc_ignore ⇒
    862               let 〈pc,ignore〉 ≝ pc_ignore in
    863               Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    864        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
    865 
    866 definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
    867  ≝ λprog.sigma00 prog (\snd prog).
    868 
    869 definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
    870  λprogram,instr_list.
    871   match sigma00 program instr_list with
    872    [ None ⇒ None …
    873    | Some result ⇒
    874       let 〈ppc,pc_sigma_map〉 ≝ result in
    875       let 〈pc,map〉 ≝ pc_sigma_map in
    876        Some … 〈ppc,pc〉 ].
    877 
    878 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
    879  λinstr_list.
    880   match sigma0 instr_list with
    881   [ None ⇒ None ?
    882   | Some result ⇒
    883     let 〈ppc,pc_sigma_map〉 ≝ result in
    884     let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    885       if gtb pc (2^16) then
    886         None ?
    887       else
    888         Some ? (λx.lookup ?? x sigma_map (zero …)) ].
    889 
    890 (* stuff about policy *)
    891 
    892 lemma policy_ok: ∀p. sigma_safe p ≠ None ….
    893  #instr_list whd in match (sigma_safe ?) whd in match (sigma0 ?)
    894  
    895 definition sigma: pseudo_assembly_program → Word → Word ≝
    896  λp.
    897   match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
    898    [ None ⇒ λabs. ⊥
    899    | Some r ⇒ λ_.r] (policy_ok p).
    900  cases abs //
    901 qed.
    902 
    903 lemma length_append:
    904  ∀A.∀l1,l2:list A.
    905   |l1 @ l2| = |l1| + |l2|.
    906  #A #l1 elim l1
    907   [ //
    908   | #hd #tl #IH #l2 normalize <IH //]
    909 qed.
    910 
    911 let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
    912  match l with
    913   [ nil ⇒ true
    914   | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
    915 
    916 lemma does_not_occur_None:
    917  ∀id,i,list_instr.
    918   does_not_occur id (list_instr@[〈None …,i〉]) =
    919   does_not_occur id list_instr.
    920  #id #i #list_instr elim list_instr
    921   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
    922 qed.
    923 
    924 lemma does_not_occur_Some:
    925  ∀id,id',i,list_instr.
    926   eq_bv ? id' id = false →
    927    does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    928     does_not_occur id list_instr.
    929  #id #id' #i #list_instr elim list_instr
    930   [ #H normalize in H ⊢ %; >H %
    931   | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
    932 qed.
    933 
    934 lemma does_not_occur_absurd:
    935  ∀id,i,list_instr.
    936   does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
    937  #id #i #list_instr elim list_instr
    938   [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
    939     >eq_bv_refl %
    940   | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
    941 qed.
    942 
    943 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    944  match l with
    945   [ nil ⇒ false
    946   | cons hd tl ⇒
    947      if instruction_matches_identifier id hd then
    948       does_not_occur id tl
    949      else
    950       occurs_exactly_once id tl ].
    951 
    952 lemma occurs_exactly_once_None:
    953  ∀id,i,list_instr.
    954   occurs_exactly_once id (list_instr@[〈None …,i〉]) =
    955   occurs_exactly_once id list_instr.
    956  #id #i #list_instr elim list_instr
    957   [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
    958 qed.
    959 
    960 lemma occurs_exactly_once_Some:
    961  ∀id,id',i,prefix.
    962   occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
    963  #id #id' #i #prefix elim prefix
    964   [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    965     change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
    966   | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
    967     cases he; normalize nodelta
    968      [ #H @ (IH H)
    969      | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    970        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
    971        [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
    972         /2/ #H >does_not_occur_Some //
    973        | #H @IH @H]]]
    974 qed.
    975 
    976 lemma index_of_internal_None: ∀i,id,instr_list,n.
    977  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    978   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    979    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    980  #i #id #instr_list elim instr_list
    981   [ #n #abs whd in abs; cases abs
    982   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
    983     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
    984     [ #H %
    985     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
    986       [ #_ % | #abs cases abs ]]]
    987 qed.
    988 
    989 lemma index_of_internal_Some_miss: ∀i,id,id'.
    990  eq_bv ? id' id = false →
    991  ∀instr_list,n.
    992  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    993   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    994    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
    995  #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
    996  change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
    997   [ #n #abs cases abs
    998   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    999     [ // | #K @IH //]]
    1000 qed.
    1001 
    1002 lemma index_of_internal_Some_hit: ∀i,id.
    1003  ∀instr_list,n.
    1004   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1005    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
    1006   = |instr_list| + n.
    1007  #i #id #instr_list elim instr_list
    1008   [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
    1009   | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
    1010     [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
    1011 qed.
    1012 
    1013 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1014  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1015   address_of_word_labels_code_mem instr_list id =
    1016   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1017  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1018  >(index_of_internal_None … H) %
    1019 qed.
    1020 
    1021 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
    1022  eq_bv ? id' id = false →
    1023   occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
    1024    address_of_word_labels_code_mem instr_list id =
    1025    address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    1026  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1027  >(index_of_internal_Some_miss … H) //
    1028 qed.
    1029 
    1030 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
    1031   occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
    1032    address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    1033    = bitvector_of_nat … (|instr_list|).
    1034  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
    1035  >(index_of_internal_Some_hit … H) //
    1036 qed.
    1037 
    1038 axiom tech_pc_sigma00_append_Some:
    1039  ∀program,prefix,costs,label,i,pc',code,ppc,pc.
    1040   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    1041    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    1042     tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
    1043 
    1044 axiom tech_pc_sigma00_append_None:
    1045  ∀program,prefix,i,ppc,pc,costs.
    1046   tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
    1047    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    1048     → False.
    1049 
    1050 lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    1051  *; //
    1052 qed.
    1053 
    1054 lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
    1055  #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
    1056 qed.
    1057 
    1058 example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    1059  cases daemon.
    1060 qed.
    1061 
    1062 axiom construct_costs_sigma:
    1063  ∀p,ppc,pc,pc',costs,costs',i.
    1064   bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
    1065    Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
    1066     bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
    1067 
    1068 definition build_maps' ≝
    1069   λpseudo_program.
    1070   let result ≝
    1071    foldl_strong
    1072     (option Identifier × pseudo_instruction)
    1073     (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
    1074       let 〈labels,ppc_pc_costs〉 ≝ res in
    1075       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    1076       let 〈pc',costs〉 ≝ pc_costs in
    1077        bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
    1078        ppc' = length … pre ∧
    1079        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
    1080        ∀id. occurs_exactly_once id pre →
    1081         lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
    1082     (\snd pseudo_program)
    1083     (λprefix,i,tl,prf,t.
    1084       let 〈labels, ppc_pc_costs〉 ≝ t in
    1085       let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
    1086       let 〈pc,costs〉 ≝ pc_costs in
    1087        let 〈label, i'〉 ≝ i in
    1088        let labels ≝
    1089          match label with
    1090          [ None ⇒ labels
    1091          | Some label ⇒
    1092            let program_counter_bv ≝ bitvector_of_nat ? pc in
    1093              insert ? ? label program_counter_bv labels
    1094          ]
    1095        in
    1096          match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    1097          [ None ⇒
    1098             let dummy ≝ 〈labels,ppc_pc_costs〉 in
    1099              dummy
    1100          | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
    1101          ]
    1102     ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
    1103   in
    1104    let 〈labels, ppc_pc_costs〉 ≝ result in
    1105    let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    1106    let 〈pc, costs〉 ≝ pc_costs in
    1107     〈labels, costs〉.
    1108  [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
    1109  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    1110    cases construct in p4 #PC #CODE #JMEQ % [% [%]]
    1111    [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
    1112    | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    1113    | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    1114    | #id normalize nodelta; -labels1; cases label; normalize nodelta
    1115      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
    1116      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    1117        generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
    1118         [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
    1119           <IH0 [@IHn1 | <(eq_bv_to_eq … EQ) in H #H @H]
    1120         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
    1121           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    1122  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    1123    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
    1124 qed.
    1125 
    1126 lemma build_maps_ok:
    1127  ∀p:pseudo_assembly_program.
    1128   let 〈labels,costs〉 ≝ build_maps' p in
    1129    ∀pc.
    1130     (nat_of_bitvector … pc) < length … (\snd p) →
    1131      lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
    1132  #p cases p #preamble #instr_list
    1133   elim instr_list
    1134    [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
    1135    | #hd #tl #IH
    1136     whd in ⊢ (match % with [ _ ⇒ ?])
    1137    ]
    1138 qed.
    1139 *)
     701    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
     702    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
     703qed.
    1140704
    1141705(*
     
    1211775lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
    1212776 #A * #l1 normalize //
    1213 qed.
    1214 
    1215 let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
    1216  (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
    1217  (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
    1218  B (app … prefix l) ≝
    1219   match l with
    1220   [ nil ⇒ ? (* b *)
    1221   | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
    1222   ].
    1223  [ applyS b
    1224  | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
    1225 qed.
    1226 
    1227 (*
    1228 let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
    1229  (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
    1230   match l with
    1231   [ nil ⇒ ? (* b *)
    1232   | cons hd tl ⇒
    1233      ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
    1234   ].
    1235  [ applyS b
    1236  | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
    1237777qed.
    1238778*)
    1239779
    1240 definition foldll:
    1241  ∀A:Type[0].∀B: Propify (list A) → Type[0].
    1242   (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
    1243    B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
    1244  ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
    1245 
    1246 axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
    1247 axiom pprefix_of_append:
    1248  ∀A:Type[0].∀l,l1,l2.
    1249   is_pprefix A l l1 → is_pprefix A l (l1@l2).
    1250 axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
    1251 axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.
    1252 
    1253 
    1254 axiom foldll':
    1255  ∀A:Type[0].∀l: list A.
    1256   ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
    1257   (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
    1258    B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
    1259  #A #l #B
    1260  generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
    1261  
    1262  
    1263   #H #acc
    1264  @foldll
    1265   [
    1266   |
    1267   ]
    1268  
    1269  ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).
    1270 
    1271 
    1272 (*
    1273 record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
    1274  { subset_wit:> A;
    1275    subset_proof: P subset_wit
    1276  }.
    1277 *)
    1278 
    1279 definition build_maps' ≝
    1280   λpseudo_program.
    1281   let 〈preamble,instr_list〉 ≝ pseudo_program in
    1282   let result ≝
    1283    foldll
    1284     (option Identifier × pseudo_instruction)
    1285     (λprefix.
    1286       Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1287        match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
    1288     (λprefix,t,i.
    1289       let 〈labels, pc_costs〉 ≝ t in
    1290       let 〈program_counter, costs〉 ≝ pc_costs in
    1291        let 〈label, i'〉 ≝ i in
    1292        let labels ≝
    1293          match label with
    1294          [ None ⇒ labels
    1295          | Some label ⇒
    1296            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    1297              insert ? ? label program_counter_bv labels
    1298          ]
    1299        in
    1300          match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
    1301          [ None ⇒
    1302             let dummy ≝ 〈labels,pc_costs〉 in
    1303               dummy
    1304          | Some construct ⇒ 〈labels, construct〉
    1305          ]
    1306     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
    1307   in
    1308    let 〈labels, pc_costs〉 ≝ result in
    1309    let 〈pc, costs〉 ≝ pc_costs in
    1310     〈labels, costs〉.
    1311  [
    1312  | @⊥
    1313  | normalize % //
    1314  ]
    1315 qed.
    1316 
    1317 definition build_maps' ≝
    1318   λpseudo_program.
    1319   let 〈preamble,instr_list〉 ≝ pseudo_program in
    1320   let result ≝
    1321    foldl
    1322     (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1323           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    1324            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
    1325     (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1326           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1327            is_prefix ? instr_list_prefix' instr_list →
    1328            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
    1329     (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
    1330           ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
    1331            tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
    1332      λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1333           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1334            is_prefix ? instr_list_prefix' instr_list →
    1335            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
    1336       let 〈labels, pc_costs〉 ≝ t in
    1337       let 〈program_counter, costs〉 ≝ pc_costs in
    1338        let 〈label, i'〉 ≝ i in
    1339        let labels ≝
    1340          match label with
    1341          [ None ⇒ labels
    1342          | Some label ⇒
    1343            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    1344              insert ? ? label program_counter_bv labels
    1345          ]
    1346        in
    1347          match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
    1348          [ None ⇒
    1349             let dummy ≝ 〈labels,pc_costs〉 in
    1350               dummy
    1351          | Some construct ⇒ 〈labels, construct〉
    1352          ]
    1353     ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
    1354   in
    1355    let 〈labels, pc_costs〉 ≝ result in
    1356    let 〈pc, costs〉 ≝ pc_costs in
    1357     〈labels, costs〉.
    1358  [4: @(list_elim_rev ?
    1359        (λinstr_list. list (
    1360         (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
    1361           let instr_list_prefix' ≝ instr_list_prefix @ [i] in
    1362            is_prefix ? instr_list_prefix' instr_list →
    1363            tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
    1364        ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
    1365       [ @[ ]
    1366       | #l' #a #limage %2
    1367         [ %[@a] #PREFIX #PREFIX_OK
    1368         | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
    1369              THE INDUCTION HYPOTHESIS INSTEAD *)
    1370           elim limage
    1371            [ %1
    1372            | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
    1373              @K1 @(prefix_of_append ???? K3)
    1374            ] 
    1375         ]
    1376        
    1377        
    1378      
    1379  
    1380   cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
    1381      % [@ (LIST_PREFIX @ [i])] %
    1382       [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
    1383       | (* DOABLE IN PRINCIPLE *)
    1384       ]
    1385  | (* assert false case *)
    1386  |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
    1387  |   
    1388 *)
    1389 
    1390780axiom assembly_ok:
    1391  ∀program,assembled,costs,labels.
    1392   Some … 〈labels,costs〉 = build_maps program →
     781 ∀program,assembled.
     782  let 〈labels,costs〉 ≝ build_maps program in
    1393783  Some … 〈assembled,costs〉 = assembly program →
    1394784  let code_memory ≝ load_code_memory assembled in
     
    1421811      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
    1422812
     813axiom pair_elim':
     814  ∀A,B,C: Type[0].
     815  ∀T: A → B → C.
     816  ∀p.
     817  ∀P: A×B → C → Prop.
     818    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
     819      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
     820
     821axiom pair_elim'':
     822  ∀A,B,C,C': Type[0].
     823  ∀T: A → B → C.
     824  ∀T': A → B → C'.
     825  ∀p.
     826  ∀P: A×B → C → C' → Prop.
     827    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
     828      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
     829
     830axiom split_elim':
     831  ∀A: Type[0].
     832  ∀B: Type[1].
     833  ∀l, m, v.
     834  ∀T: Vector A l → Vector A m → B.
     835  ∀P: B → Prop.
     836    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
     837      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
     838
     839axiom split_elim'':
     840  ∀A: Type[0].
     841  ∀B,B': Type[1].
     842  ∀l, m, v.
     843  ∀T: Vector A l → Vector A m → B.
     844  ∀T': Vector A l → Vector A m → B'.
     845  ∀P: B → B' → Prop.
     846    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
     847      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
     848        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     849
    1423850lemma fetch_assembly_pseudo2:
    1424  ∀program,assembled,costs,labels.
    1425   Some … 〈labels,costs〉 = build_maps program →
     851 ∀program,assembled.
     852  let 〈labels,costs〉 ≝ build_maps program in
    1426853  Some … 〈assembled,costs〉 = assembly program →
    1427854   ∀ppc.
     
    1436863      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
    1437864       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    1438  #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
     865 #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
    1439866 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
    1440867 letin code_memory ≝ (load_code_memory assembled)
     
    1443870 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
    1444871 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1445  whd in ⊢ (% → %)
    1446  generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
     872 whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
    1447873 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    1448874 generalize in match (fetch_assembly_pseudo program ppc
     
    22621688qed.
    22631689
    2264 axiom pair_elim':
    2265   ∀A,B,C: Type[0].
    2266   ∀T: A → B → C.
    2267   ∀p.
    2268   ∀P: A×B → C → Prop.
    2269     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
    2270       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
    2271 
    2272 axiom pair_elim'':
    2273   ∀A,B,C,C': Type[0].
    2274   ∀T: A → B → C.
    2275   ∀T': A → B → C'.
    2276   ∀p.
    2277   ∀P: A×B → C → C' → Prop.
    2278     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
    2279       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    2280 
    2281 axiom split_elim':
    2282   ∀A: Type[0].
    2283   ∀B: Type[1].
    2284   ∀l, m, v.
    2285   ∀T: Vector A l → Vector A m → B.
    2286   ∀P: B → Prop.
    2287     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
    2288       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
    2289 
    2290 axiom split_elim'':
    2291   ∀A: Type[0].
    2292   ∀B,B': Type[1].
    2293   ∀l, m, v.
    2294   ∀T: Vector A l → Vector A m → B.
    2295   ∀T': Vector A l → Vector A m → B'.
    2296   ∀P: B → B' → Prop.
    2297     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
    2298       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
    2299         (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
    2300 
    23011690axiom split_append:
    23021691  ∀A: Type[0].
     
    23171706    ((get_index_v A ? v 0 prf) ::: rest) = v.
    23181707
    2319 axiom sub_minus_one_seven_eight:
     1708example sub_minus_one_seven_eight:
    23201709  ∀v: BitVector 7.
    23211710  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    23221711  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
     1712 cases daemon.
     1713qed.
    23231714
    23241715lemma pair_destruct_1:
     
    24161807 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    24171808 cases (build_maps (code_memory … ps))
    2418   [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
    2419     #abs @⊥ normalize in abs; destruct (abs) ]
    2420  * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
     1809 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?)
    24211810 generalize in match (refl … (code_memory … ps)) cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    24221811 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    24231812  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
    24241813 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
    2425  #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
     1814 #H generalize in match (H ? (refl …)) -H; #H;
    24261815 #MAP
    24271816 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
     
    24621851    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
    24631852    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    2464     #H2 >(eq_bv_to_eq … H2) >EQ %
     1853    #H2 >(eq_bv_eq … H2) >EQ %
    24651854(*  |6: (* Mov *) #arg1 #arg2
    24661855       #H1 #H2 #EQ %[@1]
     
    24761865       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    24771866       #result #flags
    2478        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
     1867       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) % *)
    24791868  |5: (* Call *) #label #MAP
    24801869      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
     
    24901879           whd in ⊢ (???% → ??%?);
    24911880           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
    2492            >(eq_bv_to_eq … H2c)
     1881           >(eq_bv_eq … H2c)
    24931882           change with
    24941883            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
     
    24991888           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
    25001889           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
    2501            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1890           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    25021891           @split_eq_status;
    25031892            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
     
    25561945              >clock_write_at_stack_pointer whd in ⊢ (???%)
    25571946              >clock_write_at_stack_pointer %]
    2558        | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     1947       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    25591948         @pair_elim' #fst_5_addr #rest_addr #EQ1
    25601949         @pair_elim' #fst_5_pc #rest_pc #EQ2
     
    25651954         @pair_elim' * #instr #newppc' #ticks #EQn
    25661955          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
    2567           generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1956          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    25681957          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
    25691958          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
     
    25731962          >get_8051_sfr_set_8051_sfr
    25741963         
    2575           whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     1964          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    25761965           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    25771966           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     
    25911980              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
    25921981            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    2593               @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)
     1982              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
    25941983  |4: (* Jmp *) #label #MAP
    25951984      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
     
    26021991           >H2b >(eq_instruction_to_eq … H2a)
    26031992           generalize in match EQ; -EQ;
    2604            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     1993           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    26051994           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    26061995       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     
    26222011           generalize in match EQ; -EQ;
    26232012           whd in ⊢ (???% → ?);
    2624            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
     2013           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
    26252014           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ??) ? in ?) = ?)
    26262015           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 newppc) (sign_extension lower)))
     
    26462035           generalize in match EQ; -EQ;
    26472036           whd in ⊢ (???% → ?);
    2648            #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) whd in ⊢ (??%?)
     2037           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
    26492038           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
    26502039           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
     
    26832072             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
    26842073             false (DIRECT ARG2))
    2685            ? in ?) = ?)
     2074           ? in ?) = ?) //
    26862075       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
    26872076        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
    26882077       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    26892078       #result #flags
    2690        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) %
    2691     | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
     2079       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
     2080    (*| (* INC *) #arg1 #H1 #H2 #EQ %[@1]
    26922081       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    26932082       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    27002089       | cases (half_add ???) #carry #bl normalize nodelta;
    27012090         cases (full_add ????) #carry' #bu normalize nodelta ]
    2702         #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) -newppc';
     2091        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
    27032092        [5: %
    27042093        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
     
    27212110            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
    27222111            |
    2723             ]
     2112            ] *)
  • src/ASM/BitVector.ma

    r961 r985  
    88include "arithmetics/nat.ma".
    99
    10 include "ASM/Util.ma".
     10include "ASM/FoldStuff.ma".
    1111include "ASM/Vector.ma".
    1212include "ASM/String.ma".
     
    2525
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     27(* Inversion                                                                  *)
     28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     29
     30lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     32 #n #hd #tl #abs @⊥ //
     33qed.
     34
     35lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     36 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     38 [ #abs @⊥ //
     39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     40qed.
     41
     42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2743(* Lookup.                                                                    *)
    2844(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    98114      notb c.
    99115
     116lemma eq_b_eq:
     117  ∀b, c.
     118    eq_b b c = true → b = c.
     119  #b #c
     120  cases b
     121  cases c
     122  normalize //
     123qed.
     124
    100125definition eq_bv ≝
    101126  λn: nat.
     
    118143#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
    119144qed.
    120    
     145
     146lemma eq_bv_refl:
     147  ∀n,v. eq_bv n v v = true.
     148  #n #v
     149  elim v
     150  [ //
     151  | #n #hd #tl #ih
     152    normalize
     153    cases hd
     154    [ normalize
     155      @ ih
     156    | normalize
     157      @ ih
     158    ]
     159  ]
     160qed.
     161
     162lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
     163 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
     164qed.
     165
     166lemma eq_eq_bv:
     167  ∀n, v, q.
     168    v = q → eq_bv n v q = true.
     169  #n #v
     170  elim v
     171  [ #q #h <h normalize %
     172  | #n #hd #tl #ih #q #h >h //
     173  ]
     174qed.
     175
     176lemma eq_bv_eq:
     177  ∀n, v, q.
     178    eq_bv n v q = true → v = q.
     179  #n #v #q generalize in match v
     180  elim q
     181  [ #v #h @BitVector_O
     182  | #n #hd #tl #ih #v' #h
     183    cases (BitVector_Sn ? v')
     184    #hd' * #tl' #jmeq >jmeq in h;
     185    #new_h
     186    change in new_h with ((andb ? ?) = ?);
     187    cases(conjunction_true … new_h)
     188    #eq_heads #eq_tails
     189    whd in eq_heads:(??(??(%))?);
     190    cases(eq_b_eq … eq_heads)
     191    whd in eq_tails:(??(?????(%))?);
     192    change in eq_tails with (eq_bv ??? = ?);
     193    <(ih tl') //
     194  ]
     195qed.
     196
    121197axiom bitvector_of_string:
    122198  ∀n: nat.
  • src/ASM/BitVectorTrie.ma

    r782 r985  
    128128  ]
    129129qed.
     130
     131lemma BitVectorTrie_O:
     132 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     133 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     134  [ #w #_ %1 %[@w] %
     135  | #n #l #r #abs @⊥ //
     136  | #n #EQ %2 >EQ %]
     137qed.
     138
     139lemma BitVectorTrie_Sn:
     140 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     141 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     142  [ #m #abs @⊥ //
     143  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     144  | #m #EQ %2 // ]
     145qed.
     146
     147lemma lookup_prepare_trie_for_insertion_hit:
     148 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     149  lookup … b (prepare_trie_for_insertion … b v) a = v.
     150 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     151qed.
     152 
     153lemma lookup_insert_hit:
     154 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     155  lookup … b (insert … b v t) a = v.
     156 #A #a #v #n #b elim b -b -n //
     157 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     158  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     159  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     160qed.
     161
     162lemma lookup_prepare_trie_for_insertion_miss:
     163 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
     164  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
     165 #A #a #v #n #c elim c
     166  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     167  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     168    cases hd cases hd' normalize
     169    [2,3: #_ cases tl' //
     170    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
     171qed.
     172 
     173lemma lookup_insert_miss:
     174 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     175  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     176 #A #a #v #n #c elim c -c -n
     177  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     178  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     179    #t cases(BitVectorTrie_Sn … t)
     180    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     181     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     182    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     183     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     184     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
     185qed.
  • src/ASM/Interpret.ma

    r936 r985  
    11include "ASM/Status.ma".
    22include "ASM/Fetch.ma".
    3 include "ASM/Assembly.ma".
    43
    54definition sign_extension: Byte → Word ≝
     
    1211qed.
    1312   
    14 lemma inclusive_disjunction_true:
    15   ∀b, c: bool.
    16     (orb b c) = true → b = true ∨ c = true.
    17   # b
    18   # c
    19   elim b
    20   [ normalize
    21     # H
    22     @ or_introl
    23     %
    24   | normalize
    25     /2/
    26   ]
    27 qed.
    28 
    29 lemma conjunction_true:
    30   ∀b, c: bool.
    31     andb b c = true → b = true ∧ c = true.
    32   # b
    33   # c
    34   elim b
    35   normalize
    36   [ /2/
    37   | # K
    38     destruct
    39   ]
    40 qed.
    41 
    42 lemma eq_true_false: false=true → False.
    43  # K
    44  destruct
    45 qed.
    46 
    4713lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
    4814 # a
     
    5420 # K
    5521 cases (eq_true_false K)
    56 qed.
    57 
    58 lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
    59  # b
    60  cases b
    61  %
    6222qed.
    6323
     
    691651     execute_1_0 s instr_pc_ticks.
    692652
    693 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
    694   match l with
    695   [ nil ⇒ ?
    696   | cons hd tl ⇒
    697     if pred hd then
    698       acc
    699     else
    700       index_of_internal A pred tl (S acc)
    701   ].
    702   cases not_implemented.
    703 qed.
    704 
    705 definition index_of ≝
    706   λA.
    707   λeq.
    708   λl.
    709     index_of_internal A eq l 0.
    710 
    711 definition instruction_matches_identifier ≝
    712   λy: Identifier.
    713   λx: labelled_instruction.
    714     match \fst x with
    715     [ None ⇒ false
    716     | Some x ⇒ eq_bv ? x y
    717     ].
    718 
    719 definition address_of_word_labels_code_mem ≝
    720   λcode_mem.
    721   λid: Identifier.
    722     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
    723 
    724 definition address_of_word_labels ≝
    725   λps: PseudoStatus.
    726   λid: Identifier.
    727     address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
    728 
    729653definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
    730654  λticks_of.
  • src/ASM/Status.ma

    r949 r985  
    10851085    cases not_implemented.
    10861086qed.
     1087
     1088definition instruction_matches_identifier ≝
     1089  λy: Identifier.
     1090  λx: labelled_instruction.
     1091    match \fst x with
     1092    [ None ⇒ false
     1093    | Some x ⇒ eq_bv ? x y
     1094    ].
     1095
     1096let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
     1097 match l with
     1098  [ nil ⇒ true
     1099  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
     1100
     1101lemma does_not_occur_None:
     1102 ∀id,i,list_instr.
     1103  does_not_occur id (list_instr@[〈None …,i〉]) =
     1104  does_not_occur id list_instr.
     1105 #id #i #list_instr elim list_instr
     1106  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
     1107qed.
     1108
     1109lemma does_not_occur_Some:
     1110 ∀id,id',i,list_instr.
     1111  eq_bv ? id' id = false →
     1112   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
     1113    does_not_occur id list_instr.
     1114 #id #id' #i #list_instr elim list_instr
     1115  [ #H normalize in H ⊢ %; >H %
     1116  | * #x #i' #tl #IH #H whd in ⊢ (??%%) >(IH H) %]
     1117qed.
     1118
     1119lemma does_not_occur_absurd:
     1120 ∀id,i,list_instr.
     1121  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
     1122 #id #i #list_instr elim list_instr
     1123  [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
     1124    >eq_bv_refl %
     1125  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
     1126qed.
     1127
     1128
     1129let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
     1130 match l with
     1131  [ nil ⇒ false
     1132  | cons hd tl ⇒
     1133     if instruction_matches_identifier id hd then
     1134      does_not_occur id tl
     1135     else
     1136      occurs_exactly_once id tl ].
     1137
     1138lemma occurs_exactly_once_None:
     1139 ∀id,i,list_instr.
     1140  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
     1141  occurs_exactly_once id list_instr.
     1142 #id #i #list_instr elim list_instr
     1143  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
     1144qed.
     1145
     1146lemma occurs_exactly_once_Some:
     1147 ∀id,id',i,prefix.
     1148  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_bv ? id' id ∨ occurs_exactly_once id prefix.
     1149 #id #id' #i #prefix elim prefix
     1150  [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1151    change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/
     1152  | *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?)
     1153    cases he; normalize nodelta
     1154     [ #H @ (IH H)
     1155     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
     1156       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
     1157       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
     1158        /2/ #H >does_not_occur_Some //
     1159       | #H @IH @H]]]
     1160qed.
     1161
     1162let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
     1163  match l with
     1164  [ nil ⇒ ?
     1165  | cons hd tl ⇒
     1166    if pred hd then
     1167      acc
     1168    else
     1169      index_of_internal A pred tl (S acc)
     1170  ].
     1171  cases not_implemented.
     1172qed.
     1173
     1174
     1175definition index_of ≝
     1176  λA.
     1177  λeq.
     1178  λl.
     1179    index_of_internal A eq l 0.
     1180
     1181lemma index_of_internal_None: ∀i,id,instr_list,n.
     1182 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1183  index_of_internal ? (instruction_matches_identifier id) instr_list n =
     1184   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
     1185 #i #id #instr_list elim instr_list
     1186  [ #n #abs whd in abs; cases abs
     1187  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
     1188    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
     1189    [ #H %
     1190    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
     1191      [ #_ % | #abs cases abs ]]]
     1192qed.
     1193
     1194lemma index_of_internal_Some_miss: ∀i,id,id'.
     1195 eq_bv ? id' id = false →
     1196 ∀instr_list,n.
     1197 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1198  index_of_internal ? (instruction_matches_identifier id) instr_list n =
     1199   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
     1200 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
     1201 change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
     1202  [ #n #abs cases abs
     1203  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1204    [ // | #K @IH //]]
     1205qed.
     1206
     1207lemma index_of_internal_Some_hit: ∀i,id.
     1208 ∀instr_list,n.
     1209  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1210   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
     1211  = |instr_list| + n.
     1212 #i #id #instr_list elim instr_list
     1213  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
     1214  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1215    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
     1216qed.
     1217
     1218definition address_of_word_labels_code_mem ≝
     1219  λcode_mem.
     1220  λid: Identifier.
     1221    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
     1222
     1223lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
     1224 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1225  address_of_word_labels_code_mem instr_list id =
     1226  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
     1227 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1228 >(index_of_internal_None … H) %
     1229qed.
     1230
     1231lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
     1232 eq_bv ? id' id = false →
     1233  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1234   address_of_word_labels_code_mem instr_list id =
     1235   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
     1236 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1237 >(index_of_internal_Some_miss … H) //
     1238qed.
     1239
     1240lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
     1241  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1242   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
     1243   = bitvector_of_nat … (|instr_list|).
     1244 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
     1245 >(index_of_internal_Some_hit … H) //
     1246qed.
     1247
     1248definition address_of_word_labels ≝
     1249  λps: PseudoStatus.
     1250  λid: Identifier.
     1251    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
     1252
     1253definition construct_datalabels ≝
     1254  λpreamble.
     1255    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
     1256    λt. λpreamble.
     1257      let 〈datalabels, addr〉 ≝ t in
     1258      let 〈name, size〉 ≝ preamble in
     1259      let addr_16 ≝ bitvector_of_nat 16 addr in
     1260        〈insert ? ? name addr_16 datalabels, addr + size〉)
     1261          〈(Stub ? ?), 0〉 preamble).
  • src/ASM/Util.ma

    r907 r985  
    361361 /3/
    362362qed.
     363
     364lemma inclusive_disjunction_true:
     365  ∀b, c: bool.
     366    (orb b c) = true → b = true ∨ c = true.
     367  # b
     368  # c
     369  elim b
     370  [ normalize
     371    # H
     372    @ or_introl
     373    %
     374  | normalize
     375    /2/
     376  ]
     377qed.
     378
     379lemma conjunction_true:
     380  ∀b, c: bool.
     381    andb b c = true → b = true ∧ c = true.
     382  # b
     383  # c
     384  elim b
     385  normalize
     386  [ /2/
     387  | # K
     388    destruct
     389  ]
     390qed.
     391
     392lemma eq_true_false: false=true → False.
     393 # K
     394 destruct
     395qed.
     396
     397lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
     398 # b
     399 cases b
     400 %
     401qed.
     402
     403definition bool_to_Prop ≝
     404 λb. match b with [ true ⇒ True | false ⇒ False ].
     405
     406coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     407
     408lemma eq_false_to_notb: ∀b. b = false → ¬ b.
     409 *; /2/
     410qed.
     411
     412lemma length_append:
     413 ∀A.∀l1,l2:list A.
     414  |l1 @ l2| = |l1| + |l2|.
     415 #A #l1 elim l1
     416  [ //
     417  | #hd #tl #IH #l2 normalize <IH //]
     418qed.
  • src/common/AST.ma

    r961 r985  
    599599definition bool_to_Prop ≝
    600600 λb. match b with [ true ⇒ True | false ⇒ False ].
     601
     602coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    601603
    602604(* dpm: should go to standard library *)
Note: See TracChangeset for help on using the changeset viewer.