Changeset 1870


Ignore:
Timestamp:
Apr 3, 2012, 2:52:10 PM (8 years ago)
Author:
boender
Message:
  • changed sigma00 in Assembly to use foldl_strong + proved invariants
  • commented out sigma00_append
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1646 r1870  
    161161definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
    162162  λn,v. nat_of_bitvector_aux n O v.
    163    
     163
     164lemma bitvector_of_nat_ok:
     165  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
     166 #n elim n -n
     167 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
     168 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
     169 ]
     170qed.
     171
     172lemma bitvector_of_nat_abs:
     173  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
     174 #n #x #y #Hx #Hy #Heq @notb_elim
     175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
     176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
     177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
     178 | #H / by I/
     179 ]
     180qed.
     181
    164182definition two_complement_negation ≝
    165183  λn: nat.
  • src/ASM/Assembly.ma

    r1668 r1870  
    635635    let lookup_datalabels ≝ λx.zero ? in
    636636    let pc_delta_assembled ≝
    637       assembly_1_pseudoinstruction (λx.bitvector_of_nat ? program_counter)
     637      assembly_1_pseudoinstruction (λx.pc_bv)
    638638       jump_expansion (*ppc_bv*) pc_bv lookup_datalabels i in
    639639    let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
    640640     〈pc_delta + program_counter, costs〉
    641641  ].
     642 
     643axiom nat_of_bitvector_bitvector_of_nat:
     644  ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n.
     645 
     646axiom bitvector_of_nat_nat_of_bitvector:
     647  ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v.
     648
     649lemma nth_cons:
     650  ∀n,A,h,t,y.
     651  nth (S n) A (h::t) y = nth n A t y.
     652 #n #A #h #t #y /2 by refl/
     653qed.
     654 
     655lemma fetch_pseudo_instruction_prefix:
     656  ∀prefix.∀x.∀ppc.ppc < (|prefix|) →
     657  fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =
     658  fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).
     659 #prefix #x #ppc elim prefix
     660 [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n
     661 | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);
     662   whd in match (fetch_pseudo_instruction ((h::t)@x) ?);
     663   >nth_append_first
     664   [ //
     665   | >nat_of_bitvector_bitvector_of_nat
     666     [ @Hppc
     667     | cases daemon (* XXX invariant *)
     668     ]
     669   ]
     670 ]
     671qed.
    642672
    643673(* This establishes the correspondence between pseudo program counters and
    644674   program counters. It is at the heart of the proof. *)
    645675(*CSC: code taken from build_maps *)
    646 (*JPB: Here it gets strange because we need a program counter for the jump
    647  *expansion, but we can't give it to the type because we don't have it yet. Argh.
    648  *add a forall type?*)
    649 definition sigma00: policy_type2 → list ? → ? → (nat × (nat × (BitVectorTrie Word 16))) ≝
     676definition sigma00: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
     677 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
     678  let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     679  let 〈program_counter, sigma_map〉 ≝ pc_map in
     680  ppc = |l| ∧
     681  (ppc = |l| →
     682   (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
     683   (∀x.x < |l| →
     684    ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
     685   let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
     686   bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
     687   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 ) ≝
    650691 λjump_expansion: policy_type2.
    651692 λl:list labelled_instruction.
    652693 λacc.
    653   foldl …
    654    (λppc_pc_map,i.
     694  foldl_strong ?
     695   (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
     696     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     697     let 〈program_counter, sigma_map〉 ≝ pc_map in
     698     (ppc = |prefix|) ∧
     699     (ppc = |prefix| →
     700      (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
     701      (∀x.x < |prefix| →
     702       ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
     703       let pc_x ≝  bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
     704       bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) =
     705       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))))))
     707    )
     708   l
     709   (λhd.λi.λtl.λp.λppc_pc_map.
    655710     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    656711     let 〈program_counter, sigma_map〉 ≝ pc_map in
    657712     let 〈label, i〉 ≝ i in
    658713      let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in
    659          〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉
    660    ) acc l.
     714         〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉
     715   ) acc.
     716cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x -x #old_pc #old_map
     717@pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj
     718[ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
     719  <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl
     720| #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj
     721  [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl
     722  | #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx;
     723    #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew;
     724    >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew)
     725    elim (le_to_or_lt_eq … Hx) -Hx #Hx
     726    [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
     727      lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi)
     728      -Hind #Hind >lookup_insert_miss
     729      [2: @bitvector_of_nat_abs
     730        [3: @lt_to_not_eq @Hx
     731        |1: @(transitive_le … Hx)
     732        ]
     733        cases daemon (* XXX invariant *)
     734      ]
     735      >lookup_insert_miss
     736      [2: @bitvector_of_nat_abs
     737        [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n
     738        |1: @(transitive_le … (le_S_S_to_le … Hx))
     739        ]
     740        cases daemon (* XXX invariant *)
     741      ]
     742      @Hind
     743    | lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta
     744      #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) -Hind
     745      >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss
     746      [2: @bitvector_of_nat_abs
     747        [3: @lt_to_not_eq @le_n
     748        |1: @(transitive_le ??? (le_n (S x)))
     749        ]
     750        cases daemon (* XXX invariant *)
     751      ]
     752      >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second
     753      >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx)
     754      [3: @le_n]
     755      [2,3: cases daemon (* XXX invariant *)]
     756      <minus_n_n cases (half_add ???) #x #y normalize nodelta -x -y #Heq <Heq
     757      whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????);
     758      cases ins in p Hc; normalize nodelta
     759      [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
     760        [1,3,5,7: @refl
     761        |2,4,6,8: cases daemon (* XXX invariant *)
     762        ]
     763      |3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat
     764        [2: cases daemon (* XXX invariant *) ]
     765        whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl
     766      |6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
     767        [ @refl
     768        | cases daemon (* XXX invariant *)
     769        ]
     770      ]
     771    ]
     772  ]
     773]
     774qed.
    661775
    662776definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝
    663777  λprog.
    664778  λjump_expansion.
    665     sigma00 jump_expansion (\snd prog) 〈0, 〈0, Stub …〉〉.
     779    sigma00 jump_expansion (\snd prog)
     780    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉.
     781 normalize nodelta @conj
     782 [ / by refl/
     783 | #H @conj
     784   [ >lookup_insert_hit @refl
     785   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
     786   ]
     787 ]
     788qed.
    666789
    667790definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 →
    668791 list labelled_instruction → (nat × nat) ≝
    669792 λprogram,jump_expansion,instr_list.
    670    let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 〈0, 〈0, (Stub ? ?)〉〉 in (* acc copied from sigma0 *)
     793   let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list
     794   〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in
     795   (* acc copied from sigma0 *)
    671796   let 〈pc,map〉 ≝ pc_sigma_map in
    672797     〈ppc,pc〉.
     798 normalize nodelta @conj
     799 [ / by refl/
     800 | #H @conj
     801   [ >lookup_insert_hit @refl
     802   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
     803   ]
     804 ]
     805qed.
    673806
    674807definition sigma_safe: pseudo_assembly_program → policy_type2 →
     
    699832   [ None ⇒ λabs. ⊥
    700833   | Some r ⇒ λ_.r] (pi2 … policy).
    701  cases abs /2/
     834 cases abs /2 by /
    702835qed.
    703836
    704837(*CSC: Main axiom here, needs to be proved soon! *)
    705 axiom snd_assembly_1_pseudoinstruction_ok:
     838lemma snd_assembly_1_pseudoinstruction_ok:
    706839 ∀program:pseudo_assembly_program.∀pol: policy program.
    707840 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
     
    712845    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
    713846     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    714 
     847 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl
     848 whd in match (sigma ???); whd in match (sigma_safe ??); normalize nodelta
     849 lapply (pi2 ?? (
     850   sigma00 pol (\snd program)
     851    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉))
     852 normalize nodelta
     853 [ @conj
     854   [ / by refl/
     855   | #H >lookup_insert_hit @conj
     856     [ @refl
     857     | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
     858     ]
     859   ]
     860 |
     861 
     862 whd in match (sigma0 program pol);
     863(* here we go *)
     864cases daemon
     865qed.
     866 
    715867example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
    716868 cases daemon.
     
    722874   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
    723875
    724 lemma sigma00_append:
    725  ∀jump_expansion,l1,l2,acc.
     876(*lemma sigma00_append:
     877 ∀jump_expansion,l1,l2.
     878 ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).
    726879  sigma00 jump_expansion (l1@l2) acc =
    727    sigma00 jump_expansion
    728     l2 (sigma00 jump_expansion l1 acc).
    729  whd in match sigma00; normalize nodelta;
    730  #jump_expansion #l1 #l2 #acc @foldl_append
    731 qed.
     880  sigma00 jump_expansion
     881    l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)
    732882
    733883(* lemma sigma00_strict:
Note: See TracChangeset for help on using the changeset viewer.