Library topsy_hmInit_prg

Require Import ssreflect.
From mathcomp Require Import eqtype.
Require Import bipl ZArith.
Require Import expr_b_dp.
Require Import topsy_hm.

Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.

Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.

Definition hmEnd : var.v := 1%nat.

Definition hmInit (adr sz : nat) :=
  hmStart <- nat_e adr ;
  hmStart -.> next *<- nat_e adr \+ nat_e sz \- cst_e 2%Z ;
  hmStart -.> status *<- Free ;
  hmEnd <-* hmStart -.> next ;
  hmEnd -.> next *<- cst_e 0%Z ;
  hmEnd -.> status *<- Allocated.