Timings for FlatToRiscvMetric.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev//./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev//./rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.timing
Require Import riscv.Spec.Primitives.
Require Import riscv.Platform.RiscvMachine.
Require Import riscv.Platform.MetricRiscvMachine.
Require Import riscv.Platform.MetricLogging.
Require Import riscv.Utility.Utility.
Require Import riscv.Utility.runsToNonDet.
Require Import riscv.Utility.InstructionCoercions.
Require Import compiler.util.Common.
Require Import compiler.eqexact.
Require Import coqutil.Tactics.Simp.
Require Import compiler.on_hyp_containing.
Require Import compiler.SeparationLogic.
Require Export coqutil.Word.SimplWordExpr.
Require Import compiler.GoFlatToRiscv.
Require Import compiler.DivisibleBy4.
Require Import compiler.MetricsToRiscv.
Require Import compiler.FlatImp.
Require Import compiler.RiscvWordProperties.
Require Import compiler.FlatToRiscvDef.
Require Import compiler.FlatToRiscvCommon.
Require Import compiler.FlatToRiscvLiterals.
Require Import coqutil.Tactics.fwd.
Local Arguments Z.mul: simpl never.
Local Arguments Z.add: simpl never.
Local Arguments Z.of_nat: simpl never.
Local Arguments Z.modulo : simpl never.
Local Arguments Z.pow: simpl never.
Local Arguments Z.sub: simpl never.
Context {iset: Decode.InstructionSet}.
Context {pos_map: map.map String.string Z}.
Context (compile_ext_call: pos_map -> Z -> Z -> stmt Z -> list Decode.Instruction).
Context {width: Z} {BW: Bitwidth width} {word: word.word width} {word_ok: word.ok word}.
Context {word_riscv_ok: RiscvWordProperties.word.riscv_ok word}.
Context {locals: map.map Z word} {locals_ok: map.ok locals}.
Context {mem: map.map word byte} {mem_ok: map.ok mem}.
Context {env: map.map String.string (list Z * list Z * stmt Z)} {env_ok: map.ok env}.
Context {M: Type -> Type}.
Context {MM: Monads.Monad M}.
Context {RVM: Machine.RiscvProgram M word}.
Context {PRParams: PrimitivesParams M MetricRiscvMachine}.
Context {ext_spec: Semantics.ExtSpec} {ext_spec_ok: Semantics.ext_spec.ok ext_spec}.
Context {PR: MetricPrimitives.MetricPrimitives PRParams}.
Context {BWM: bitwidth_iset width iset}.
Add Ring wring : (word.ring_theory (word := word))
(preprocess [autorewrite with rew_word_morphism],
morphism (word.ring_morph (word := word)),
constants [word_cst]).
Local Notation RiscvMachineL := (MetricRiscvMachine (width := width)).
Ltac run1done :=
apply runsToDone;
simpl_MetricRiscvMachine_get_set;
rewrite ?word.sru_ignores_hibits,
?word.slu_ignores_hibits,
?word.srs_ignores_hibits,
?word.mulhuu_simpl,
?word.divu0_simpl,
?word.modu0_simpl;
simpl in *;
eexists; (* finalMH *)
eexists; (* finalMetricsH *)
repeat split;
simpl_word_exprs word_ok;
first
[ solve [eauto]
| solve_MetricLog
| solve_word_eq word_ok
| solve [wcancel_assumption]
| eapply rearrange_footpr_subset; [ eassumption | wwcancel ]
| solve [solve_valid_machine word_ok]
| idtac ].
Ltac IH_sidecondition :=
simpl_word_exprs word_ok;
try solve
[ reflexivity
| auto
| solve_word_eq word_ok
| simpl; solve_divisibleBy4
| solve_valid_machine word_ok
| eapply rearrange_footpr_subset; [ eassumption | wwcancel ]
| wcancel_assumption ].
Hypothesis no_ext_calls: forall t mGive action argvals outcome,
ext_spec t mGive action argvals outcome -> False.
Hypothesis stackalloc_always_0: forall x n body t m (l: locals) mc post,
FlatImp.exec map.empty (SStackalloc x n body) t m l mc post -> n = 0.
Hypothesis sp_always_set: forall l: locals,
map.get l RegisterNames.sp = Some (word.of_Z 42).
(* not needed any more *)
Definition stmt_not_too_big(s: stmt Z): Prop := True.
Lemma compile_stmt_correct:
forall (s: stmt Z) t initialMH initialRegsH postH initialMetricsH,
FlatImp.exec map.empty s t initialMH initialRegsH initialMetricsH postH ->
forall R Rexec (initialL: RiscvMachineL) insts pos,
compile_stmt iset compile_ext_call map.empty pos 12345678 s = insts ->
stmt_not_too_big s ->
valid_FlatImp_vars s ->
divisibleBy4 initialL.(getPc) ->
initialL.(getRegs) = initialRegsH ->
subset (footpr (program iset initialL.(getPc) insts * Rexec)%sep) (of_list initialL.(getXAddrs)) ->
(program iset initialL.(getPc) insts * Rexec * eq initialMH * R)%sep initialL.(getMem) ->
initialL.(getLog) = t ->
initialL.(getNextPc) = add initialL.(getPc) (word.of_Z 4) ->
valid_machine initialL ->
runsTo initialL (fun finalL => exists finalMH finalMetricsH,
postH finalL.(getLog) finalMH finalL.(getRegs) finalMetricsH /\
subset (footpr (program iset initialL.(getPc) insts * Rexec)%sep)
(of_list finalL.(getXAddrs)) /\
(program iset initialL.(getPc) insts * Rexec * eq finalMH * R)%sep finalL.(getMem) /\
finalL.(getPc) = add initialL.(getPc)
(word.mul (word.of_Z 4) (word.of_Z (Z.of_nat (length insts)))) /\
finalL.(getNextPc) = word.add finalL.(getPc) (word.of_Z 4) /\
(finalL.(getMetrics) - initialL.(getMetrics) <=
lowerMetrics (finalMetricsH - initialMetricsH))%metricsL /\
valid_machine finalL).
induction 1; intros;
repeat match goal with
| m: _ |- _ => destruct_RiscvMachine m; simpl_MetricRiscvMachine_get_set
end;
simpl in *;
subst;
simp.
lazymatch goal with
| A: map.get map.empty _ = Some _ |- _ =>
exfalso; simpl in *;
rewrite map.get_empty in A
end.
unfold Memory.load, Memory.load_Z in *.
simpl_MetricRiscvMachine_get_set.
assert ((eq m * (program iset initialL_pc [[compile_store iset sz a v o]] * Rexec * R))%sep
initialL_mem) as A by ecancel_assumption.
match goal with
| H: _ |- _ => pose proof (store_bytes_frame H A) as P; move H at bottom;
unfold Memory.store, Memory.store_Z, Memory.store_bytes in H
end.
destruct P as (finalML & P1 & P2).
destruct (eq_sym (LittleEndianList.length_le_split (Memory.bytes_per(width:=width) sz) (word.unsigned val))) in t0, E.
eapply preserve_subset_of_xAddrs.
assert (map.get (map.put l x (word.add initialL_pc (word.of_Z 4))) i = Some index).
rewrite map.get_put_diff by congruence.
assert (Memory.load sz initialL_mem
(word.add (word.add (word.add initialL_pc (word.of_Z 4)) index) (word.of_Z 0))
= Some v).
eapply load_from_compile_byte_list.
rewrite !map.put_put_same in *.
assert (valid_register RegisterNames.sp) by (cbv; auto).
specialize (stackalloc_always_0 x n body t mSmall l mc post).
move stackalloc_always_0 at bottom.
eapply stackalloc_always_0.
eapply H1 with (mStack := map.empty) (mCombined := mSmall).
rewrite map.split_empty_r.
unfold Memory.anybytes, Memory.ftprint, map.of_disjoint_list_zip in *.
rewrite map.split_empty_r in H6p0p1.
repeat match goal with
| m: _ |- _ => destruct_RiscvMachine m; simpl_MetricRiscvMachine_get_set
end.
split; [solve [sidecondition]|].
split; [solve [sidecondition]|].
split; [solve [sidecondition]|].
RunInstruction.get_runsTo_valid_for_free.
eapply compile_lit_correct_full.
(* ecancel. (* The term "Tree.Leaf (subset (footpr (program iset initialL_pc (compile_lit x v) * Rexec)%sep))" has type "Tree.Tree (set word -> Prop)" while it is expected to have type "Tree.Tree (?map -> Prop)". *) *)
eapply RelationClasses.reflexivity.
run1done;
remember (updateMetricsForLiteral v initialL_metrics) as finalMetrics;
symmetry in HeqfinalMetrics;
pose proof update_metrics_for_literal_bounded (width := width) as Hlit;
specialize Hlit with (1 := HeqfinalMetrics);
solve_MetricLog.
match goal with
| o: Syntax.bopname.bopname |- _ => destruct o
end;
simpl in *.
all: match goal with
| y: operand, H: context[Syntax.bopname.eq] |- _ =>
destr y; simpl in *;
[ run1det; simpl_MetricRiscvMachine_get_set; run1det; run1done
| ]; try fwd
| y: operand |- _ =>
destr y; simpl in *;
[ run1det; run1done
| ]; try fwd
end; simpl in *; fwd.
all: try match goal with
| H: context[Decode.InvalidInstruction] |- _ =>
assert (Encode.verify (Decode.InvalidInstruction (-1)) iset \/
valid_InvalidInstruction (Decode.InvalidInstruction (-1))) by
( eapply invert_ptsto_instr; ecancel_assumption)
| H: _ |- _ => run1det; run1done
end.
all:
try match goal with
| H: Encode.verify (Decode.InvalidInstruction (-1)) iset \/
valid_InvalidInstruction (Decode.InvalidInstruction (-1)) |- _ =>
exfalso; destruct H;
[ unfold Encode.verify in H; simpl in H;
destruct H; assumption | unfold valid_InvalidInstruction in H]; fwd
end.
all:
try match goal with
| H: 0 <= -1 < 2^32 |- False
=> destruct H;
match goal with
| H: 0 <= -1 |- False => destruct H; simpl; reflexivity
end
end.
all: try match goal with
| H: ?post _ _ _ |- ?post _ _ _ => eqexact H
end.
all : rewrite ?word.srs_ignores_hibits,
?word.sru_ignores_hibits,
?word.slu_ignores_hibits,
?word.mulhuu_simpl,
?word.divu0_simpl,
?word.modu0_simpl; trivial.
all: try solve_MetricLog.
rewrite reduce_eq_to_sub_and_lt.
(* SIf/Then *)
(* execute branch instruction, which will not jump *)
eapply runsTo_det_step_with_valid_machine; simpl in *; subst.
simpl_MetricRiscvMachine_get_set.
destruct cond; [destruct op | ];
simpl in *; simp; repeat (simulate'; simpl_bools; simpl); try reflexivity.
eapply runsTo_trans; simpl_MetricRiscvMachine_get_set.
(* use IH for then-branch *)
eapply IHexec; IH_sidecondition.
(* jump over else-branch *)
destruct_RiscvMachine middle.
(* SIf/Else *)
(* execute branch instruction, which will jump over then-branch *)
eapply runsTo_det_step_with_valid_machine; simpl in *; subst.
destruct cond; [destruct op | ];
simpl in *; simp; repeat (simulate'; simpl_bools; simpl); try reflexivity.
eapply runsTo_trans; simpl_MetricRiscvMachine_get_set.
(* use IH for else-branch *)
eapply IHexec; IH_sidecondition.
(* at end of else-branch, i.e. also at end of if-then-else, just prove that
computed post satisfies required post *)
destruct_RiscvMachine middle.
on hyp[(stmt_not_too_big body1); runsTo] do (fun H => rename H into IH1).
on hyp[(stmt_not_too_big body2); runsTo] do (fun H => rename H into IH2).
on hyp[(stmt_not_too_big (SLoop body1 cond body2)); runsTo] do (fun H => rename H into IH12).
eapply runsTo_trans; simpl_MetricRiscvMachine_get_set.
(* 1st application of IH: part 1 of loop body *)
eapply IH1; IH_sidecondition.
destruct_RiscvMachine middle.
destruct (eval_bcond middle_regs cond) as [condB|] eqn: E.
2: exfalso;
match goal with
| H: context [_ <> None] |- _ => solve [eapply H; eauto]
end.
(* true: iterate again *)
eapply runsTo_det_step_with_valid_machine; simpl in *; subst.
destruct cond; [destruct op | ];
simpl in *; simp; repeat (simulate'; simpl_bools; simpl); try reflexivity.
eapply runsTo_trans; simpl_MetricRiscvMachine_get_set.
(* 2nd application of IH: part 2 of loop body *)
eapply IH2; IH_sidecondition; simpl_MetricRiscvMachine_get_set;
try eassumption; IH_sidecondition.
destruct_RiscvMachine middle.
(* jump back to beginning of loop: *)
eapply runsTo_trans; simpl_MetricRiscvMachine_get_set.
(* 3rd application of IH: run the whole loop again *)
eapply IH12 with (pos := pos); IH_sidecondition; simpl_MetricRiscvMachine_get_set;
try eassumption; IH_sidecondition.
(* at end of loop, just prove that computed post satisfies required post *)
destruct_RiscvMachine middle.
(* false: done, jump over body2 *)
eapply runsTo_det_step_with_valid_machine; simpl in *; subst.
destruct cond; [destruct op | ];
simpl in *; simp; repeat (simulate'; simpl_bools; simpl); try reflexivity.
on hyp[(stmt_not_too_big s1); runsTo] do (fun H => rename H into IH1).
on hyp[(stmt_not_too_big s2); runsTo] do (fun H => rename H into IH2).
eapply IH1; IH_sidecondition.
destruct_RiscvMachine middle.
eapply IH2; IH_sidecondition; simpl_MetricRiscvMachine_get_set;
try eassumption; IH_sidecondition.
destruct_RiscvMachine middle.