# L'echantillon embarque (stratifie, graine 42) : 30 Dafny + 12 Lean.
# Le benchmark complet fait 16k fichiers ; on embarque les specs tirees.
SAMPLE_DAFNY = ['DA0121', 'DA0026', 'DA0298', 'DA0265', 'DA0240', 'DA0150', 'DT0107', 'DT0634', 'DT0092', 'DT0495', 'DT0034', 'DT0030', 'DD0075', 'DD0168', 'DD0199', 'DD0606', 'DD0723', 'DD0037', 'DJ0081', 'DJ0140', 'DJ0087', 'DJ0147', 'DH0087', 'DH0002', 'DH0050', 'DH0131', 'DV0128', 'DV0108', 'DV0064', 'DV0085']
SAMPLE_LEAN = ['LA0345', 'LA0104', 'LA0094', 'LD0424', 'LD0073', 'LD0373', 'LJ0088', 'LJ0155', 'LV0084', 'LV0013', 'LB0046', 'LS0029']
SPECS = json.loads('{"DA0121": "// <vc-preamble>\\npredicate ValidInput(x: int, y: int, z: int)\\n{\\n x >= 0 && y >= 0 && z > 0\\n}\\n\\nfunction MaxCoconuts(x: int, y: int, z: int): int\\n requires ValidInput(x, y, z)\\n{\\n (x + y) / z\\n}\\n\\nfunction MinExchange(x: int, y: int, z: int): int\\n requires ValidInput(x, y, z)\\n{\\n var rx := x % z;\\n var ry := y % z;\\n if rx + ry < z then 0\\n else z - if rx > ry then rx else ry\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(x: int, y: int, z: int) returns (coconuts: int, exchange: int)\\n requires ValidInput(x, y, z)\\n ensures coconuts == MaxCoconuts(x, y, z)\\n ensures exchange == MinExchange(x, y, z)\\n ensures coconuts >= x / z + y / z\\n ensures coconuts <= x / z + y / z + 1\\n ensures exchange >= 0 && exchange < z\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DA0026": "// <vc-preamble>\\npredicate ValidInput(l1: int, r1: int, l2: int, r2: int, k: int) {\\n l1 <= r1 && l2 <= r2\\n}\\n\\nfunction IntersectionLeft(l1: int, l2: int): int {\\n if l1 > l2 then l1 else l2\\n}\\n\\nfunction IntersectionRight(r1: int, r2: int): int {\\n if r1 < r2 then r1 else r2\\n}\\n\\nfunction IntersectionSize(l1: int, r1: int, l2: int, r2: int): int {\\n var left := IntersectionLeft(l1, l2);\\n var right := IntersectionRight(r1, r2);\\n if right - left + 1 > 0 then right - left + 1 else 0\\n}\\n\\npredicate KInIntersection(l1: int, r1: int, l2: int, r2: int, k: int) {\\n var left := IntersectionLeft(l1, l2);\\n var right := IntersectionRight(r1, r2);\\n left <= k <= right\\n}\\n\\nfunction ExpectedResult(l1: int, r1: int, l2: int, r2: int, k: int): int {\\n var intersection_size := IntersectionSize(l1, r1, l2, r2);\\n if KInIntersection(l1, r1, l2, r2, k) then\\n if intersection_size - 1 > 0 then intersection_size - 1 else 0\\n else\\n intersection_size\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(l1: int, r1: int, l2: int, r2: int, k: int) returns (result: int)\\n requires ValidInput(l1, r1, l2, r2, k)\\n ensures result == ExpectedResult(l1, r1, l2, r2, k)\\n ensures result >= 0\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DA0298": "// <vc-preamble>\\npredicate ValidPermutation(p: seq<int>, n: int)\\n{\\n |p| == n && n >= 1 &&\\n (forall i :: 0 <= i < n ==> 1 <= p[i] <= n) &&\\n (forall i, j :: 0 <= i < j < n ==> p[i] != p[j])\\n}\\n\\nfunction countRecords(s: seq<int>): int\\n ensures countRecords(s) >= 0\\n{\\n if |s| == 0 then 0\\n else 1 + countRecordsFromIndex(s, 1, s[0])\\n}\\n\\nfunction countRecordsAfterRemoval(p: seq<int>, toRemove: int): int\\n requires forall i :: 0 <= i < |p| ==> 1 <= p[i] <= |p|\\n requires forall i, j :: 0 <= i < j < |p| ==> p[i] != p[j]\\n requires toRemove in p\\n{\\n var filtered := seq(|p| - 1, i requires 0 <= i < |p| - 1 => \\n if indexOf(p, toRemove) <= i then p[i + 1] else p[i]);\\n countRecords(filtered)\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(n: int, p: seq<int>) returns (result: int)\\n requires ValidPermutation(p, n)\\n ensures 1 <= result <= n\\n ensures result in p\\n ensures forall x :: x in p ==> countRecordsAfterRemoval(p, result) >= countRecordsAfterRemoval(p, x)\\n ensures forall x :: x in p && countRecordsAfterRemoval(p, x) == countRecordsAfterRemoval(p, result) ==> result <= x\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DA0265": "// <vc-preamble>\\npredicate ValidInput(columns: seq<(int, int)>)\\n{\\n forall i :: 0 <= i < |columns| ==> columns[i].0 > 0 && columns[i].1 > 0\\n}\\n\\nfunction abs(x: int): int\\n{\\n if x >= 0 then x else -x\\n}\\n\\nfunction sum_left(columns: seq<(int, int)>): int\\n{\\n if |columns| == 0 then 0\\n else columns[0].0 + sum_left(columns[1..])\\n}\\n\\nfunction sum_right(columns: seq<(int, int)>): int\\n{\\n if |columns| == 0 then 0\\n else columns[0].1 + sum_right(columns[1..])\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(columns: seq<(int, int)>) returns (result: int)\\n requires ValidInput(columns)\\n ensures 0 <= result <= |columns|\\n ensures var L := sum_left(columns);\\n var R := sum_right(columns);\\n var original_beauty := abs(L - R);\\n if result == 0 then\\n forall i :: 0 <= i < |columns| ==> \\n var new_L := L - columns[i].0 + columns[i].1;\\n var new_R := R - columns[i].1 + columns[i].0;\\n abs(new_L - new_R) <= original_beauty\\n else\\n 1 <= result <= |columns| &&\\n var best_idx := result - 1;\\n var best_L := L - columns[best_idx].0 + columns[best_idx].1;\\n var best_R := R - columns[best_idx].1 + columns[best_idx].0;\\n var best_beauty := abs(best_L - best_R);\\n best_beauty > original_beauty &&\\n forall i :: 0 <= i < |columns| ==> \\n var new_L := L - columns[i].0 + columns[i].1;\\n var new_R := R - columns[i].1 + columns[i].0;\\n abs(new_L - new_R) <= best_beauty\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DA0240": "// <vc-preamble>\\nfunction gcd(a: int, b: int): int\\n requires a > 0 && b >= 0\\n decreases b\\n{\\n if b == 0 then a else gcd(b, a % b)\\n}\\n\\npredicate ValidInput(r: int, b: int, k: int)\\n{\\n r > 0 && b > 0 && k > 0\\n}\\n\\nfunction MaxConsecutiveSameColor(r: int, b: int): int\\n requires r > 0 && b > 0\\n{\\n var a := if r <= b then r else b;\\n var b_val := if r <= b then b else r;\\n var n := gcd(a, b_val);\\n -((n - b_val) / a)\\n}\\n\\npredicate CanAvoidConsecutive(r: int, b: int, k: int)\\n requires ValidInput(r, b, k)\\n{\\n MaxConsecutiveSameColor(r, b) < k\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(r: int, b: int, k: int) returns (result: string)\\n requires ValidInput(r, b, k)\\n ensures result == (if CanAvoidConsecutive(r, b, k) then \\"OBEY\\" else \\"REBEL\\")\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DA0150": "// <vc-preamble>\\npredicate ValidInput(a: int, b: int, c: int, d: int) {\\n a > 0 && b > 0 && c > 0 && d > 0\\n}\\n\\npredicate IsValidFractionString(s: string, num: int, den: int) {\\n num >= 0 && den > 0 && \\n gcd(num, den) == 1 &&\\n s == intToString(num) + \\"/\\" + intToString(den)\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod solve(a: int, b: int, c: int, d: int) returns (result: string)\\n requires ValidInput(a, b, c, d)\\n ensures a * d == b * c ==> result == \\"0/1\\"\\n ensures a * d > b * c ==> exists numerator, denominator :: \\n numerator > 0 && denominator > 0 && \\n gcd(numerator, denominator) == 1 &&\\n result == intToString(numerator) + \\"/\\" + intToString(denominator) &&\\n numerator * a * d == (a * d - b * c) * denominator\\n ensures a * d < b * c ==> exists numerator, denominator :: \\n numerator > 0 && denominator > 0 && \\n gcd(numerator, denominator) == 1 &&\\n result == intToString(numerator) + \\"/\\" + intToString(denominator) &&\\n numerator * b * c == (b * c - a * d) * denominator\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0107": "// <vc-preamble>\\nLooking at the compilation error, the issue is that the `Ln` function is marked as `:opaque` but has no body, making it impossible to compile. I need to provide a body for this function to enable compilation.\\n\\nHere\'s the corrected Dafny code:\\n\\n\\n\\n// Abstract function for natural logarithm\\nfunction {:opaque} Ln(x: real): real\\n requires x > 0.0\\n{\\n 0.0 // Placeholder implementation for compilation\\n}\\n\\n// Method to get Euler\'s constant e with mathematical properties\\n// Helper function for absolute value of real numbers\\nfunction {:opaque} Abs(x: real): real\\n{\\n if x >= 0.0 then x else -x\\n}\\n\\nThe key change is adding a placeholder body `{ 0.0 }` to the `Ln` function. This minimal implementation allows the code to compile while preserving all the original specifications and comments.\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod GetEulersConstant() returns (e: real)\\n ensures 2.718 < e < 2.719\\n // Mathematical property: e is approximately 2.718281828459045 (NumPy\'s precision)\\n ensures Abs(e - 2.718281828459045) < 0.000000000000001\\n // Mathematical property: e is positive\\n ensures e > 0.0\\n // Mathematical property: e is greater than 2 but less than 3\\n ensures 2.0 < e < 3.0\\n // Mathematical property: More precise bounds based on known rational approximations\\n // e is between 2.71828182 and 2.71828183\\n ensures 2.71828182 < e < 2.71828183\\n // Mathematical property: e > 5/2 and e < 11/4 (classical rational bounds)\\n ensures e > 2.5 && e < 2.75\\n // Mathematical property: e is greater than approximation from limit definition\\n // This approximates the limit definition of e = lim(n→∞) (1 + 1/n)^n\\n ensures e > 2.71828\\n // Fundamental mathematical property: ln(e) = 1 (defining property of Euler\'s constant)\\n ensures Abs(Ln(e) - 1.0) < 0.000000000000001\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0634": "// <vc-preamble>\\nHere\'s the corrected Dafny code with the trigger issue fixed:\\n\\n\\n\\n// Helper predicate: checks if pattern occurs at specific position in string\\npredicate OccursAt(s: string, pattern: string, pos: nat)\\n{\\n pos + |pattern| <= |s| && s[pos..pos + |pattern|] == pattern\\n}\\n\\n// Helper predicate: checks if positions represent non-overlapping occurrences\\npredicate NonOverlappingOccurrences(s: string, pattern: string, positions: seq<nat>)\\n{\\n (forall i :: 0 <= i < |positions| ==> OccursAt(s, pattern, positions[i])) &&\\n (forall i, j :: 0 <= i < j < |positions| ==> positions[i] < positions[j]) &&\\n (forall i, j :: 0 <= i < j < |positions| ==> positions[i] + |pattern| <= positions[j])\\n}\\n\\n// Helper predicate: checks if positions represent all possible non-overlapping occurrences\\npredicate AllNonOverlappingOccurrences(s: string, pattern: string, positions: seq<nat>)\\n{\\n NonOverlappingOccurrences(s, pattern, positions) &&\\n (forall pos :: 0 <= pos <= |s| - |pattern| && OccursAt(s, pattern, pos) ==>\\n exists i :: 0 <= i < |positions| && \\n (positions[i] <= pos < positions[i] + |pattern| || pos == positions[i]))\\n}\\n\\n// Helper function: performs string replacement at given positions\\nfunction ReplaceAtPositions(s: string, pattern: string, replacement: string, positions: seq<nat>): string\\n requires NonOverlappingOccurrences(s, pattern, positions)\\n ensures |ReplaceAtPositions(s, pattern, replacement, positions)| >= 0\\n{\\n if |positions| == 0 then s\\n else if |pattern| == 0 then s\\n else\\n var pos := positions[0];\\n var before := s[..pos];\\n var after := s[pos + |pattern|..];\\n var remaining_positions := seq(|positions| - 1, i requires 0 <= i < |positions| - 1 => positions[i + 1] - |pattern| + |replacement|);\\n before + replacement + ReplaceAtPositions(after, pattern, replacement, remaining_positions)\\n}\\nThe only change made was adding the explicit trigger `{:trigger NonOverlappingOccurrences(a[i], oldSeq[i], positions)}` to the quantifier on line 59. This tells Dafny to use the `NonOverlappingOccurrences` predicate as a trigger for instantiating this quantifier, which resolves the warning about not finding a trigger.\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod Replace(a: seq<string>, oldSeq: seq<string>, replacement: seq<string>, count: seq<int>) \\n returns (result: seq<string>)\\n requires |a| == |oldSeq| == |replacement| == |count|\\n requires forall i :: 0 <= i < |a| ==> count[i] == 0 || |oldSeq[i]| > 0\\n ensures |result| == |a|\\n ensures forall i :: 0 <= i < |a| ==>\\n // Zero count behavior: if count is 0, no replacements occur\\n (count[i] == 0 ==> result[i] == a[i]) &&\\n \\n // Identity property: if oldSeq doesn\'t occur, result equals original\\n ((forall pos :: 0 <= pos <= |a[i]| - |oldSeq[i]| ==> !OccursAt(a[i], oldSeq[i], pos)) ==>\\n result[i] == a[i]) &&\\n \\n // Replacement property: result is formed by valid replacements\\n (exists num_replacements: nat, positions: seq<nat> :: {:trigger NonOverlappingOccurrences(a[i], oldSeq[i], positions)}\\n |positions| == num_replacements &&\\n NonOverlappingOccurrences(a[i], oldSeq[i], positions) &&\\n \\n // Count limiting: if count >= 0, at most count replacements\\n (count[i] >= 0 ==> num_replacements <= count[i]) &&\\n \\n // Complete replacement: if count < 0, all occurrences replaced\\n (count[i] < 0 ==> AllNonOverlappingOccurrences(a[i], oldSeq[i], positions)) &&\\n \\n // If count >= 0, we take first min(count, total_occurrences) positions\\n (count[i] >= 0 ==> \\n exists all_positions: seq<nat> ::\\n AllNonOverlappingOccurrences(a[i], oldSeq[i], all_positions) &&\\n num_replacements == (if count[i] <= |all_positions| then count[i] else |all_positions|) &&\\n positions == all_positions[..num_replacements]) &&\\n \\n // Result is the string with replacements applied\\n result[i] == ReplaceAtPositions(a[i], oldSeq[i], replacement[i], positions))\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0092": "// <vc-preamble>\\nLooking at the Dafny compilation errors, the issue is that the quantifiers don\'t have triggers, which Dafny requires for verification. I\'ll add explicit triggers to fix this:\\n\\n\\n\\n// Method representing NumPy\'s False_ boolean constant\\nThe fix adds explicit triggers `{:trigger result || b}` and `{:trigger result && b}` to the quantified expressions to resolve the compilation warnings.\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod False_() returns (result: bool)\\n // The result must be false\\n ensures result == false\\n // False_ is the identity element for logical OR: false || b == b for any boolean b \\n ensures forall b: bool {:trigger result || b} :: result || b == b\\n // False_ is the absorbing element for logical AND: false && b == false for any boolean b\\n ensures forall b: bool {:trigger result && b} :: result && b == false\\n // False_ is the negation of true\\n ensures result == !true\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0495": "// <vc-preamble>\\n// Method to create a Legendre series representation of a straight line\\n// The line is defined as off + scl*x, where off is the y-intercept and scl is the slope\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod legline(off: real, scl: real) returns (result: array<real>)\\n // The result is always a 2-element array containing the Legendre coefficients\\n ensures result.Length == 2\\n // The first coefficient represents the constant term (off)\\n ensures result[0] == off\\n // The second coefficient represents the linear term coefficient (scl) \\n ensures result[1] == scl\\n // Ensures the result array is freshly allocated\\n ensures fresh(result)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0034": "// <vc-preamble>\\n// Ghost function for real number exponentiation with natural number exponents\\nghost function Pow(base: real, exp: nat): real\\n decreases exp\\n{\\n if exp == 0 then 1.0\\n else base * Pow(base, exp - 1)\\n}\\n\\n// Generate a Vandermonde matrix with decreasing powers (default behavior)\\n// The Vandermonde matrix is a matrix with terms of a geometric progression in each row\\n// For input vector x of length n and m columns, entry (i,j) = x[i]^(m-1-j)\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod Vander(x: seq<real>, m: nat) returns (result: seq<seq<real>>)\\n requires m > 0\\n ensures |result| == |x|\\n ensures forall i :: 0 <= i < |result| ==> |result[i]| == m\\n ensures forall i, j :: 0 <= i < |x| && 0 <= j < m ==> \\n result[i][j] == Pow(x[i], (m - 1 - j) as nat)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DT0030": "// <vc-preamble>\\n// Method that creates a sequence of ones with the same length as input\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod OnesLike<T>(a: seq<T>, one: T) returns (result: seq<T>)\\n // Postcondition: result has same length as input\\n ensures |result| == |a|\\n // Postcondition: every element in result is the \\"one\\" value\\n ensures forall i :: 0 <= i < |result| ==> result[i] == one\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0075": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod MultipleReturns(x: int, y: int) returns (more: int, less: int)\\n ensures more == x+y\\n ensures less == x-y\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0168": "// <vc-preamble>\\npredicate odd(n: nat) { n % 2 == 1 }\\npredicate even(n: nat) { n % 2 == 0 }\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod partitionOddEven(a: array<nat>) \\n modifies a\\n ensures multiset(a[..]) == multiset(old(a[..]))\\n ensures ! exists i, j :: 0 <= i < j < a.Length && even(a[i]) && odd(a[j])\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0199": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod FindZero(a: array<int>) returns (index: int)\\n requires a != null\\n requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]\\n requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i]\\n ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0\\n ensures 0 <= index ==> index < a.Length && a[index] == 0\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0606": "// <vc-preamble>\\nfunction Factorial(n: nat): nat\\n{\\n if n == 0 then 1 else n * Factorial(n-1)\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod ComputeFactorial(n: int) returns (u: int)\\n requires 1 <= n;\\n ensures u == Factorial(n);\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0723": "// <vc-preamble>\\npredicate IsNegative(n: int)\\n{\\n n < 0\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod FindNegativeNumbers(arr: array<int>) returns (negativeList: seq<int>)\\n\\n ensures forall i :: 0 <= i < |negativeList| ==> IsNegative(negativeList[i]) && negativeList[i] in arr[..]\\n\\n ensures forall i :: 0 <= i < arr.Length && IsNegative(arr[i]) ==> arr[i] in negativeList\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DD0037": "// <vc-preamble>\\nfunction sum (a:array<int>, i:int, j:int) :int\\ndecreases j\\nreads a\\nrequires 0 <= i <= j <= a.Length\\n{\\n if i == j then\\n 0\\n else\\n a[j-1] + sum(a, i, j-1)\\n}\\n\\npredicate is_prefix_sum_for (a:array<int>, c:array<int>)\\nreads c, a\\n{\\n a.Length + 1 == c.Length\\n && c[0] == 0\\n && forall j :: 1 <= j <= a.Length ==> c[j] == sum(a,0,j)\\n}\\n\\ndatatype List<T> = Nil | Cons(head: T, tail: List<T>)\\n\\nmethod from_array<T>(a: array<T>) returns (l: List<T>)\\nrequires a.Length > 0\\nensures forall j::0 <= j < a.Length ==> mem(a[j],l)\\n{\\n assume{:axiom} false;\\n}\\n\\nfunction mem<T(==)> (x: T, l:List<T>) : bool\\ndecreases l\\n{\\n match l\\n case Nil => false\\n case Cons(y,r)=> if (x==y) then true else mem(x,r)\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod queryFast (a:array<int>, c:array<int>, i:int, j:int) returns (r:int)\\nrequires is_prefix_sum_for(a,c) && 0 <= i <= j <= a.Length < c.Length\\nensures r == sum(a, i,j)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DJ0081": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod ListDeepClone(arr: array<int>) returns (copied: array<int>)\\n ensures arr.Length == copied.Length\\n ensures forall i :: 0 <= i < arr.Length ==> arr[i] == copied[i]\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DJ0140": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod Barrier(arr: array<int>, p: int) returns (result: bool)\\n requires\\n arr.Length > 0 &&\\n 0 <= p < arr.Length\\n ensures\\n result == forall k, l :: 0 <= k <= p && p < l < arr.Length ==> arr[k] < arr[l]\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DJ0087": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod HasCommonElement(list1: array<int>, list2: array<int>) returns (result: bool)\\n ensures\\n result == (exists i: int, j: int ::\\n 0 <= i < list1.Length && 0 <= j < list2.Length && (list1[i] == list2[j]))\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DJ0147": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod IntegerSquareRoot(n: int) returns (result: int)\\n requires n >= 1\\n ensures 0 <= result * result\\n ensures result * result <= n\\n ensures n < (result + 1) * (result + 1)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n}\\n// </vc-code>\\n", "DH0087": "// <vc-preamble>\\nfunction sumc(s: seq<int>, p: seq<bool>) : int\\n requires |s| == |p|\\n {\\n if |s| == 0 then 0 else (if p[0] then s[0] else 0) + sumc(s[1..], p[1..])\\n }\\nfunction add_conditon(lst: seq<int>) : (p : seq<bool>)\\n ensures |lst| == |p|\\n {\\n seq(|lst|, i requires 0 <= i < |lst| => i % 2 == 1 && lst[i] % 2 == 0)\\n }\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod add(v: seq<int>) returns (r : int)\\n\\n ensures r == sumc(v, add_conditon(v))\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n }\\n// </vc-code>\\n", "DH0002": "// <vc-preamble>\\n\\npredicate ValidInput(number: real)\\n{\\n number >= 0.0\\n}\\n\\npredicate ValidOutput(result: real, input: real)\\n{\\n 0.0 <= result < 1.0 && result == input - Floor(input)\\n}\\n\\nfunction Floor(x: real): real\\n ensures Floor(x) <= x < Floor(x) + 1.0\\n{\\n if x >= 0.0 then\\n FloorNonnegative(x)\\n else\\n -CeilNonnegative(-x)\\n}\\n\\nfunction FloorNonnegative(x: real): real\\n requires x >= 0.0\\n ensures FloorNonnegative(x) <= x < FloorNonnegative(x) + 1.0\\n ensures FloorNonnegative(x) >= 0.0\\n{\\n FloorHelper(x, 0)\\n}\\n\\nfunction FloorHelper(x: real, n: int): real\\n requires x >= 0.0\\n requires n >= 0\\n ensures FloorHelper(x, n) <= x + n as real < FloorHelper(x, n) + 1.0\\n ensures FloorHelper(x, n) >= n as real\\n decreases x\\n{\\n if x < 1.0 then \\n n as real\\n else \\n FloorHelper(x - 1.0, n + 1)\\n}\\n\\nfunction CeilNonnegative(x: real): real\\n requires x >= 0.0\\n ensures CeilNonnegative(x) >= x\\n ensures x > 0.0 ==> CeilNonnegative(x) < x + 1.0\\n{\\n if x == 0.0 then \\n 0.0\\n else if FloorNonnegative(x) == x then\\n x\\n else\\n FloorNonnegative(x) + 1.0\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod truncate_number(number: real) returns (result: real)\\n requires ValidInput(number)\\n ensures ValidOutput(result, number)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n }\\n// </vc-code>\\n", "DH0050": "// <vc-preamble>\\n\\nfunction to_lower(c: char): char\\n{\\n if \'A\' <= c <= \'Z\' then\\n (c as int - \'A\' as int + \'a\' as int) as char\\n else\\n c\\n}\\n\\npredicate IsPalindrome(text: string)\\n{\\n forall i :: 0 <= i < |text| ==> to_lower(text[i]) == to_lower(text[|text| - 1 - i])\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod is_palindrome(text: string) returns (result: bool)\\n ensures result <==> IsPalindrome(text)\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n }\\n// </vc-code>\\n", "DH0131": "// <vc-preamble>\\nfunction IsPrime(n: nat) : bool\\n{\\n n > 1 &&\\n forall k :: 2 <= k < n ==> n % k != 0\\n}\\nfunction min(a: int, b: int): int\\n{\\n if a <= b then a else b\\n}\\nfunction max(a: int, b: int): int\\n{\\n if a >= b then a else b\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod Intersection(start1: int, end1: int, start2: int, end2: int) returns (result: string)\\n\\n requires start1 <= end1 && start2 <= end2\\n\\n ensures result == \\"YES\\" || result == \\"NO\\"\\n ensures result == \\"YES\\" <==>\\n (max(start1, start2) <= min(end1, end2) &&\\n IsPrime((min(end1, end2) - max(start1, start2) + 1) as nat))\\n// </vc-spec>\\n// <vc-code>\\n{\\n assume {:axiom} false;\\n }\\n// </vc-code>\\n", "DV0128": "// <vc-preamble>\\nghost predicate IsPerfectSquare(n: nat)\\n{\\n exists i: nat :: i * i == n\\n}\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod IsPerfectSquareFn(n: int) returns (result: bool)\\n requires n >= 0\\n ensures result <==> IsPerfectSquare(n as nat)\\n// </vc-spec>\\n// <vc-code>\\n{\\n // impl-start\\n assume {:axiom} false;\\n result := false;\\n // impl-end\\n}\\n// </vc-code>\\n", "DV0108": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod IsPrime(n: nat) returns (result: bool)\\n requires n >= 2\\n ensures result ==> forall k: nat :: 2 <= k < n ==> n % k != 0\\n ensures !result ==> exists k: nat :: 2 <= k < n && n % k == 0\\n// </vc-spec>\\n// <vc-code>\\n{\\n // impl-start\\n assume {:axiom} false;\\n result := false;\\n // impl-end\\n}\\n// </vc-code>\\n", "DV0064": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod ReverseString(s: array<char>) returns (result: array<char>)\\n ensures\\n result.Length == s.Length &&\\n forall i :: 0 <= i < s.Length ==> result[i] == s[s.Length - 1 - i]\\n// </vc-spec>\\n// <vc-code>\\n{\\n // impl-start\\n assume {:axiom} false;\\n result := new char[0];\\n // impl-end\\n}\\n// </vc-code>\\n", "DV0085": "// <vc-preamble>\\n// </vc-preamble>\\n\\n// <vc-helpers>\\n// </vc-helpers>\\n\\n// <vc-spec>\\nmethod multiply(a: int, b: int) returns (result: int)\\n ensures result == a * b\\n// </vc-spec>\\n// <vc-code>\\n{\\n // impl-start\\n assume {:axiom} false;\\n result := 0;\\n // impl-end\\n}\\n// </vc-code>\\n", "LA0345": "-- <vc-preamble>\\ndef ValidInput (cards : List Int) : Prop :=\\n cards.length ≥ 1 ∧\\n (∀ i, 0 ≤ i ∧ i < cards.length → cards[i]! > 0) ∧\\n (∀ i j, 0 ≤ i ∧ i < j ∧ j < cards.length → cards[i]! ≠ cards[j]!)\\n\\ndef sum (cards : List Int) : Int :=\\n cards.sum\\n\\ndef sereja_optimal_score (cards : List Int) (left : Int) (right : Int) (sereja_turn : Bool) : Int :=\\n if h : 0 ≤ left ∧ left ≤ right ∧ right < cards.length then\\n if left = right then\\n if sereja_turn then cards[left.toNat]! else 0\\n else if cards[left.toNat]! > cards[right.toNat]! then\\n (if sereja_turn then cards[left.toNat]! else 0) + sereja_optimal_score cards (left+1) right (!sereja_turn)\\n else\\n (if sereja_turn then cards[right.toNat]! else 0) + sereja_optimal_score cards left (right-1) (!sereja_turn)\\n else 0\\ntermination_by (right - left + 1).toNat\\n\\ndef ValidOutput (scores : List Int) (cards : List Int) : Prop :=\\n scores.length = 2 ∧\\n scores[0]! ≥ 0 ∧ scores[1]! ≥ 0 ∧\\n scores[0]! + scores[1]! = sum cards ∧\\n scores[0]! = sereja_optimal_score cards 0 (cards.length - 1) true ∧\\n scores[1]! = sum cards - sereja_optimal_score cards 0 (cards.length - 1) true\\n\\n@[reducible, simp]\\ndef solve_precond (cards : List Int) : Prop :=\\n ValidInput cards\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef solve (cards : List Int) (h_precond : solve_precond cards) : List Int :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef solve_postcond (cards : List Int) (scores : List Int) (h_precond : solve_precond cards) : Prop :=\\n ValidOutput scores cards\\n\\ntheorem solve_spec_satisfied (cards : List Int) (h_precond : solve_precond cards) :\\n solve_postcond cards (solve cards h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LA0104": "-- <vc-preamble>\\ndef ValidInput (a1 a2 k1 k2 n : Int) : Prop :=\\n a1 ≥ 1 ∧ a2 ≥ 1 ∧ k1 ≥ 1 ∧ k2 ≥ 1 ∧ n ≥ 1\\n\\ndef MinimumSentOff (a1 a2 k1 k2 n : Int) (h : ValidInput a1 a2 k1 k2 n) : Int :=\\n let max_non_sendoff_cards := (k1 - 1) * a1 + (k2 - 1) * a2\\n if n - max_non_sendoff_cards > 0 then n - max_non_sendoff_cards else 0\\n\\ndef MaximumSentOff (a1 a2 k1 k2 n : Int) (h : ValidInput a1 a2 k1 k2 n) : Int :=\\n if k1 < k2 then\\n let team1_sent := if n / k1 < a1 then n / k1 else a1\\n let remaining_cards := n - team1_sent * k1\\n team1_sent + remaining_cards / k2\\n else\\n let team2_sent := if n / k2 < a2 then n / k2 else a2\\n let remaining_cards := n - team2_sent * k2\\n team2_sent + remaining_cards / k1\\n\\ndef ValidResult (a1 a2 k1 k2 n minimum maximum : Int) (h : ValidInput a1 a2 k1 k2 n) : Prop :=\\n minimum ≥ 0 ∧ maximum ≥ 0 ∧\\n minimum ≤ maximum ∧\\n maximum ≤ a1 + a2 ∧\\n minimum ≤ n ∧\\n maximum ≤ n ∧\\n minimum = MinimumSentOff a1 a2 k1 k2 n h ∧\\n maximum = MaximumSentOff a1 a2 k1 k2 n h\\n\\n@[reducible, simp]\\ndef solve_precond (a1 a2 k1 k2 n : Int) : Prop :=\\n ValidInput a1 a2 k1 k2 n\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef solve (a1 a2 k1 k2 n : Int) (h_precond : solve_precond a1 a2 k1 k2 n) : Int × Int :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef solve_postcond (a1 a2 k1 k2 n : Int) (result: Int × Int) (h_precond : solve_precond a1 a2 k1 k2 n) : Prop :=\\n ValidResult a1 a2 k1 k2 n result.1 result.2 h_precond\\n\\ntheorem solve_spec_satisfied (a1 a2 k1 k2 n : Int) (h_precond : solve_precond a1 a2 k1 k2 n) :\\n solve_postcond a1 a2 k1 k2 n (solve a1 a2 k1 k2 n h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LA0094": "-- <vc-preamble>\\ndef CharToPosSpec (c : String) : Int :=\\n if c == \\"v\\" then 0\\n else if c == \\">\\" then 1\\n else if c == \\"^\\" then 2\\n else if c == \\"<\\" then 3\\n else 0\\n\\npartial def FindNewline (s : String) (start : Nat) : Nat :=\\n if start >= s.length then s.length\\n else if s.data[start]! == \'\\\\n\' then start\\n else FindNewline s (start + 1)\\n\\npartial def SplitLinesSpec (s : String) : List String :=\\n if s.length == 0 then []\\n else\\n let i := FindNewline s 0\\n if i == s.length then [s]\\n else [s.take i] ++ SplitLinesSpec (s.drop (i+1))\\n\\npartial def FindSpace (s : String) (start : Nat) : Nat :=\\n if start >= s.length then s.length\\n else if s.data[start]! == \' \' then start\\n else FindSpace s (start + 1)\\n\\npartial def SplitBySpaceSpec (s : String) : List String :=\\n if s.length == 0 then []\\n else\\n let i := FindSpace s 0\\n if i == s.length then [s]\\n else [s.take i] ++ SplitBySpaceSpec (s.drop (i+1))\\n\\npartial def StringToIntHelper (s : String) (pos : Nat) (acc : Int) (negative : Bool) : Int :=\\n if pos >= s.length then (if negative then -acc else acc)\\n else if pos == 0 && s.data[pos]! == \'-\' then StringToIntHelper s (pos + 1) acc true\\n else if \'0\' ≤ s.data[pos]! && s.data[pos]! ≤ \'9\' then \\n StringToIntHelper s (pos + 1) (acc * 10 + (s.data[pos]!).toNat - \'0\'.toNat) negative\\n else StringToIntHelper s (pos + 1) acc negative\\n\\ndef StringToIntSpec (s : String) : Int :=\\n StringToIntHelper s 0 0 false\\n\\ndef ValidInput (input : String) : Prop :=\\n input.length > 0\\n\\ndef ValidOutput (result : String) : Prop :=\\n result == \\"cw\\" ∨ result == \\"ccw\\" ∨ result == \\"undefined\\"\\n\\n@[reducible, simp]\\ndef solve_precond (input : String) : Prop :=\\n ValidInput input\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef solve (input : String) (h_precond : solve_precond input) : String :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef solve_postcond (input : String) (result : String) (h_precond : solve_precond input) : Prop :=\\n ValidOutput result ∧\\n (input.length > 0 → (\\n let lines := SplitLinesSpec input\\n lines.length ≥ 2 → (\\n let positions := SplitBySpaceSpec lines[0]!\\n positions.length ≥ 2 → (\\n let startChar := positions[0]!\\n let endChar := positions[1]!\\n let n := StringToIntSpec lines[1]!\\n let startPos := CharToPosSpec startChar\\n let endPos := CharToPosSpec endChar\\n let ccw := (startPos + n) % 4 = endPos\\n let cw := (startPos - n) % 4 = endPos\\n (cw ∧ ¬ccw → result = \\"cw\\") ∧\\n (ccw ∧ ¬cw → result = \\"ccw\\") ∧\\n (¬(cw ∧ ¬ccw) ∧ ¬(ccw ∧ ¬cw) → result = \\"undefined\\")\\n )\\n )\\n ))\\n\\ntheorem solve_spec_satisfied (input : String) (h_precond : solve_precond input) :\\n solve_postcond input (solve input h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LD0424": "-- <vc-preamble>\\ndef valid_permut (a b : Array Int) : Prop :=\\na.size = b.size ∧ a.toList = b.toList\\ndef sorted (a : Array Int) : Prop :=\\n∀ i j, 0 ≤ i → i ≤ j → j < a.size → a[i]! ≤ a[j]!\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef swap (a : Array Int) (i j : Int) : Array Int :=\\nsorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\ntheorem swap_spec (a : Array Int) (i j : Nat) :\\n0 ≤ i → i < a.size → 0 ≤ j → j < a.size →\\nlet result := swap a i j\\n\\n-- Result is a valid permutation\\n\\nvalid_permut result a ∧\\n\\n-- Elements are swapped correctly\\n\\nresult.size = a.size ∧\\n\\nresult[i]! = a[j]! ∧\\n\\nresult[j]! = a[i]! ∧\\n\\n-- Other elements remain unchanged\\n\\n(∀ k, 0 ≤ k → k < a.size → k ≠ i → k ≠ j → result[k]! = a[k]!) :=\\nsorry\\n-- </vc-theorems>", "LD0073": "-- <vc-preamble>\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef Min_ (x y : Int) : Int :=\\nsorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\ntheorem Min_spec (x y z : Int) :\\nz = Min_ x y →\\n((x ≤ y → z = x) ∧\\n(x > y → z = y)) :=\\nsorry\\n-- </vc-theorems>", "LD0373": "-- <vc-preamble>\\ndef NChoose2 (n : Int) : Int :=\\nn * (n - 1) / 2\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef BubbleSort (a : Array Int) : Nat :=\\nsorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\ntheorem bubbleSort_spec (a : Array Int) (n : Nat) :\\nn ≤ NChoose2 a.size :=\\nsorry\\n-- </vc-theorems>", "LJ0088": "-- <vc-preamble>\\n@[reducible, simp]\\ndef isGreater_precond (arr : Array Int) (number : Int) : Prop :=\\n True\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef isGreater (arr : Array Int) (number : Int) (h_precond : isGreater_precond arr number) : Bool :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef isGreater_postcond (arr : Array Int) (number : Int) (result: Bool) (h_precond : isGreater_precond arr number) :=\\n (∀ i, i < arr.size → number > arr[i]!) ↔ result\\n\\ntheorem isGreater_spec_satisfied (arr: Array Int) (number: Int) (h_precond : isGreater_precond arr number) :\\n isGreater_postcond arr number (isGreater arr number h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LJ0155": "-- <vc-preamble>\\n@[reducible, simp]\\ndef removeDuplicates_precond (a : Array Int) := a.size ≥ 1\\n\\ndef inArray (a : Array Int) (x : Int) : Prop :=\\n ∃ i, i < a.size ∧ a[i]! = x\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef removeDuplicates (a : Array Int) (h_precond : removeDuplicates_precond a) : Array Int :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef removeDuplicates_postcond (a : Array Int) (result: Array Int) (h_precond : removeDuplicates_precond a) :=\\n (∀ i, i < result.size → inArray a result[i]!) ∧ \\n (∀ i j, i < j → j < result.size → result[i]! ≠ result[j]!)\\n\\ntheorem removeDuplicates_spec_satisfied (a: Array Int) (h_precond : removeDuplicates_precond a) :\\n removeDuplicates_postcond a (removeDuplicates a h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LV0084": "-- <vc-preamble>\\n@[reducible, simp]\\ndef kthElement_precond (arr : Array Int) (k : Nat) : Prop :=\\n k ≥ 1 ∧ k ≤ arr.size\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef kthElement (arr : Array Int) (k : Nat) (h_precond : kthElement_precond (arr) (k)) : Int :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible, simp]\\ndef kthElement_postcond (arr : Array Int) (k : Nat) (result: Int) (h_precond : kthElement_precond (arr) (k)) :=\\n arr.any (fun x => x = result ∧ x = arr[k - 1]!)\\n\\ntheorem kthElement_spec_satisfied (arr: Array Int) (k: Nat) (h_precond : kthElement_precond (arr) (k)) :\\n kthElement_postcond (arr) (k) (kthElement (arr) (k) h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LV0013": "-- <vc-preamble>\\n@[reducible]\\ndef ifPowerOfFour_precond (n : Nat) : Prop :=\\n True\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef ifPowerOfFour (n : Nat) (h_precond : ifPowerOfFour_precond (n)) : Bool :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\n@[reducible]\\ndef ifPowerOfFour_postcond (n : Nat) (result: Bool) (h_precond : ifPowerOfFour_precond (n)) : Prop :=\\n result ↔ (∃ m:Nat, n=4^m)\\n\\ntheorem ifPowerOfFour_spec_satisfied (n: Nat) (h_precond : ifPowerOfFour_precond (n)) :\\n ifPowerOfFour_postcond (n) (ifPowerOfFour (n) h_precond) h_precond := by\\n sorry\\n-- </vc-theorems>", "LB0046": "-- <vc-preamble>\\ndef ValidBitString (s : String) : Prop :=\\n ∀ {i c}, s.get? i = some c → (c = \'0\' ∨ c = \'1\')\\n\\ndef Str2Int (s : String) : Nat :=\\n s.data.foldl (fun acc ch => 2 * acc + (if ch = \'1\' then 1 else 0)) 0\\n\\ndef Exp_int (x y : Nat) : Nat :=\\n if y = 0 then 1 else x * Exp_int x (y - 1)\\n\\ndef ModExpPow2 (sx sy : String) (n : Nat) (sz : String) : String :=\\n sorry\\n\\naxiom ModExpPow2_spec (sx sy : String) (n : Nat) (sz : String)\\n (hx : ValidBitString sx) (hy : ValidBitString sy) (hz : ValidBitString sz)\\n (hsy_pow2 : Str2Int sy = Exp_int 2 n ∨ Str2Int sy = 0)\\n (hsy_len : sy.length = n + 1)\\n (hsz_gt1 : Str2Int sz > 1) :\\n ValidBitString (ModExpPow2 sx sy n sz) ∧\\n Str2Int (ModExpPow2 sx sy n sz) = Exp_int (Str2Int sx) (Str2Int sy) % Str2Int sz\\n\\ndef Mul_ (s1 s2 : String) : String :=\\n sorry\\n\\naxiom Mul_spec (s1 s2 : String) (h1 : ValidBitString s1) (h2 : ValidBitString s2) :\\n ValidBitString (Mul_ s1 s2) ∧ Str2Int (Mul_ s1 s2) = Str2Int s1 * Str2Int s2\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef ModExp (sx sy sz : String) : String :=\\n sorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\ntheorem ModExp_spec (sx sy sz : String) (hx : ValidBitString sx) (hy : ValidBitString sy) (hz : ValidBitString sz)\\n (hsy_pos : sy.length > 0) (hsz_gt1 : Str2Int sz > 1) :\\n ValidBitString (ModExp sx sy sz) ∧\\n Str2Int (ModExp sx sy sz) = Exp_int (Str2Int sx) (Str2Int sy) % Str2Int sz := by\\n sorry\\n-- </vc-theorems>", "LS0029": "-- <vc-preamble>\\n-- </vc-preamble>\\n\\n-- <vc-helpers>\\n-- </vc-helpers>\\n\\n-- <vc-definitions>\\ndef lcmInt (a b : Int) : Int :=\\nsorry\\n-- </vc-definitions>\\n\\n-- <vc-theorems>\\ntheorem lcmInt_spec (a b : Int) :\\n lcmInt a b ≥ 0 ∧\\n lcmInt a b % a = 0 ∧\\n lcmInt a b % b = 0 ∧\\n ∀ m : Int, m > 0 → m % a = 0 → m % b = 0 → lcmInt a b ≤ m :=\\nsorry\\n-- </vc-theorems>"}')
assert len(SAMPLE_DAFNY) == 30 and len(SAMPLE_LEAN) == 12
assert set(SPECS) == set(SAMPLE_DAFNY) | set(SAMPLE_LEAN)
print(f"{len(SPECS)} specs embarquees : {len(SAMPLE_DAFNY)} Dafny + {len(SAMPLE_LEAN)} Lean")
apercu = SPECS[SAMPLE_DAFNY[0]]
print(f"\n--- {SAMPLE_DAFNY[0]}_specs.dfy ({len(apercu)} caracteres) ---")
print(apercu[:520])