Stone Game / 石子游戏

English

Problem

Alice and Bob take turns removing an entire pile from either end of a row of stone piles. Alice moves first. Each player's score is the number of stones collected. Both players play optimally. Complete the proof of the supplied function, which returns 1 if Alice's score is strictly greater than Bob's, and 0 otherwise. The input array must remain unchanged.

int stone_game(int *piles, int n, int **dp);

The caller supplies an array of n row pointers. Each row points to n zero-initialized integers. The row-pointer array, all rows, and piles occupy pairwise disjoint memory resources. The function fills the upper triangle of this matrix using dynamic programming; it does not allocate memory.

The fixed STONE_ROW(p, k) macro accesses row pointer p[k] through the byte offset k * sizeof(void *). The judge ABI gives int * and void * the same size, so this is the same row access. The final cell is read into score before testing whether it is positive.

Constraints and mathematical model

2 <= n <= 500, and n is even.
piles has exactly n elements, each between 1 and 500, inclusive.
The total number of stones is odd.
The matrix has exactly n rows, each of length n, initially all zero.

The ghost parameter xs records the original pile array, and rows records the initial matrix contents. StoneMatrix dp n rows owns the row-pointer array and each row, using separating conjunction. These parameters are mathematical values, not additional C arguments.

stone_score(xs, i, j) is the optimal score difference between the player whose turn it is and the opponent on the inclusive interval [i, j]. On valid, nonempty intervals it satisfies

stone_score(xs, i, i) = xs[i]
stone_score(xs, i, j) = max(xs[i] - stone_score(xs, i + 1, j),
                          xs[j] - stone_score(xs, i, j - 1))   when i < j

The header defines this model by recursion on a natural-number interval length. Length zero has value zero. An interval [lo, hi] uses length max(hi - lo + 1, 0). Accesses outside the mathematical list, including negative indices, have value zero. stone_sum is the ordinary list sum, with empty sum zero. All these definitions use mathematical integers; executable C score arithmetic must separately be shown to fit in a signed 32-bit int.

Verification task

Prove that, on return:

The return value satisfies StoneResult xs result: it is 1 exactly when stone_score(xs, 0, n - 1) > 0, and 0 otherwise.
Every entry dp[i][j] with 0 <= i <= j < n equals stone_score(xs, i, j).
piles retains all its original elements, and ownership of the row-pointer array and all n rows of length n is returned. The postcondition imposes no additional value requirement on the lower triangle.

The task checks memory safety, absence of integer overflow, and partial correctness with respect to this contract. The parity assumptions do not remove the requirement to verify the computed table.

Submission

Complete starter.c using C* loop invariants, proof blocks, and any needed proof-only definitions or lemmas. Submit the completed file; the judge checks it as problem.c alongside the fixed problem.h.

You may add or change proof-only material. Keep the header, function signature, ghost parameters, precondition, postcondition, and executable C statements fixed. Do not add axioms, admissions, or unproved strategies. No main, input parsing, or output handling is needed.

Source: LeetCode 877.

中文

题目

Alice 和 Bob 轮流从一排石子的任意一端取走一整堆石子，Alice 先手。每位玩家的得分是自己取得的石子总数。双方都采用最优策略。请补全给定函数的证明：当 Alice 的得分严格大于 Bob 时返回 1，否则返回 0。输入数组的内容必须保持不变。

int stone_game(int *piles, int n, int **dp);

调用方提供一个包含 n 个行指针的数组，每个指针指向 n 个初始化为零的整数。行指针数组、各行以及 piles 分别占有互不重叠的内存资源。函数通过动态规划填充矩阵的上三角部分，不分配内存。

固定宏 STONE_ROW(p, k) 通过字节偏移 k * sizeof(void *) 访问行指针 p[k]。评测平台的 ABI 中，int * 与 void * 的大小相同，因此该写法访问的仍是同一行。程序将最终单元格的值读入 score，再判断其是否为正。

约束与数学模型

2 <= n <= 500，且 n 为偶数。
piles 恰有 n 个元素，每个元素均在 1 到 500 之间（含端点）。
石子总数为奇数。
矩阵恰有 n 行，每行长度为 n，初始元素均为零。

幽灵参数 xs 记录原始石子数组，rows 记录矩阵的初始内容。 StoneMatrix dp n rows 通过分离合取描述行指针数组及每一行的内存所有权。这些参数是数学值，不是额外的 C 函数参数。

stone_score(xs, i, j) 表示在闭区间 [i, j] 上，当前行动的玩家相对于对手的最优得分差。对合法的非空区间，它满足

stone_score(xs, i, i) = xs[i]
stone_score(xs, i, j) = max(xs[i] - stone_score(xs, i + 1, j),
                          xs[j] - stone_score(xs, i, j - 1))   当 i < j 时

头文件通过自然数区间长度上的递归定义这一模型。长度为零时，得分差为零。区间 [lo, hi] 对应的长度为 max(hi - lo + 1, 0)。对数学列表的越界访问（包括负下标）取值为零。stone_sum 是通常的列表求和，空列表之和为零。这些定义中的运算均使用数学整数；还需单独证明可执行 C 代码中与得分相关的运算不会超出有符号 32 位 int 的范围。

验证任务

证明函数返回时：

返回值满足 StoneResult xs result：当且仅当 stone_score(xs, 0, n - 1) > 0 时返回 1，否则返回 0。
对所有 0 <= i <= j < n，dp[i][j] 等于 stone_score(xs, i, j)。
piles 的每个元素保持不变，并归还行指针数组以及全部 n 行的内存所有权，每行长度仍为 n。后置条件对下三角部分的元素值不作额外要求。

本题检查内存安全、整数运算不溢出，以及相对于给定契约的部分正确性。即使输入满足上述奇偶性约束，也必须验证实际计算出的整个上三角表格。

提交方式

在 starter.c 中补充 C* 循环不变式、证明块，以及所需的纯证明定义和引理。提交补全后的文件；评测系统将其命名为 problem.c，与固定的 problem.h 一同验证。

可以添加或修改纯证明内容。头文件、函数签名、幽灵参数、前置条件、后置条件以及可执行 C 语句均不可修改。不得添加公理、跳过证明或使用未经证明的策略。无需编写 main、输入解析或输出处理。

来源：LeetCode 877。

Examples / 示例

Piles / 石子数组	Return value / 返回值
`[5, 3, 4, 5]`	`1`
`[3, 7, 2, 3]`	`1`
`[1, 2]`	`1`

The optimal score differences for these three arrays are 1, 5, and 1, respectively. For [1, 2], Alice takes the pile of size 2, leaving 1 for Bob.

这三个数组对应的最优得分差分别为 1、5 和 1。对于 [1, 2]， Alice 取走有 2 个石子的那一堆，Bob 得到剩下的 1 个石子。