This file contains the unprocessed output of HOL4 on the ring-buffer example. A cleaned-up version with comments can be found here. It can be reproduced by running holfoot-full -f ring_buffer.hol.
Saved definition __ "EXTRACT_SUBLIST_def"
val EXTRACT_SUBLIST_ALT_DEF =
|- first < LENGTH data ∧ len ≤ LENGTH data ⇒
(EXTRACT_SUBLIST first len data = SEG len first (data ++ data)):
thm
val EXTRACT_SUBLIST_def =
|- ∀first len data.
EXTRACT_SUBLIST first len data =
TAKE len (DROP first (data ++ data)):
thm
Saved definition __ "holfoot_ap_ring_buffer_def"
Saved theorem _____ "holfoot_ap_ring_buffer_REWRITE"
val holfoot_ap_ring_buffer_REWRITE =
|- ∀dta b s data.
holfoot_ap_ring_buffer dta b s data =
b ⟼ [... ] ★
(s = #_sv) ★
data_array(#_d, s, dta:_full_data) ★
pure(_f < _sv ∧ LENGTH data ≤ _sv ∧ (_sv = LENGTH _full_data) ∧
(data = EXTRACT_SUBLIST _f (LENGTH data) _full_data)):
thm
val holfoot_ap_ring_buffer_def =
|- ∀dta b s data.
holfoot_ap_ring_buffer dta b s data =
⍟
[b ⟼ [... ]; (s = #_sv); data_array(#_d, s, dta:_full_data);
pure(_f < _sv ∧ LENGTH data ≤ _sv ∧ (_sv = LENGTH _full_data) ∧
(data = EXTRACT_SUBLIST _f (LENGTH data) _full_data))]:
thm
Saved theorem _____ "holfoot_ap_ring_buffer_REWRITE2"
val holfoot_ap_ring_buffer_REWRITE2 =
|- ∀dta b s data.
holfoot_ap_ring_buffer dta b s data =
b ⟼ [size:s, len:LENGTH data, first: #_f, data: #_d] ★
(s = #_sv) ★
data_array(#_d, s, dta:_full_data) ★
pure(_f < _sv ∧ LENGTH data ≤ _sv ∧ (_sv = LENGTH _full_data) ∧
(data = EXTRACT_SUBLIST _f (LENGTH data) _full_data)):
thm
val holfoot_ap_ring_buffer_term = ``holfoot_ap_ring_buffer``: term
val mk_holfoot_ap_ring_buffer_absyn = fn:
Absyn.absyn * Absyn.absyn * Absyn.absyn * Absyn.absyn -> Absyn.absyn
Warning- in '/tmp/MLTEMPMwGpjM.hol', line 121.
Matches are not exhaustive.
Found near
fn
[b, s, data] =>
mk_holfoot_ap_ring_buffer_absyn (Absyn.mk_AQ (... ...), b, ...)
val ring_buffer_printer = fn:
'a ->
'b ->
(term_pp_types.grav * term_pp_types.grav * term_pp_types.grav ->
int -> term -> (term_pp_types.printing_info, 'c) smpp.t) ->
term_pp_types.ppstream_funs ->
'd -> int -> term -> term_pp_types.uprinter
Saved theorem _____ "VAR_RES_IS_STACK_IMPRECISE___USED_VARS___holfoot_ap_ring_buffer"
val VAR_RES_IS_STACK_IMPRECISE___USED_VARS___holfoot_ap_ring_buffer =
|- ∀dta b s data vs.
VAR_RES_IS_STACK_IMPRECISE_EXPRESSION___USED_VARS_SUBSET vs b ∧
VAR_RES_IS_STACK_IMPRECISE_EXPRESSION___USED_VARS_SUBSET vs s ⇒
VAR_RES_IS_STACK_IMPRECISE___USED_VARS vs
ring_buffer(b, s, dta: data):
thm
Saved theorem _____ "var_res_prop_varlist_update___holfoot_ap_ring_buffer"
val var_res_prop_varlist_update___asl_star___holfoot_MP =
|- VAR_RES_IS_STACK_IMPRECISE p1 ∧ VAR_RES_IS_STACK_IMPRECISE p2 ∧
(var_res_prop_varlist_update vL p1 = p1') ∧
(var_res_prop_varlist_update vL p2 = p2') ⇒
(var_res_prop_varlist_update vL p1 ★ p2 = p1' ★ p2'):
thm
val var_res_prop_varlist_update___holfoot_ap_ring_buffer =
|- IS_SOME (VAR_RES_IS_STACK_IMPRECISE_EXPRESSION___USED_VARS b) ∧
IS_SOME (VAR_RES_IS_STACK_IMPRECISE_EXPRESSION___USED_VARS s) ⇒
(var_res_prop_varlist_update vcL ring_buffer(b, s, dta: data) =
ring_buffer(var_res_exp_varlist_update vcL b,
var_res_exp_varlist_update vcL s, dta: data)):
thm
val it = (): unit
val it = (): unit
val it = (): unit
val EXTRACT_SUBLIST___len_0 = |- EXTRACT_SUBLIST first 0 data = []: thm
val EXTRACT_SUBLIST___data_Nil = |- EXTRACT_SUBLIST first l [] = []: thm
val EL_EXTRACT_SUBLIST =
|- n < len ∧ len ≤ LENGTH data ∧ first < LENGTH data ⇒
(EL n (EXTRACT_SUBLIST first len data) =
EL
(if n + first < LENGTH data then
n + first
else
(n + first − LENGTH data)) data):
thm
val EXTRACT_SUBLIST___head =
|- (EXTRACT_SUBLIST first len data = x::xs) ∧ first < LENGTH data ∧
len ≤ LENGTH data ⇒
(EL first data = x):
thm
val SEG_SUC_CONS_TL =
|- ∀m n l.
m + SUC n ≤ LENGTH l ⇒ (SEG m (SUC n) l = TL (SEG (SUC m) n l)):
thm
val SEG_SUC_CONS_SNOC =
|- ∀m n l.
SUC m + n ≤ LENGTH l ⇒
(SEG (SUC m) n l = SNOC (EL (m + n) l) (SEG m n l)):
thm
val SEG_FIRSTN =
|- ∀m n l. m + n < LENGTH l ⇒ (SEG m n l = SEG m n (TAKE (m + n) l)):
thm
val EXTRACT_SUBLIST___pop =
|- (EXTRACT_SUBLIST first len data = x::xs) ∧ first < LENGTH data ∧
len ≤ LENGTH data ⇒
(EXTRACT_SUBLIST ((first + 1) MOD LENGTH data) (len − 1) data = xs):
thm
val EXTRACT_SUBLIST___push =
|- first < LENGTH data ∧ len < LENGTH data ⇒
(EXTRACT_SUBLIST first len data ++ [x] =
EXTRACT_SUBLIST first (len + 1)
(REPLACE_ELEMENT x ((first + len) MOD LENGTH data) data)):
thm
parsing ... 0.066 s - OK
HOLFOOT_SPECIFICATION (
create(r; n_const) [w/r: r; | (0 < #n_const )] {
local (n = n_const), d;
r = new() ;
d = new-block (n) [dta];
r→size = n;
r→len = 0;
r→first = 0;
r→data = d;
} [w/r: r; | ring_buffer(r, #n_const, dta: [])]
clear(; b_const) [w/r: ; | ring_buffer(#b_const, #s, dta: data)] {
local (b = b_const); b→len = 0
} [w/r: ; | ring_buffer(#b_const, #s, dta: [])]
head(r; b_const) [w/r: r; | ring_buffer(#b_const, #s, dta: x::xs)] {
local (b = b_const), v_f, v_d;
v_f = b→first; v_d = b→data; r = (v_d + v_f)→dta;
} [w/r: r; | (r = #x) ★ ring_buffer(#b_const, #s, dta: x::xs)]
push(; b_const, x_const)
[w/r: ; | ring_buffer(#b_const, #s, dta: xs) ★
pure(LENGTH xs < s)] {
local (b = b_const), (x = x_const), v_s, v_f, v_l, v_d;
v_f = b→first;
v_l = b→len;
v_s = b→size;
v_d = b→data;
(v_d + ((v_f + v_l) MOD v_s) )→dta = x;
b→len = (v_l + 1);
} [w/r: ; | ring_buffer(#b_const, #s, dta: xs ++ [x_const])]
pop(r; b_const) [w/r: r; | ring_buffer(#b_const, #s, dta: x::xs)] {
local (b = b_const), v_f, v_d, v_l, v_s;
v_f = b→first;
v_d = b→data;
v_l = b→len;
v_s = b→size;
r = (v_d + v_f)→dta;
b→len = (v_l − 1);
b→first = ((v_f + 1) MOD v_s);
} [w/r: r; | (r = #x) ★ ring_buffer(#b_const, #s, dta: xs)]
test(b; x_const, y_const, z_const) [w/r: b; | pure(T)] {
local (x = x_const), (y = y_const), (z = z_const), h;
create(b; 2);
push(; b, x);
push(; b, y);
pop(h; b);
assert [(h = x)];
push(; b, z);
pop(h; b);
assert [(h = y)];
pop(h; b);
assert [(h = z)];
} [w/r: b; | ring_buffer(b, 2, dta: [])]
)
preprocessing ... 0.179 s - OK
verifying specification ...
* create ... 0.252 s - OK
* clear ... 0.223 s - OK
* head ... 0.539 s - OK
* push ... 1.529 s - OK
* pop ... 0.648 s - OK
* test ... 0.340 s - OK
done
time needed: 5.031 s
val clear_TAC = fn: tactic
val create_TAC = fn: tactic
val file = "ring_buffer.dsf": string
val final_thm =
|- HOLFOOT_SPECIFICATION (
create(r; n_const) [w/r: r; | (0 < #n_const )] {
local (n = n_const), d;
r = new() ;
d = new-block (n) [dta];
r→size = n;
r→len = 0;
r→first = 0;
r→data = d;
} [w/r: r; | ring_buffer(r, #n_const, dta: [])]
clear(; b_const)
[w/r: ; | ring_buffer(#b_const, #s, dta: data)] {
local (b = b_const); b→len = 0
} [w/r: ; | ring_buffer(#b_const, #s, dta: [])]
head(r; b_const)
[w/r: r; | ring_buffer(#b_const, #s, dta: x::xs)] {
local (b = b_const), v_f, v_d;
v_f = b→first; v_d = b→data; r = (v_d + v_f)→dta;
} [w/r: r; | (r = #x) ★ ring_buffer(#b_const, #s, dta: x::xs)]
push(; b_const, x_const)
[w/r: ; | ring_buffer(#b_const, #s, dta: xs) ★
pure(LENGTH xs < s)] {
local (b = b_const), (x = x_const), v_s, v_f, v_l, v_d;
v_f = b→first;
v_l = b→len;
v_s = b→size;
v_d = b→data;
(v_d + ((v_f + v_l) MOD v_s) )→dta = x;
b→len = (v_l + 1);
} [w/r: ; | ring_buffer(#b_const, #s, dta: xs ++ [x_const])]
pop(r; b_const)
[w/r: r; | ring_buffer(#b_const, #s, dta: x::xs)] {
local (b = b_const), v_f, v_d, v_l, v_s;
v_f = b→first;
v_d = b→data;
v_l = b→len;
v_s = b→size;
r = (v_d + v_f)→dta;
b→len = (v_l − 1);
b→first = ((v_f + 1) MOD v_s);
} [w/r: r; | (r = #x) ★ ring_buffer(#b_const, #s, dta: xs)]
test(b; x_const, y_const, z_const) [w/r: b; | pure(T)] {
local (x = x_const), (y = y_const), (z = z_const), h;
create(b; 2);
push(; b, x);
push(; b, y);
pop(h; b);
assert [(h = x)];
push(; b, z);
pop(h; b);
assert [(h = y)];
pop(h; b);
assert [(h = z)];
} [w/r: b; | ring_buffer(b, 2, dta: [])]
):
thm
val head_TAC = fn: tactic
val pop_TAC = fn: tactic
val push_TAC = fn: tactic
val test_TAC = fn: tactic