Datastructure with potential in abstract layer

[maxhaslbeck]

Idea

We want to try to prove an complex data structure whose time analysis involves potential on the abstract layer.

For dynamic arrays with time analysis, we worked directly on Imperative-HOL-Time with its machinery and then extracted an hnr rule from that.
Now we want to avoid setting up complex time infrastructure for the basic LLVM level, and instead prove the data structure correct on the abstract level, then refining it with the basic data structure arrays we already have.

Rough Approach

• prove list_copy on NREST level with copy
• synthesize array_copy
• model dynamic arrays (as,c,n) and their operations (new, push, pop, update, lookup, [destroy :: dynarray => array ?]) in NREST
• synthesize raw_hnr
• prove hnr_shift_money
• encapsulate array an potential into dyn_array_assn
• prove hnr rule
• encapsulate and hide potential in hnr rule

Notes

hnr ($(1 load) ** array_assn xs xsi) array_nth (array_assn xs xsi) A (return (xs!i))

hnr_shift_money:
hnr ($t ** G) c G' R a
<-->
hnr (G) c G' R (consume a t)

consume (RETURNT ra) Ca ≤ m
<-->
consume (RETURNT ra) (Ca+t) ≤ consume m t


hnr (array_assn ** $Phi) pushi (array_assn ** $Phi)  R (consume (return xs@[x]) 1)

--> 
hnr (array_assn ** $Phi) ?c ?G' ?R (copy )
--> 
hnr (array_assn) ?c ?G' ?R (consume Phi copy )


RAW:
hnr (array_assn) pushi (array_assn)  R (consume (return xs@[x]) (raw_costs(xs,c,n)))

inres (push x) x' ==>
\Phi((xs,n))-\Phi(x') + advertised_costs >= raw_costs(xs,c,n)

ADVERTISED_AUX: 
hnr (array_assn * (DELTA)) pushi (array_assn)  R (consume (return xs@[x]) (advertised_costs ))

FINAL:
hnr (array_assn * (\Phi(xs))) pushi (array_assn * \Phi(xs@[x]))  R (consume (return xs@[x]) (advertised_costs ))

dyn_array_assn1 (xs,n,c) (xsi,ni,ci) 
= array_assn xs xsi ** int_assn n ni ** int_assn c ci ** \Phi(xs,n,c)

dyn_array_assn2  xs' (xs,n,c) == xs' = take n xs



- prove operation auf arrays
- RAW:
    hnr (array_assn ) push_llvm (array_assn... (array_assn)  ( SPECT [ as@[x] |-> (if ... then 2*|as| else 1) ] )
    - hnr (dyn_array_assn ) push_llvm (array_assn... (array_assn)  ( SPECT [ as@[x] |-> 2  ] )


  "hn_refine Γ c Γ' R m =
  nofailT m ⟶
  (∀F s cr . 
      llSTATE (Γ ∧* F) (s,cr) ⟶ 
      (∃ra Ca. consume (RETURNT ra) Ca ≤ m
        ∧ wp c (λr. llSTATE (Γ' ∧* R ra r ∧* F ∧* GC)) (s, cr+Ca)
      )
  )"

dyn_array_assn (p,n) as =
  array_assn p(take n as) * $ Φ (n, as)

hnr GAMMA c GAMMA' R (m )

m = SPEC (%. sort xs) ( sort_time )

GAMMA = SL+TC assertion

dyn_array (p,n) xs
= \exists bs, xs = take n bs ∧ n< |bs| ∗$(Φ r) * p|->bs