From 7557425fb9b9dd5ba6bc3563ef1e0e6e0ebd5f8c Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Fri, 26 Feb 2016 11:25:29 +0100 Subject: [PATCH] new example: patience game (VSTTE 14) --- examples/patience.mlw | 896 ++++++++++++++++++++++++++++++ examples/patience/why3session.xml | 526 ++++++++++++++++++ examples/patience/why3shapes.gz | Bin 0 -> 13880 bytes 3 files changed, 1422 insertions(+) create mode 100644 examples/patience.mlw create mode 100644 examples/patience/why3session.xml create mode 100644 examples/patience/why3shapes.gz diff --git a/examples/patience.mlw b/examples/patience.mlw new file mode 100644 index 000000000..8614c6d8c --- /dev/null +++ b/examples/patience.mlw @@ -0,0 +1,896 @@ + + +(** {1 The Patience Solitaire Game} + +Problem 1 from the {h Verified Software +Competition 2014} + +Patience Solitaire is played by taking cards one-by-one from a deck of +cards and arranging them face up in a sequence of stacks arranged from +left to right as follows. The very first card from the deck is kept +face up to form a singleton stack. Each subsequent card is placed on +the leftmost stack where its card value is no greater than the topmost +card on that stack. If there is no such stack, then a new stack is +started to right of the other stacks. We can do this with positive +numbers instead of cards. If the input sequence is 9, 7, 10, 9, 5, 4, +and 10, then the stacks develop as + +{h
```}
+<[[9]]>
+<[[7, 9]]>
+<[[7, 9]], [[10]]>
+<[[7, 9]], [[9, 10]]>
+<[[5, 7, 9]], [[9, 10]]>
+<[[4, 5, 7, 9]], [[9, 10]]>
+<[[4, 5, 7, 9]], [[9, 10]], [[10]]>
+{h ```
} + +Verify the claim is that the number of stacks at the end of the game +is the length of the longest (strictly) increasing subsequence in the +input sequence. + + +*) + + + +(** {2 Preliminary: pigeon-hole lemma} *) + + +module PigeonHole + +(** The Why standard library provides a lemma + [map.MapInjection.injective_surjective] stating that a map from + [(0..n-1)] to [(0..n-1)] that is an injection is also a + surjection. + + This is more or less equivalent to the pigeon-hole lemma. However, we need such a lemma more generally on functions instead of maps. + + Thus we restate the pigeon-hole lemma here. Proof is left as an exercise. + +*) + + use import int.Int + use HighOrd + + predicate range (f: int -> int) (n: int) (m:int) = + forall i: int. 0 <= i < n -> 0 <= f i < m + (** [range f n m] is true when [f] maps the domain + [(0..n-1)] into [(0..m-1)] *) + + predicate injective (f: int -> int) (n: int) (m:int) = + forall i j: int. 0 <= i < j < n -> f i <> f j + (** [injective f n m] is true when [f] is an injection + from [(0..n-1)] to [(0..m-1)] *) + + + + +(* + lemma pigeon_hole2: + forall n m:int, f: int -> int. + range f n m /\ n > m >= 0 -> + not (injective f n m) +*) + + + + + exception Found + + function shift (f: int -> int) (i:int) : int -> int = + \k:int. if k < i then f k else f (k+1) + + let rec lemma pigeon_hole (n m:int) (f: int -> int) + requires { range f n m } + requires { n > m >= 0 } + variant { m } + ensures { not (injective f n m) } + = try + for i = 0 to n-1 do + invariant { forall k. 0 <= k < i -> f k <> m-1 } + if f i = m-1 then + begin + (* we have found index i such that f i = m-1 *) + for j = i+1 to n-1 do + invariant { forall k. i < k < j -> f k <> m-1 } + if f j = m-1 then raise Found + done; + (* we know that for all k <> i, f k <> m-1 *) + let g = shift f i in + assert { range g (n-1) (m-1) }; + pigeon_hole (n-1) (m-1) g; + raise Found; + end + done; + (* we know that for all k, f k <> m-1 *) + assert { range f n (m-1) }; + pigeon_hole n (m-1) f + with Found -> + (* we know that f i = f j = m-1 hence we are done *) + () + end + +end + + + + +(** {2 Patience idiomatic code} *) + + +module PatienceCode + + use import int.Int + use import list.List + use import list.RevAppend + + (** this code was the one written initially, without any + specification, except for termination, ans unreachability + of the 'absurd' branch'. + + It can be tested, see below. *) + + type card = int + + (** stacks are well-formed if they are non-empty *) + predicate wf_stacks (stacks: list (list card)) = + match stacks with + | Nil -> true + | Cons Nil _ -> false + | Cons (Cons _ _) rem -> wf_stacks rem + end + + (** concatenation of well-formed stacks is well-formed *) + let rec lemma wf_rev_append_stacks (s1 s2: list (list int)) + requires { wf_stacks s1 } + requires { wf_stacks s2 } + variant { s1 } + ensures { wf_stacks (rev_append s1 s2) } + = match s1 with + | Nil -> () + | Cons Nil _ -> absurd + | Cons s rem -> wf_rev_append_stacks rem (Cons s s2) + end + + (** [push_card c stacks acc] pushes card [c] on stacks [stacks], + assuming [acc] is an accumulator (in reverse order) of stacks + where [c] could not be pushed. + *) + let rec push_card (c:card) (stacks : list (list card)) + (acc : list (list card)) : list (list card) + requires { wf_stacks stacks } + requires { wf_stacks acc } + variant { stacks } + ensures { wf_stacks result } + = + match stacks with + | Nil -> + (* we put card [c] in a new stack *) + rev_append (Cons (Cons c Nil) acc) Nil + | Cons stack remaining_stacks -> + match stack with + | Nil -> absurd (* because [wf_stacks stacks] *) + | Cons c' _ -> + if c <= c' then + (* card is placed on the leftmost stack where its card + value is no greater than the topmost card on that + stack *) + rev_append (Cons (Cons c stack) acc) remaining_stacks + else + (* try next stack *) + push_card c remaining_stacks (Cons stack acc) + end + end + + let rec play_cards (input: list card) (stacks: list (list card)) + : list (list card) + requires { wf_stacks stacks } + variant { input } + ensures { wf_stacks result } + = + match input with + | Nil -> stacks + | Cons c rem -> + let stacks' = push_card c stacks Nil in + play_cards rem stacks' + end + + + let play_game (input: list card) : list (list card) = + play_cards input Nil + + + (** test, can be run using [why3 patience.mlw --exec PatienceCode.test] *) + let test () = + (** the list given in the problem description + 9, 7, 10, 9, 5, 4, and 10 *) + play_game + (Cons 9 (Cons 7 (Cons 10 (Cons 9 (Cons 5 (Cons 4 (Cons 10 Nil))))))) + +end + + +(** {2 Abstract version of Patience game} *) + +module PatienceAbstract + + use import int.Int + +(** To specify the expected property of the Patience game, we first + provide an abstract version, working on a abstract state that + includes a lot of information regarding the positions of the cards + in the stack and so on. + + This abstract state should then be including in the real code as a + ghost state, with a gluing invariant that matches the ghost state + and the concrete stacks of cards. + +*) + + + type card = int + + (** {3 Abstract state} *) + + use import map.Map + use import map.Const + + type state = { + mutable num_elts : int; + (** number of cards already seen *) + mutable values : map int card; + (** cards values seen, indexed in the order they have been seen, + from [0] to [num_elts-1] *) + mutable num_stacks : int; + (** number of stacks built so far *) + mutable stack_sizes : map int int; + (** sizes of these stacks, numbered from [0] to [num_stacks - 1] *) + mutable stacks : map int (map int int); + (** indexes of the cards in respective stacks *) + mutable positions : map int (int,int); + (** table that given a card index, provides its position, i.e. in + which stack it is and at which height *) + mutable preds : map int int; + (** predecessors of cards, i.e. for each card index [i], [preds[i]] + provides an index of a card in the stack on the immediate left, + whose value is smaller. Defaults to [-1] if the card is on the + leftmost stack. *) + } + +(** {3 Invariants on the abstract state} *) + + predicate inv (s:state) = + 0 <= s.num_stacks <= s.num_elts + (** the number of stacks is less or equal the number of cards *) + /\ (s.num_elts > 0 -> s.num_stacks > 0) + (** when there is at least one card, there is at least one stack *) + /\ (forall i. 0 <= i < s.num_stacks -> + s.stack_sizes[i] >= 1 + (** stacks are non-empty *) + /\ forall j. 0 <= j < s.stack_sizes[i] -> + 0 <= s.stacks[i][j] < s.num_elts) + (** contents of stacks are valid card indexes *) + /\ (forall i. 0 <= i < s.num_elts -> + let (is,ip) = s.positions[i] in + 0 <= is < s.num_stacks && + let st = s.stacks[is] in + 0 <= ip < s.stack_sizes[is] && + st[ip] = i) + (** the position table of cards is correct, i.e. when + [(is,ip) = s.positions[i]] then card [i] indeed + occurs in stack [is] at height [ip] *) + /\ (forall is. 0 <= is < s.num_stacks -> + forall ip. 0 <= ip < s.stack_sizes[is] -> + let idx = s.stacks[is][ip] in + (is,ip) = s.positions[idx]) + (** positions is the proper inverse of stacks *) + /\ (forall i. 0 <= i < s.num_stacks -> + let stack_i = s.stacks[i] in + forall j,k. 0 <= j < k < s.stack_sizes[i] -> + stack_i[j] < stack_i[k]) + (** in a given stack, indexes are increasing from bottom to top *) + /\ (forall i. 0 <= i < s.num_stacks -> + let stack_i = s.stacks[i] in + forall j,k. 0 <= j <= k < s.stack_sizes[i] -> + s.values[stack_i[j]] >= s.values[stack_i[k]]) + (** in a given stack, card values are decreasing from bottom to top *) + /\ (forall i. 0 <= i < s.num_elts -> + let pred = s.preds[i] in + -1 <= pred < s.num_elts && + (** the predecessor is a valid index or [-1] *) + pred < i /\ + (** predecessor is always a smaller index *) + let (is,_ip) = s.positions[i] in + if pred < 0 then is = 0 + (** if predecessor is [-1] then [i] is in leftmost stack *) + else + s.values[pred] < s.values[i] /\ + (** if predecessor is not [-1], it denotes a card with smaller value... *) + is > 0 && + (** ...the card is not on the leftmost stack... *) + let (ps,_pp) = s.positions[pred] in + ps = is - 1) + (** ...and predecessor is in the stack on the immediate left *) + + + + (** {2 Programs} *) + + use import ref.Ref + exception Return int + + (** [play_card c i s] pushes the card [c] on state [s] *) + let play_card (c:card) (s:state) : unit + requires { inv s } + writes { s } + ensures { inv s } + ensures { s.num_elts = (old s).num_elts + 1 } + ensures { s.values = (old s).values[(old s).num_elts <- c] } + = + let pred = ref (-1) in + try + for i = 0 to s.num_stacks - 1 do + invariant { if i=0 then !pred = -1 else + let stack_im1 = s.stacks[i-1] in + let stack_im1_size = s.stack_sizes[i-1] in + let top_stack_im1 = stack_im1[stack_im1_size - 1] in + !pred = top_stack_im1 /\ + c > s.values[!pred] /\ + 0 <= !pred < s.num_elts /\ + let (ps,_pp) = s.positions[!pred] in + ps = i - 1 + } + let stack_i = s.stacks[i] in + let stack_i_size = s.stack_sizes[i] in + let top_stack_i = stack_i[stack_i_size - 1] in + if c <= s.values[top_stack_i] then + raise (Return i) + else + begin + assert { 0 <= top_stack_i < s.num_elts }; + assert { let (is,ip) = s.positions[top_stack_i] in + 0 <= is < s.num_stacks && + 0 <= ip < s.stack_sizes[is] && + s.stacks[is][ip] = top_stack_i && + is = i /\ ip = stack_i_size - 1 + }; + pred := top_stack_i + end + done; + (* we add a new stack *) + let idx = s.num_elts in + let i = s.num_stacks in + let stack_i = s.stacks[i] in + let new_stack_i = stack_i[0 <- idx] in + s.num_elts <- idx + 1; + s.values <- s.values[idx <- c]; + s.num_stacks <- s.num_stacks + 1; + s.stack_sizes <- s.stack_sizes[i <- 1]; + s.stacks <- s.stacks[i <- new_stack_i]; + s.positions <- s.positions[idx <- (i,0)]; + s.preds <- s.preds[idx <- !pred] + with Return i -> + let stack_i = s.stacks[i] in + let stack_i_size = s.stack_sizes[i] in + (* we put c on top of stack i *) + let idx = s.num_elts in + let new_stack_i = stack_i[stack_i_size <- idx] in + s.num_elts <- idx + 1; + s.values <- s.values[idx <- c]; + (* s.num_stacks unchanged *) + s.stack_sizes <- s.stack_sizes[i <- stack_i_size + 1]; + s.stacks <- s.stacks[i <- new_stack_i]; + s.positions <- s.positions[idx <- (i,stack_i_size)]; + s.preds <- s.preds[idx <- !pred]; + end + + + + + + use import list.List + use import list.Length + use import list.NthNoOpt + + + + let rec play_cards (input: list int) (s: state) : unit + requires { inv s } + variant { input } + writes { s } + ensures { inv s } + ensures { s.num_elts = (old s).num_elts + length input } + ensures { forall i. 0 <= i < (old s).num_elts -> + s.values[i] = (old s).values[i] } + ensures { forall i. (old s).num_elts <= i < s.num_elts -> + s.values[i] = nth (i - (old s).num_elts) input } + = + match input with + | Nil -> () + | Cons c rem -> play_card c s; play_cards rem s + end + + + + + + + + type seq 'a = { seqlen: int; seqval: map int 'a } + + predicate increasing_subsequence (s:seq int) (l:list int) = + 0 <= s.seqlen <= length l && + (* subsequence *) + ((forall i. 0 <= i < s.seqlen -> 0 <= s.seqval[i] < length l) + /\ (forall i,j. 0 <= i < j < s.seqlen -> s.seqval[i] < s.seqval[j])) + (* increasing *) + && (forall i,j. 0 <= i < j < s.seqlen -> + nth s.seqval[i] l < nth s.seqval[j] l) + + + + + + + use import PigeonHole + + + + + + + + + let play_game (input: list int) : state + ensures { exists s: seq int. s.seqlen = result.num_stacks /\ + increasing_subsequence s input + } + ensures { forall s: seq int. + increasing_subsequence s input -> s.seqlen <= result.num_stacks + } + = let s = { + num_elts = 0; + values = Const.const (-1) ; + num_stacks = 0; + stack_sizes = Const.const 0; + stacks = Const.const (Const.const (-1)); + positions = Const.const (-1,-1); + preds = Const.const (-1); + } + in + play_cards input s; + (** + + This is ghost code to build an increasing subsequence of maximal length + + *) + let ns = s.num_stacks in + if ns = 0 then + begin + assert { input = Nil }; + let seq = { seqlen = 0 ; seqval = Const.const (-1) } in + assert { increasing_subsequence seq input }; + s + end + else + let last_stack = s.stacks[ns-1] in + let idx = ref (last_stack[s.stack_sizes[ns-1]-1]) in + let seq = ref (Const.const (-1)) in + for i = ns-1 downto 0 do + invariant { -1 <= !idx < s.num_elts } + invariant { i >= 0 -> !idx >= 0 && + let (is,_) = s.positions[!idx] in is = i } + invariant { i+1 < ns -> !idx < !seq[i+1] } + invariant { 0 <= i < ns-1 -> s.values[!idx] < s.values[!seq[i+1]] } + invariant { forall j. i < j < ns -> 0 <= !seq[j] < s.num_elts } + invariant { forall j,k. i < j < k < ns -> !seq[j] < !seq[k] } + invariant { forall j,k. i < j < k < ns -> + s.values[!seq[j]] < s.values[!seq[k]] + } + 'L: + seq := !seq[i <- !idx]; + idx := s.preds[!idx]; + done; + let sigma = { seqlen = ns ; seqval = !seq } in + assert { forall i. 0 <= i < length input -> nth i input = s.values[i] }; + assert { increasing_subsequence sigma input }; + (** + + These are assertions to prove that no increasing subsequence of + length larger than the number of stacks may exists + + *) + assert { (* non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > s.num_stacks -> + let f = \i:int. + let si = sigma.seqval[i] in + let (stack_i,_) = s.positions[si] in + stack_i + in range f sigma.seqlen s.num_stacks && + not (injective f sigma.seqlen s.num_stacks) + + }; + assert { (* non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > s.num_stacks -> + exists i,j. + 0 <= i < j < sigma.seqlen && + let si = sigma.seqval[i] in + let sj = sigma.seqval[j] in + let (stack_i,_pi) = s.positions[si] in + let (stack_j,_pj) = s.positions[sj] in + stack_i = stack_j + }; + assert { (* contradiction from non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > s.num_stacks -> + forall i,j. + 0 <= i < j < sigma.seqlen -> + let si = sigma.seqval[i] in + let sj = sigma.seqval[j] in + let (stack_i,pi) = s.positions[si] in + let (stack_j,pj) = s.positions[sj] in + stack_i = stack_j -> + si < sj && pi < pj && s.values[si] < s.values[sj] + }; + s + + let test () = + (* the list given in the problem description + 9, 7, 10, 9, 5, 4, and 10 *) + play_game + (Cons 9 (Cons 7 (Cons 10 (Cons 9 (Cons 5 (Cons 4 (Cons 10 Nil))))))) + +end + +(** {2 Gluing abstract version with the original idiomatic code} *) + +module PatienceFull + + use import int.Int + use import PatienceAbstract + + +(** glue between the ghost state and the stacks of cards *) + + use import list.List + use import list.Length + use import list.NthNoOpt + use import map.Map + + predicate glue_stack (s:state) (i:int) (st:list card) = + length st = s.stack_sizes[i] /\ + let stack_i = s.stacks[i] in + forall j. 0 <= i < length st -> + nth j st = s.values[stack_i[j]] + + predicate glue (s:state) (st:list (list card)) = + length st = s.num_stacks /\ + forall i. 0 <= i < length st -> + glue_stack s i (nth i st) + + + + +(** {3 playing a card} *) + + use import list.RevAppend + use import ref.Ref + exception Return + + +(** FIXME: not proved + + let play_card (c:card) (old_stacks : list (list card)) (ghost state:state) : list (list card) + requires { inv state } + requires { glue state old_stacks } + writes { state } + ensures { inv state } + ensures { state.num_elts = (old state).num_elts + 1 } + ensures { state.values = (old state).values[(old state).num_elts <- c] } + ensures { glue state result } + = + let acc = ref Nil in + let rem_stacks = ref old_stacks in + let ghost pred = ref (-1) in + let ghost i = ref 0 in + try + while !rem_stacks <> Nil do + invariant { 0 <= !i <= state.num_stacks } + invariant { if !i = 0 then !pred = -1 else + let stack_im1 = state.stacks[!i-1] in + let stack_im1_size = state.stack_sizes[!i-1] in + let top_stack_im1 = stack_im1[stack_im1_size - 1] in + !pred = top_stack_im1 /\ + c > state.values[!pred] /\ + 0 <= !pred < state.num_elts /\ + let (ps,_pp) = state.positions[!pred] in + ps = !i - 1 + } + invariant { old_stacks = rev_append !acc !rem_stacks } + invariant { + forall j. 0 <= j < !i -> glue_stack state j (nth (!i - j) !acc) + } + invariant { + forall j. !i <= j < state.num_stacks -> + glue_stack state j (nth (j - !i) !rem_stacks) + } + variant { !rem_stacks } + match !rem_stacks with + | Nil -> absurd + | Cons stack remaining_stacks -> + rem_stacks := remaining_stacks; + match stack with + | Nil -> + assert { glue_stack state !i stack }; + absurd + | Cons c' _ -> + if c <= c' then + begin + acc := Cons (Cons c stack) !acc; + raise Return; + end; + let ghost stack_i = state.stacks[!i] in + let ghost stack_i_size = state.stack_sizes[!i] in + let ghost top_stack_i = stack_i[stack_i_size - 1] in + assert { 0 <= top_stack_i < state.num_elts }; + assert { let (is,ip) = state.positions[top_stack_i] in + 0 <= is < state.num_stacks && + 0 <= ip < state.stack_sizes[is] && + state.stacks[is][ip] = top_stack_i && + is = !i /\ ip = stack_i_size - 1 + }; + i := !i + 1; + acc := Cons stack !acc; + pred := top_stack_i + end + end + done; + (* we add a new stack *) + let ghost idx = state.num_elts in + let ghost i = state.num_stacks in + let ghost stack_i = state.stacks[i] in + let ghost new_stack_i = stack_i[0 <- idx] in + state.num_elts <- idx + 1; + state.values <- state.values[idx <- c]; + state.num_stacks <- state.num_stacks + 1; + state.stack_sizes <- state.stack_sizes[i <- 1]; + state.stacks <- state.stacks[i <- new_stack_i]; + state.positions <- state.positions[idx <- (i,0)]; + state.preds <- state.preds[idx <- !pred]; + (* we put card [c] in a new stack *) + rev_append (Cons (Cons c Nil) !acc) Nil + with Return -> + let ghost stack_i = state.stacks[!i] in + let ghost stack_i_size = state.stack_sizes[!i] in + let ghost top_stack_i = stack_i[stack_i_size - 1] in + assert { c <= state.values[top_stack_i] }; + (* we put c on top of stack i *) + let ghost idx = state.num_elts in + let ghost new_stack_i = stack_i[stack_i_size <- idx] in + state.num_elts <- idx + 1; + state.values <- state.values[idx <- c]; + (* state.num_stacks unchanged *) + state.stack_sizes <- state.stack_sizes[!i <- stack_i_size + 1]; + state.stacks <- state.stacks[!i <- new_stack_i]; + state.positions <- state.positions[idx <- (!i,stack_i_size)]; + state.preds <- state.preds[idx <- !pred]; + (* card is placed on the leftmost stack where its card + value is no greater than the topmost card on that + stack *) + rev_append !acc !rem_stacks + end + +*) + + +(*i a version closer to the original code + let play_card (c:card) (old_stacks : list (list card)) (ghost state:state) : list (list card) + requires { inv state } + requires { glue state old_stacks } + writes { state } + ensures { inv state } + ensures { state.num_elts = (old state).num_elts + 1 } + ensures { state.values = (old state).values[(old state).num_elts <- c] } + ensures { glue state result } + = let i = ref 0 in + let pred = ref (-1) in + let rec push_card (c:card) (st : list (list card)) + (acc : list (list card)) : list (list card) + requires { old_stacks = rev_append acc st } + variant { st } + = + match st with + | Nil -> + (* we put card [c] in a new stack *) + rev_append (Cons (Cons c Nil) acc) Nil + | Cons stack remaining_stacks -> + match stack with + | Nil -> + assert { glue_stack state !i stack }; + absurd + | Cons c' _ -> + if c <= c' then + (* card is placed on the leftmost stack where its card + value is no greater than the topmost card on that + stack *) + rev_append (Cons (Cons c stack) acc) remaining_stacks + else + (* try next stack *) + push_card c remaining_stacks (Cons stack acc) + end + end + in + let new_stacks = push_card c old_stacks Nil in + let idx = state.num_elts in + state.num_elts <- idx + 1; + state.values <- state.values[idx <- c]; + new_stacks +*) + + +(** {3 playing cards} *) + + + +(* + + + let rec play_cards (input: list card) (stacks: list (list card)) + (ghost state:state) : list (list card) + requires { inv state } + requires { glue state stacks } + variant { input } + (* writes { state } *) + ensures { inv state } + ensures { state.num_elts = (old state).num_elts + length input } + ensures { forall i. 0 <= i < (old state).num_elts -> + state.values[i] = (old state).values[i] } + ensures { forall i. (old state).num_elts <= i < state.num_elts -> + state.values[i] = nth (i - (old state).num_elts) input } + ensures { glue state result } + = + match input with + | Nil -> stacks + | Cons c rem -> + let stacks' = play_card c stacks state in + play_cards rem stacks' state + end + +*) + + + + + + +(** {3 playing a whole game} *) + +(* + + type seq 'a = { seqlen: int; seqval: map int 'a } + (** a sequence is defined by a length and a mapping *) + + (** definition of an increasing sub-sequence of a list of card *) + predicate increasing_subsequence (sigma:seq int) (l:list card) = + 0 <= sigma.seqlen <= length l + (** the length of [sigma] is at most the number of cards *) + && (forall i. 0 <= i < sigma.seqlen -> 0 <= sigma.seqval[i] < length l) + (** [sigma] maps indexes to valid indexes in the card list *) + && (forall i,j. 0 <= i < j < sigma.seqlen -> sigma.seqval[i] < sigma.seqval[j]) + (** [sigma] is an increasing sequence of indexes *) + && (forall i,j. 0 <= i < j < sigma.seqlen -> + nth sigma.seqval[i] l < nth sigma.seqval[j] l) + (** the card values denoted by [sigma] are increasing *) + + use import PigeonHole + + let play_game (input: list card) : list (list card) + requires { length input > 0 } + ensures { exists sigma: seq int. + sigma.seqlen = length result /\ + increasing_subsequence sigma input + } + ensures { forall sigma: seq int. + increasing_subsequence sigma input -> + sigma.seqlen <= length result + } + = let ghost state = { + num_elts = 0; + values = Const.const (-1) ; + num_stacks = 0; + stack_sizes = Const.const 0; + stacks = Const.const (Const.const (-1)); + positions = Const.const (-1,-1); + preds = Const.const (-1); + } + in + let final_stacks = play_cards input Nil state in + assert { forall i. 0 <= i < length input -> nth i input = state.values[i] }; + (** + + This is ghost code to build an increasing subsequence of maximal length + + *) + let ghost ns = state.num_stacks in + let ghost _sigma = + if ns = 0 then + begin + assert { input = Nil }; + absurd +(* + TODO: if input is empty, we may be able to prove that: + let sigma = { seqlen = 0 ; seqval = Const.const (-1) } in + assert { increasing_subsequence sigma input }; + sigma +*) + end + else + let ghost last_stack = state.stacks[ns-1] in + let ghost idx = ref (last_stack[state.stack_sizes[ns-1]-1]) in + let ghost seq = ref (Const.const (-1)) in + for i = ns-1 downto 0 do + invariant { -1 <= !idx < state.num_elts } + invariant { i >= 0 -> !idx >= 0 && + let (is,_) = state.positions[!idx] in is = i } + invariant { i+1 < ns -> !idx < !seq[i+1] } + invariant { 0 <= i < ns-1 -> state.values[!idx] < state.values[!seq[i+1]] } + invariant { forall j. i < j < ns -> 0 <= !seq[j] < state.num_elts } + invariant { forall j,k. i < j < k < ns -> !seq[j] < !seq[k] } + invariant { forall j,k. i < j < k < ns -> + state.values[!seq[j]] < state.values[!seq[k]] + } + 'L: + seq := !seq[i <- !idx]; + idx := state.preds[!idx]; + done; + let ghost sigma = { seqlen = ns ; seqval = !seq } in + assert { increasing_subsequence sigma input }; + (** + + These are assertions to prove that no increasing subsequence of + length larger than the number of stacks may exists + + *) + assert { (* non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > state.num_stacks -> + let f = \i:int. + let si = sigma.seqval[i] in + let (stack_i,_) = state.positions[si] in + stack_i + in range f sigma.seqlen state.num_stacks && + not (injective f sigma.seqlen state.num_stacks) + }; + assert { (* non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > state.num_stacks -> + exists i,j. + 0 <= i < j < sigma.seqlen && + let si = sigma.seqval[i] in + let sj = sigma.seqval[j] in + let (stack_i,_pi) = state.positions[si] in + let (stack_j,_pj) = state.positions[sj] in + stack_i = stack_j + }; + assert { (* contradiction from non-injectivity *) + forall sigma: seq int. + increasing_subsequence sigma input /\ sigma.seqlen > state.num_stacks -> + forall i,j. + 0 <= i < j < sigma.seqlen -> + let si = sigma.seqval[i] in + let sj = sigma.seqval[j] in + let (stack_i,pi) = state.positions[si] in + let (stack_j,pj) = state.positions[sj] in + stack_i = stack_j -> + si < sj && pi < pj && state.values[si] < state.values[sj] + }; + sigma + in + final_stacks + +*) + +end diff --git a/examples/patience/why3session.xml b/examples/patience/why3session.xml new file mode 100644 index 000000000..fa0835aa1 --- /dev/null +++ b/examples/patience/why3session.xml @@ -0,0 +1,526 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/patience/why3shapes.gz b/examples/patience/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..7b95ae9bf7ab84b117bf171605a0e49e8d9e119d GIT binary patch literal 13880 zcmZwNV~{4nwlM0pZQHhO+qS2B+U}mVZQGo-ZQHi>ws~it@4FFqpSTqjna^5L|0-8y ztc)Uzf&%)V>*v~6I}VRK@x=Qp(uWXE2**JPrIbhx1O\$ekG0H=m4u-GFS%Q99istF+ z`<VZk#MF!Y_Ix3|=sk7-1_`Q6L+9XR=i~GC zb{?YtP^*LA&&THKy~FeVw7fBjc!IjACG z!%gZsA;p1R@iD0{3PAjwkM@L6(&jDD&EL}e^{)Nx-JKL}c*87nNBJ7Hd-c&PSd7@7 z>-3k9TG#&P{KcQ!Y6%!JW4HQ|OdlJS2NC92-r%5%HO=Wn^EhB4Wx\$!Zi\$-N9Z|5Xo zAClkwx&Mgp#\$SKRUtFP_C!NMSq>+>Rg?6D3G2Wk5O9w7BRnb8(#u?zsuzMAc(Jii{ zz&;l9dd(KNunJD+lG4SaC6vaCdM2z9103nCN}%?v2)P8E|W?ntP z*f%EyT(xZA\$\$i=Vwy4LkS@K2zU`VOz_*&M3)>#EUb8YjqGX#Q&qEKtut\$BSRjjF5`u5M?yzkHoh(Sans-P_8YU%AM^U7 zZQiKs-ACPG2m0_2Yb}`bgtB;{<@`sVm~At{FoY9RFm;k!#+?6Vwd6#2RBcft^PawU7l!9VVsDBsZE%Mm20e9Bi1B\$ z60XKb=oTZ1\$%PWjeaRxVp zF-8{WNHOq`4sfHWuDOmQ(l_A9AYx6aNO|F?WDRH_QO5c;=hqS+%dHFdE{+p?v`{TK zUNSvGyH#VN6EHgMeQ?SYQI0OzGSDhwC0B`l8dww2xjP\$+Dm2(Bf1*k7ly2IJR(NE% zlQbwBO{~~vTpvFWmg%||6+-N`x+#>\$tIdR@;a7sCx^MobCmr?b5M~>W!nGS0b7@Tw zIl>P-San6{SvV7APslOE?P)Cbwx9(_Dcc8DQqRZP8Pzze(Bgs?44frLh)U^+odBD\$ z9bKTcZH(\$)YkHtno>T?BqQ{M&5|A|Ni7&z>yn%=&kCKL4*)>quFtEq4NnOXNWkMknOyHQWanUlHO#^3K+LK~#g>qL3iGnMqlGt_trEy=QkdDSh*U0*GT23| zF_NZO6MVEu*g}7gBH;+b)sx|~E3d<;l#|Pun_?u#Cc4##_`xf%L->y7vt~8TqUq3% zSUc^+(}6*=Im%hSR(cU%EZ122wLEpL\$*z7lnk%YubW`;TQ7%jkw>2g}UlgJD!K)D+sk(1yhtEJ%L49M zxb|3>W%1^7BY>EJVOOw#&>w%{>h7w@LTidZhz6JLND\${7=+H2B\$C8OjDYlC~(>Lpa z%_gC&1T`4Y5*D*&q`(&F*K1_ebuK^CKcSTjS(BS^fF*;QP%lbwfs(BcffdEsEC0y# z_C^u7hcCRo1th!rV)7rNM6=M@\$oHN6cB+-faDs#Oj>CA^f2jKZw}UzBpzsIRm6 z*wAc(Yp5cD`@Ay@fUBMW&h-t3Pho&0^Vh~efBZ-tT_du\$RRKdfGITW>iu z`N9Vmc3rZKg7UJ*I>XkFi8KV9fhux}+tk{pqSF9b27BH_c7@F-;WOc1hC@sn7Q{Uf zD0_ZR1||s-B!c#R6)9?hMgQD3qEDm<@^23cVt8~%Ks zifm zs>0F\$Rf{r%=cqX~-xb!7AEQeeM`j!E={R7ON|#1{_n\$^5m~EgM6Mmnr--(R=+}_zI zC=DZ-0^H7`{C;wNzCza!ZmFc~vha{Xepz#DzJBX1zJ7qNwtRcruQD7v>+gHjrEk5l z5QKCA%DTDL;jCxPB|^XjNIbUTDJF;~mY|`%)EktOW`QeteB1k5P{-~Zft!MEo\$?

M5J3Mu5H=6r4_o&@?dGcOVB%K&E;Q zQ%Ow|2x*K){>c)GQVNOI1@LFbMc~J7B{R>lPP7UA)MIN(Kv^kD7KdoHHI~jUv!PBu zUQ`#;-;4IvY6S{IpJ4rp{!#Eq8qODX^krx8j1ICaIfHol)ayk8Lhpaxpq(JfRvQkxnG18DhN5oPxHm=5dhB~M@ z@PGyDbJ\$\$1fOV(^dowb6UP#s+m<0RS`AuDK-o>~fmY|7;Y4ba> zMuVL8l0przL2TXg>ynNbh24#FIhM*OLmc)At&EtzcM-~xdMANH*->0GHY5bvRmsjK z\$4r_nX=6)zCq(aXPVr6{h`t4x1a%)pEeB=`_FT<&Jou{NrFp}{ex+R(XAs0j&N`cJ zFjeWG^u&v-Q^HIqK#\$aK59vXAgLr13Cq(QgMD+i;&yWmF(95fF?Fuz0tfNaA?)!X* z5VCDFUJMR\$b990Kc)Q&sX1mEee;1CC{{ATxNDgaww=(=euRB@H`ZHBCeoPXYKxl7; zSTQE^WwrbH6t{bLiI@gRhs2T=3mO1K{cffJ+(_HoSS+5a2LVcwvjgr zU-u>1>\$tpseGUF}@+_SZohMu@UoUAft}EJVYdVR!CaUh*ORdE3eSm8VF3g@}OotFN zY|I10N\$-o@43_tufSQ@J(_G{?FBXJ!mcxS;5ygd`2jz6 z{`Pw-B-~9?)BNrGW=5GS7zX%pOpKcadVIsnCo2W9kBT12eLwDF6pe)?A|biW=%p0t>Ss=g@CNYF4Jh|~bp%FG>&?NYg7e\$~L~O8hnA z4J2X?w!_?a7\$-#1vw8`W-Xg0P`jNstlf{jYwnIb-mtKCWoA4IcMw6e^f>KSlw7kbU z90?Jx&jI4nfZZJW3Fzl?{)oF`y`hFnauLShTG>>{_VBG\$m@QohoBRvBNgjw4HGZY` z@d~F+Lv1##TN_V!g2Q6XKaOAL>{5ExKe_WAnVVmX%DmSx_2(HjlCdK5KGa(jW7LnSJs2>19oWcwPp>V7K0XToRV|i0x7N+xhS{xhSz^((QOI- zJ!O<-%t2%e>AQlUu_E0vaC~4a=2j|N8Z<932+CD{e6+VzJ7_;j`R9(Yn(n>kCC|X% z-oiYl\$?rxtp{8;yo=-li^Sa^Ud4+|H7LG@E(#Y6X*Q6{B-Z|u)pUIo1R0se1vL6S) z6r\$Pa?FgGhd%32x!h+3\$-lbaWi3%2HPpFmL#3k_59Db|n4fo6R@38prlK>lMzg_On zQ69F1qIo`ew8F\$tmUE>K=hR8HPSnk@QubFolkS9-83+Tps~F4;xTP{`ReBP2DJ;{6 zwdOb^8ljSp&^_?*f8mod=%C-0-s4~Z*_fEy#AA;tfZ1C;s@us}eq%l*CSx&)?TAV6g\$cg?TUOo\$Kh8imrAQlp~d!&Lvt<2-&u3DZ`6Q zs|\$1k9{Ezxt>4#;7F4-&9yFU7diD_s=HeEl1AJpQaDyf6KJl~;+>NjoTh#eN5WL45 z_eGTF*WR3BOJTs^NNKiZ7JW&`9SH z{osk0*6ir{L&-iMD&s0yokUT0sjRRvzfaP@eeitpmYQNkrnp\$>*4eZ*uR}&_D=fRB zJBdjZP-~iG*O\$;q6=1I!`{7j&AM9i}A2nk?N1Oadu^Pw}pwNE8-h5mggp&V7u+u4> zgnCs7b_y)ap&B^6xVEWF+o5oITLe}Dx74RVFnfv5\$?&2IqO2UaQ?!>J{V9~(cQzKX zM4~L66b;dJzXfi?4b4a0BLi)J2`f{Q5=jT\$ zNg_M&JeJ5LnF@xdjq)s!D)wTCKOwKZe5kM)%|Y;(S6Ke z\$I@|o&bEHj;sdn`Xw5}jrIN~W7~CuZ=nd\$la@V*yt|REyvuV%lu0_no&lf5M;M!nk zvQ}VA>L9bUmbe|\$s)1mAvb zC6Je~D1q{FbJcafync@*c16;Sd(YcZYKPU%Q}RBv!sv!sd z|FWk@r)k;tCrGqei&^bL`1hr>+lyi&p5HaWBNbd?zGH4)J;M>;r`}Q0_v;24_G^I{F=RwB5f^\$A1;~qn&wfB*n3X!p`iIzu-J`(tkUL8XoAQ9JtZE4jO zk&;-aR+sS|@?&F359zIOuDN0}>cvj5TaD)92f4v*F#j)ndNd7+6LSHnCWBv(x!~Ft zMmA!#Y3NkXBk-A)Y3*Yxl76%&B`#^W+C{^KvS3XZQ3VzJH)cna=*VU=U^h0YP%)LM zlkk9RL(m5FjHu\$YvX_YCS_0o{-ff4hzqql7xoRC*i?Bx7M;v4D&;Je6)A;`rIO>6> z@x|JHK8~`(L6)f0GgBYB*6+1T3)?`YLO1(~;gYiI{Bn|;ed3pDCH}USEXiH`O^&l? z5*ozfBb#h&C\$c4nJwh?G7QB{VZzmEhAO07bnS=QMWQ4KdR3jt^f|I5oX;@&Gku7T;u^6-8^ACmvE+%7iCAJvyjBt!DdK_!cq|baHO_CL>3eeC&B_XPDEyy8ULEk zA2m)+!~&DS4W-=ohXpl|m8CW;yK;)I+svYM|HZM?cM*Jzrjmh{bCSk45XmVxV|h)QX6;^a0yvU*ygwQ z{=e|uSU1sW=Br^WO^KSJn1FnMC!YY5P>h)N+c&14bKn!5mp}Ch@{{n+zwZb5=fCjN zIOs2evN!-!8gn<#a`{IaltIxF*yZcyH1N\$QqD3pq6VwydvMkN z^?g@_Hni@C_i)9%{F{^d{O\$GfgMm}Vav6b_c^l(?~U{({)A810v* zUb9+^I>j@2A%m}9@u|W(5Y`!jSjFc5mzPXZlSK4EO>hej&IuU\$KKWW~iIZ4C\$2zFU zRw@gl\$*(-to{n3v*j*-fk^Qs~by)u|UcqYrZln`}R4q5_NL}87PK!IJn zfaz0hA(TQrBLBjd*N1TDguGC33E_^tbqsLE-\$sUMujl=Oy-3Rk|NiimXdao28|*O=Vok&^P5kpCIdq5\$eR@5MfL-^Sl zQ`IqT#~Y>njkp~abK*iO2q7|l4-FDS\$TJTLDpjvz^5CPt*B6xn+aRC-JywFsgD`gl z`|;2w`yHldB=2TueRd|`S+&plk\$OF{kdj*bwXSycT)e+C3jNdP^=%yh!y@RtlYev` z27!GV7FQ)=Yo@|1W36?-r#%^MKIBmm@gk%3m!b()R6xu<{3Z=;yV_9L8+3>pIq0b0 zx&kdhhKwNi!TtH`;}s#|S83MVBU*?j|7jx}iMc5fBYYuPLa}_P\$7v#fdC`zKW;!(K zv_Hk3Ky0b3>*Cu`+46K^D%i;UZmlUdM1fJ&0MW>|C9jbEHM_-gd;__}>hzp8JPYf< zO?vB(vtn?vnpODFxZRW1qnd?0O3lLk|2a5K!Q0_q<0QOs`f7OfZ4w6}OeOo>f;d{* zywFFpZ(STv^Yr#4W44mT(Rel0qvyfAu3}!0Z5mo~2 z@h--AUNlQ\$UH9t)W)j=AOsTO8t7%f`=~+MY*e5|?W%_V|W>SP=(i=g|aKl-v z7FOjsN|p~3Hm`be1V20^`mSqV6C_w)(ZKtUzHWi;1-wtmDH>(9Jx%x|?9-%nq0Zl9 z*T1&~Rojue_+;=9)hd219*yF*Ox02=KMRp\$cSVZc&+zwb6 zm-XoGFkjt7P}Au8-*cv}9s9Ls%Wh+rTB@3Hi*|7~v=n)|Dm^ySCx+nFUM16&wzU{H zn3cFiKdf}ketNm(KNq1YW9kTcA^nm(kGc`NJj>2AFsAxQ\$?@)?)4Fxs-G6wD1mxWC z;?>k7v*-D}rUElmkRJ1J8pjmLkhf+*zJgiZEm^8 zZk~NC5I56\$@sB5jJDF_M_}BLs5Jjx7tjcooBvDU\$qX9TLqu z&xsIeBX|4Jg3Jil\$3qr)okY%gZ@HJ6C@u4TnTY+W4H5CseB|kbYKLzu`^9H`64#>^7f*PwsN2yL7d0N0IVY zRlq8oKu75nXuAq?*\$psjYvv=*YdYScxumzMB6r=(slRk*_<4MNZmQ?HyTh`Q|I@P`%1ka68a-@guWb;Ja~Aq|Caf7q5e3 z4HJ=?lB4T)54-?)jNyd%fbM~YK#>st3u!v&E#oYg!r=HJ@N~+AfiVWWvpI_<=t#GK z*i!W+*\$%)RnEHz#m6;zO9S;\$JVoY!Ja|<#BwjGqkuuH2(e6_3tG<3?vAzSdM z1hUC<3p#@_6!DjgBvU!BjDTm;(ueV5L5Wp4R4EbSR|d0g@I)H?w>|CVGBQ9r4OE0PSh9l&l|*> zHmuV)xpHjN)g7b9Yv%G?pjdR3Tll>;M3&V8o=&314tSQu8B*kbjajVGBk(o_&gn!# zv^@74PKUdQ#k;A9#W8o1fvRLR6Oe{7bsrO97ZlqTNeyna%_ulx8XDL z\$XaLo*QzS75UxPcj_oS8zR;ok))PFEJthw3wUf0WVhb|i4XxSkI=l&Z%p!EWCh-Dq zm3E_y0uKa+gVW=U+!0vk+^Z+l%e0lxeb=R1F@dmM4t6Xe~v#o8)M4p*^EIPg62wm!(@\$LsTA>poz zu6e#^wwUp\$t=mc)VCloims)i%\$hr|)n(>%5NY~TfJ@^5b35^Q~FFU?M9kD`N;KdG6 zTABlaemCK+s@PC{ZViS8ol*B+\$d?}Ie`8+=*!Ki2hC1SvSryf=lhP5FD35DkmmC#H zm})cv9uFU\$QbP`bTOqdyetY*_{};Zw_c;zDuyWKEi082Aml{eZ_b@@uB75Tznap%3(XoJdjZ#Z4ed7|hweR?y+z&u zlj{Ee+SSjQ*25P7?FlzfwJxj?H4J|{U*nE9i--?mp*8pEvhQ|` z(|UBi\$M;2tc\$Im_-3V`ZcP(W1Eg)((W>*%wJRqkyYjww1?`rh6Yv8tfG@9A@HQ}yP zCBGb61Q{I+bISIT%2*{WDu26USK5)bXXR%S\$nXEJMg33H`V*MGOGZipF9t)NW4ggB zPt1ZJ(@0&E%RUund4(3qb*L2_{PGZhgB?d7AdCpXkM(FY7xZ6vEqnwD2QC2fsG(;M z)`3;vs!dwfkkTrHj3d%ocGTw>Jgb4R3l99`nEU)aM~LvQ-~4a*Iu8x{wxHv|dkhQu z{yjHZV?HSSL+L&@YY2T4-WnP@1ovW;biV;zX9{P5K5fd+Ut_a6J55i?X>#3=2J}>1 zs#%yzf66uY&Z9\$Uduw{_TiqSk{POo%U}Xoh!??OzkR|wkf?gCIO%M{}g+CZV6)QU( zQdVYkWRxMguG8&yrx;APJRQ3UpVs4jfPM%FTr4}I`hfq!EA={%F-{kNczp_jFKCGF zuUblqcOKTz(;m;-)C#4&E^8+;HzMM*V%>V*O)gX%`?`@hs7ONnC! zN@(K0`MT|Gv`Y?}O*%AGD5hSxoeY{)?qBUFlaEXECwlrX{EWqK zP*w!9Q#f9TF2!p}iE%TSIkAnnaz2cAg9Yu@KzXk##SLEtbU{84jCm8?{(srGqND5h+-6oJ=01%m}1eV&G3&0&FPlqflAp4y z2X|<{j0_>J&j~3^eyBg&AYellPoePXUmb^Wja}zOw%@>@Lbj)IO%aT8C;j{2IktIp z^ibmq?=m=N3ic*&2_1jz{3~Ohqdb3Fg\$H!Uaz>uaT!(;esay)M?Sr-0l@(3dr;mX= zWJp!s9z)427feScdbxjx!7Hl-s9}DP@8}0a6!j4ddmV2C`3MJp#*Slc{hyH`hrT>_ z&7H;+eK8&5A\$K6f-BbS^qIkw&)%BxjenbRShl}2#o9TVW4++bZbh&K6h_V5692MCp zGbP5=AKw|GZXti3<mcy?rB>aqvg&e4=H&b`@A-Lk z`FawE=r7nX9|!sC=lRa7f{A(CH!>1bKTQ(>X0lSu<;6NHrD8*w@sRTXsO_LED|psc zAn)N9jA?NtC#k9tgdC8RD!|Fbv*yBMvRJQMpEV-eErw<(Wi_t3?D6k=@AL!9{P>~\$ z(tVSsHV2QNygrd*VSi4Kg3 zw&9kbj5PJlT}4}*_^T\$rUx^G4tqL+1m24Y4hxnlu#!qq^*J?R;Ydd^#)1wXcgvk6F zpO*y`S7|u-FCy%TV\$REQBjHr9C<+QB+muon=kSD6w{f1(y)fI4Y zb}gHXr6Jym9Mn@^nJ3O|g4*Pm0IXC#=>hO_5H!OtATpkK*d(;0!j5CrU~oH%B{gF^ zs>+ha1tUDOf@yhESK6\$}wyMb_AJ!Rj(t?ibMmaUG*3tlYFJa\$F2 zEwGt(GHNdB*+=ID{lc0kI3ykzg{!hR4;I zaW(_=rb?5%ra74F1Y+oB|DJN\$3dB4(yGa^ds7Y@eGy*PAC2KM{wpug ztXbYK=g1(fTM7-Hd-B*&jT2q{C%^@|_EA<(B|n0oI`mwuNWzs@BkWpl9y^I;^G^6D z3uoag+o\$CtA%Vb%NE9JzX5!s{{;B)8bhsxY81?_zoHxBSUkCbJYVxn;m_A~h{dm{f z&|#kj56CH1{=DV\$ygTun*BF+LQ!8AzV>>7bRHbatMxkMr^v~MBtoKxJ2Pe4m(?33Y zDVOEHM{_9SuX0v>GHrJC(AtKpW;I06u\$WNTn3x%RM7fPBD7@%O+a@>Px1;5MELUN^1GDumJ;?QCDR9+F7w-^V|CUUo z)B1&f4s=e`!NZOmJ-TstKpN;o;f?3Azcs&UZW^k8n>*Oi`?qKI8lZQd)6>W^j_s6P zVFpE*?+-F}X6D+A`c7C2f0pjnjqg4xH?MaTl|TE^2bI<;kp=@a956&?QiJc(Y2A#? zZB@9!_`MBULj(>|6>lxN4TzGck?-apFKtw-X+na8XiEc4fKkbQ{#51}GIV67%H{is z)y@a1ds{h zj&qNJ=pRy=NRF5>|HM*~)+IayfvAW?MC{&S)HQRkIz%wE&8u`-U501J zYdVJJ&~3+SO5>o}Gsb^?U4pbP|DL-#76w!uaaiWBdm7q06=c30LpXWYp5fM3i4VH6 zqoC2Jw%6u@A8KdV_O1gWcxHL&8K*iw9|pP>ZH#x02?1T5TMu?u3{9VH>)fR2!>HIL zj2FwYIa!gIBCetm4~S8;Y22jF{lQ1AREmdLJtI}=W\$MFQJrl;p253_oM?{g%3c|)O zPm>`Ao}cHB7gK%s{#=nv-(OcrZ(\$#XO_MTH<^V}3QWek`2CnmN1u|}|CT?b19; zLSS;HwtO2nB1&{aATp!Va!h;U?e3`ivcal#(r4!0lG9?iJS{t|h_kXq{8\$r;b5dW| zyG{^t+ad-Uu^5*Wv\$b\$I>HwLEoJ%cE^iD+Y-Z2xzT?C|(6{__Fz`\$BG*\$g<`aenNR zaGKQA5?65&#\$S5Z(zVw@FxPDf_cX(6DN9_DPo|3Qt4qVRdWnJiU_=AV@K{(DbZ#y1;\$OmIx=kWe392XMxS4NQPZC6vfY8 zgmTUrXDY&VpXGoJ6X^8(_jSmAN%N+~`L`%L-Za#rd76AgPDWZN7QKSf1_JXJL0J0n zIemkK<^m{_gKHt1*h%@+NTzP@G83ayf~F{4kLuq&x*?!MD~5jOO4D!wih;KyZrNoz zjCAS6#ZaaV@>)N=z4=AthqU9@es+Rik*fFDF+EM7K01GFo_F9\$MQ;<\$@yEd#W@lKb?;yCjVe4Hk_Qj+b2;#6{>i>bS}#7zRzL z>Uu79!?X\$zt`3kZ(1E&3Uue9oCZCvC!K`yej}kS5DxV{-_QPBzfXdV^^= zv4GB=BJ6T3(gfX9lzFkv_!_A@BlB=JTw_cO3!_F%m?zTb1(aq+ZD_&3>`{+-_nIm! z-Vbn\$mHEjdgKzB1?V3f;u#y2kQ*nk`n@n=e_Tf6JO1f+~7M?#YaGa`~{n@r;m5lOk z+ZSY9zr_EfyQ+L\$1}e}nl)szbLv~+qYQ\$#Jzs5w!`k5X`yP%NP;A;DZ95>)%w<}Yo z0HMA9!KraYDT-03WU#Jg36\$ljK-gG4BZJs2QGiM0E~S><;zn9320>!^*k{v5nbj{_ zJvm>8Nu{RMvW<*pA48tz(pD6@Dt!MeKbcw5h*EN@BzMqksNSPs4^hL;E_Dsje27XN z\$fgaH&C*P6+OSLVzdXX|I;U0B=Q=;s88t>c9FJ\$%qxF&|U1SXgr=\$aiGG6Xwux@ms zy_qaTskLc50QBTfGZ52x-~NX1S zCJp{g%v=~VyETuKV-{fJUboxx1*l!R_MrLPpB@Zz27khTt#O@PT5I2Et|_Q~VPVy` zZYL57NmLd+qJaU;947b7eCm8d*yeITYy7L;u!~6(-&e>CEu@T7VL5O<#GMVc-)w7_G-`k&Cbe>uEIe zOh8Knbw\$^q3|(e7xW3EHbjw#U^v-hKYz7exligBU3M?b_pJan{G_-`FaTF+3W}s_u zq;6e?mRUwR*e8f{RVj&X8ig!%\$Bo*^#b\$L!FGuz4!v7Q9I;n3#69*+xlOCI)L@3jw zhL9nO)aTOl45H~LCQcF}M7\$x8NtE@0I4fJv5YL}AfsKNd1bR!STaiHhJJT zR3p^l!wzS)V=CY-J~uIMdu*iF=A_Nm&Fy39;HTAz2FaPz6CSd=ZlNx26)GREgNYZc zZI_Naf9Z7z8{6jQJX@a9ts)FMaQ%|2S{!ltYGUs8+el}~rhW z;tNNo_ELKspdyA9i6qEg^S(|9bz)ndhXQ}at1if%8vrpY6lG}yKienH2MYBc?{yBb zil1Xurl4|M{+`KrR+N&_gnB=b(VXm|#Kui==t*I`@nuevRFX@)Br2k5vB+<0@EF=&afmrMb%~ zv^wCTdExxgpq%se{ytA0+B^b#*_GzHh3Kd};M0AH*+#W*;h)b#M)b=Bq-D};EuIZq z|2d+{PW=+`QC|W=EjM}E>o`S)q`ca+7\$ur(woSEv{2IAq@d?m(Wa%Vyey9FJf#|Jr!_7zD{F1g1UpLv1zr1ji|a0`Pue zob749{U+`-I<<-cwV#M8;T-d*GyLLh>hrO&qvrb7(#&7g&8~G=)34(I-*QsZ&){Xd zbT7P-jxxm+d2\$*p#rE6M%6P{xaemCB0ebwP+*jA^=B\$B*_iSlbk?;2rb&x\$SL5wWTay9F{DVqWQP#>c%|6a+~_i_S~ z7Aj0ZcQv+Qx1Qw?Bf;h=mEsPB=-#e56WH9y1lu+%7##`94M>oC?0D9S*naE_H;27Mnxro%~- z\$l6T#n8BHUYfrc8L}6o0XG04zQI|PO*NRlPECy~~LSuf!PHa8%NxLXU&c4xnIJ^OU zV{FBWv{MWhyD-Ksg`ZCqv&>rDGaChKjj{;(0Awh4}gMp@o lao`iH15^C%?%|oX)6@BZwCn\$RH~9nUwM(P&1OW>4{{R?%Gamo| literal 0 HcmV?d00001 -- GitLab