Module StacklayoutC

Require Import CoqlibC.
Require Import AST Memory Separation.
Require Import Bounds.

Local Open Scope sep_scope.
newly added *
Require Export Stacklayout.
Require Import Lia.


Local Opaque Z.add Z.mul.

Lemma bound_outgoing_stack_data: forall b,
   (4 * bound_outgoing b <= fe_stack_data (make_env b)).
Proof.
  Local Transparent make_env. ss. Local Opaque make_env.
  des_ifs. etrans; cycle 1.
  { eapply align_le; eauto. lia. }
  etrans; cycle 1.
  { generalize (bound_local_pos b); i. instantiate (1:= align (size_callee_save_area b (align (4 * bound_outgoing b) 8 + 8)) 8). lia. }
  etrans; cycle 1.
  { eapply align_le; eauto. lia. }
  etrans; cycle 1.
  { eapply size_callee_save_area_incr. }
  etrans; cycle 1.
  { instantiate (1:= align (4 * bound_outgoing b) 8). lia. }
  eapply align_le; eauto. lia.
Qed.