# Changeset 1870

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

Unmodified
Removed
• ## src/ASM/Arithmetic.ma

 r1646 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ λn,v. nat_of_bitvector_aux n O v. lemma bitvector_of_nat_ok: ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. #n elim n -n [ #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 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) ] qed. lemma bitvector_of_nat_abs: ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y). #n #x #y #Hx #Hy #Heq @notb_elim lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/ | #H / by I/ ] qed. definition two_complement_negation ≝ λn: nat.
• ## src/ASM/Assembly.ma

 r1668 let lookup_datalabels ≝ λx.zero ? in let pc_delta_assembled ≝ assembly_1_pseudoinstruction (λx.bitvector_of_nat ? program_counter) assembly_1_pseudoinstruction (λx.pc_bv) jump_expansion (*ppc_bv*) pc_bv lookup_datalabels i in let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in 〈pc_delta + program_counter, costs〉 ]. axiom nat_of_bitvector_bitvector_of_nat: ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n. axiom bitvector_of_nat_nat_of_bitvector: ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v. lemma nth_cons: ∀n,A,h,t,y. nth (S n) A (h::t) y = nth n A t y. #n #A #h #t #y /2 by refl/ qed. lemma fetch_pseudo_instruction_prefix: ∀prefix.∀x.∀ppc.ppc < (|prefix|) → fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) = fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc). #prefix #x #ppc elim prefix [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??); whd in match (fetch_pseudo_instruction ((h::t)@x) ?); >nth_append_first [ // | >nat_of_bitvector_bitvector_of_nat [ @Hppc | cases daemon (* XXX invariant *) ] ] ] qed. (* This establishes the correspondence between pseudo program counters and program counters. It is at the heart of the proof. *) (*CSC: code taken from build_maps *) (*JPB: Here it gets strange because we need a program counter for the jump *expansion, but we can't give it to the type because we don't have it yet. Argh. *add a forall type?*) definition sigma00: policy_type2 → list ? → ? → (nat × (nat × (BitVectorTrie Word 16))) ≝ definition sigma00: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? → (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). let 〈ppc,pc_map〉 ≝ ppc_pc_map in let 〈program_counter, sigma_map〉 ≝ pc_map in ppc = |l| ∧ (ppc = |l| → (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ (∀x.x < |l| → ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi))))) ) ≝ λjump_expansion: policy_type2. λl:list labelled_instruction. λacc. foldl … (λppc_pc_map,i. foldl_strong ? (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)). let 〈ppc,pc_map〉 ≝ ppc_pc_map in let 〈program_counter, sigma_map〉 ≝ pc_map in (ppc = |prefix|) ∧ (ppc = |prefix| → (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧ (∀x.x < |prefix| → ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi → let pc_x ≝  bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) + (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi)))))) ) l (λhd.λi.λtl.λp.λppc_pc_map. let 〈ppc,pc_map〉 ≝ ppc_pc_map in let 〈program_counter, sigma_map〉 ≝ pc_map in let 〈label, i〉 ≝ i in let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ) acc l. 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉 ) acc. cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x -x #old_pc #old_map @pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl | #x <(pair_eq1 ?????? Heq) >append_length append_length (injective_S … Hnew) elim (le_to_or_lt_eq … Hx) -Hx #Hx [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi) -Hind #Hind >lookup_insert_miss [2: @bitvector_of_nat_abs [3: @lt_to_not_eq @Hx |1: @(transitive_le … Hx) ] cases daemon (* XXX invariant *) ] >lookup_insert_miss [2: @bitvector_of_nat_abs [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n |1: @(transitive_le … (le_S_S_to_le … Hx)) ] cases daemon (* XXX invariant *) ] @Hind | lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) -Hind >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss [2: @bitvector_of_nat_abs [3: @lt_to_not_eq @le_n |1: @(transitive_le ??? (le_n (S x))) ] cases daemon (* XXX invariant *) ] >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx) [3: @le_n] [2,3: cases daemon (* XXX invariant *)] Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat [1,3,5,7: @refl |2,4,6,8: cases daemon (* XXX invariant *) ] |3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat [2: cases daemon (* XXX invariant *) ] whd in match (expand_pseudo_instruction ?????); normalize Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat [ @refl | cases daemon (* XXX invariant *) ] ] ] ] ] qed. definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝ λprog. λjump_expansion. sigma00 jump_expansion (\snd prog) 〈0, 〈0, Stub …〉〉. sigma00 jump_expansion (\snd prog) 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉. normalize nodelta @conj [ / by refl/ | #H @conj [ >lookup_insert_hit @refl | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n ] ] qed. definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 → list labelled_instruction → (nat × nat) ≝ λprogram,jump_expansion,instr_list. let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 〈0, 〈0, (Stub ? ?)〉〉 in (* acc copied from sigma0 *) let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in (* acc copied from sigma0 *) let 〈pc,map〉 ≝ pc_sigma_map in 〈ppc,pc〉. normalize nodelta @conj [ / by refl/ | #H @conj [ >lookup_insert_hit @refl | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n ] ] qed. definition sigma_safe: pseudo_assembly_program → policy_type2 → [ None ⇒ λabs. ⊥ | Some r ⇒ λ_.r] (pi2 … policy). cases abs /2/ cases abs /2 by / qed. (*CSC: Main axiom here, needs to be proved soon! *) axiom snd_assembly_1_pseudoinstruction_ok: lemma snd_assembly_1_pseudoinstruction_ok: ∀program:pseudo_assembly_program.∀pol: policy program. ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl whd in match (sigma ???); whd in match (sigma_safe ??); normalize nodelta lapply (pi2 ?? ( sigma00 pol (\snd program) 〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉)) normalize nodelta [ @conj [ / by refl/ | #H >lookup_insert_hit @conj [ @refl | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n ] ] | whd in match (sigma0 program pol); (* here we go *) cases daemon qed. example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. cases daemon. (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list. lemma sigma00_append: ∀jump_expansion,l1,l2,acc. (*lemma sigma00_append: ∀jump_expansion,l1,l2. ∀acc:ℕ×ℕ×(BitVectorTrie Word 16). sigma00 jump_expansion (l1@l2) acc = sigma00 jump_expansion l2 (sigma00 jump_expansion l1 acc). whd in match sigma00; normalize nodelta; #jump_expansion #l1 #l2 #acc @foldl_append qed. sigma00 jump_expansion l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*) (* lemma sigma00_strict:
Note: See TracChangeset for help on using the changeset viewer.