proofs/containers/intrusive_doubly_linked_list/example.bend
bend-collections-laws-containers@1.0.0.0 · 22 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/history.bend as H
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/array_adapter.bend as A
5
6# Non-vacuity witness: middle, head and tail removal, then identity reuse.
7# Payload 42 is arbitrary; the general theorem quantifies over every P.
8def initial() -> G.Graph<A.Node,A.Root,U32>:
9 G.Graph{Nil{},Nil{},Nil{},42}
10
11def edits() -> List<&2,H.Edit<A.Node>>:
12 Con{H.Prepend{A.A{}},Con{H.Prepend{A.B{}},Con{H.Prepend{A.C{}},Con{H.RemoveAfter{Nil{},A.C{},A.B{},Con{A.A{},Nil{}}},Con{H.RemoveHead{A.C{},Con{A.A{},Nil{}}},Con{H.Prepend{A.B{}},Con{H.RemoveAfter{Nil{},A.B{},A.A{},Nil{}},Con{H.RemoveHead{A.B{},Nil{}},Nil{}}}}}}}}}
13
14def initial_valid() -> G.valid(~A.Node,~A.Root,~U32,~A.eq,~A.req,initial(),A.Ready{},Nil{}):
15 (Unit{},({==},Unit{}))
16
17def history_legal() -> H.legal(~A.Node,~A.Root,~U32,~A.eq,~A.req,edits(),initial(),A.Ready{},Nil{}):
18 ((Unit{},({==},{==})),(((({==},{==}),Unit{}),({==},{==})),(((({==},{==}),(({==},{==}),Unit{})),({==},{==})),({==},({==},(((({==},{==}),Unit{}),({==},{==})),({==},({==},Unit{}))))))))
19
20# This proof uses the public-function refinement and invariant induction.
21def correct() -> G.both({A.run(~U32,edits(),A.real(~U32,initial()),A.Ready{}) == A.real(~U32,H.run(~A.Node,~A.Root,~U32,~A.eq,~A.req,edits(),initial(),A.Ready{})) : A.Store<U32>},G.both(G.valid(~A.Node,~A.Root,~U32,~A.eq,~A.req,H.run(~A.Node,~A.Root,~U32,~A.eq,~A.req,edits(),initial(),A.Ready{}),A.Ready{},H.orders(~A.Node,edits(),Nil{})),{G.frame(~A.Node,~A.Root,~U32,H.run(~A.Node,~A.Root,~U32,~A.eq,~A.req,edits(),initial(),A.Ready{})) == 42 : U32})):
22 A.histories_correct(~U32,edits(),initial(),A.Ready{},Nil{},history_legal(),initial_valid())