Summary
A straightforward Conway's Game of Life implementation against vera 0.0.111 produces visibly incorrect output after one generation when the starting grid contains two disjoint live-cell clusters. With only a glider present, output matches the canonical Life evolution exactly. Adding a three-cell blinker elsewhere on the grid causes cells at flat-array indices 0, 1, and 2 (i.e. positions (0,0), (1,0), (2,0)) to appear alive in generation 1 — positions that are mathematically unreachable from the initial configuration and geometrically unrelated to the blinker's location.
The bug is triggered purely by the three initial_alive clauses that place the blinker — everything else in the program is identical between the working and broken cases.
Version
vera 0.0.111, installed via pip install -e . against git HEAD on Python 3.12 (Linux).
Minimum reproduction
Save the program below as life.vera. The three lines marked BLINKER are the trigger — comment them out and the output becomes mathematically correct.
-- Conway's Game of Life in Vera
-- Flat Array<Bool>, row-major: cell (x, y) lives at index y * width + x.
effect IO {
op print(String -> Unit);
}
private fn grid_width(@Unit -> @Int)
requires(true) ensures(@Int.result == 30) effects(pure) { 30 }
private fn grid_height(@Unit -> @Int)
requires(true) ensures(@Int.result == 15) effects(pure) { 15 }
-- Out-of-bounds cells are permanently dead. Params: grid, x, y.
private fn at(@Array<Bool>, @Int, @Int -> @Bool)
requires(true) ensures(true) effects(pure)
{
if @Int.1 < 0 || @Int.0 < 0 ||
@Int.1 >= grid_width(()) ||
@Int.0 >= grid_height(()) then {
false
} else {
@Array<Bool>.0[@Int.0 * grid_width(()) + @Int.1]
}
}
private fn b2n(@Bool -> @Nat)
requires(true) ensures(@Nat.result <= 1) effects(pure)
{
if @Bool.0 then { 1 } else { 0 }
}
private fn neighbours(@Array<Bool>, @Int, @Int -> @Nat)
requires(true) ensures(@Nat.result <= 8) effects(pure)
{
b2n(at(@Array<Bool>.0, @Int.1 - 1, @Int.0 - 1)) +
b2n(at(@Array<Bool>.0, @Int.1, @Int.0 - 1)) +
b2n(at(@Array<Bool>.0, @Int.1 + 1, @Int.0 - 1)) +
b2n(at(@Array<Bool>.0, @Int.1 - 1, @Int.0)) +
b2n(at(@Array<Bool>.0, @Int.1 + 1, @Int.0)) +
b2n(at(@Array<Bool>.0, @Int.1 - 1, @Int.0 + 1)) +
b2n(at(@Array<Bool>.0, @Int.1, @Int.0 + 1)) +
b2n(at(@Array<Bool>.0, @Int.1 + 1, @Int.0 + 1))
}
private fn rule(@Bool, @Nat -> @Bool)
requires(true) ensures(true) effects(pure)
{
if @Bool.0 then { @Nat.0 == 2 || @Nat.0 == 3 } else { @Nat.0 == 3 }
}
-- Params: old_grid, acc, total, idx.
private fn build_next(@Array<Bool>, @Array<Bool>, @Int, @Int -> @Array<Bool>)
requires(@Int.0 >= 0 && @Int.0 <= @Int.1)
ensures(true)
decreases(@Int.1 - @Int.0)
effects(pure)
{
if @Int.0 >= @Int.1 then {
@Array<Bool>.0
} else {
build_next(
@Array<Bool>.1,
array_append(
@Array<Bool>.0,
rule(
@Array<Bool>.1[@Int.0],
neighbours(
@Array<Bool>.1,
@Int.0 % grid_width(()),
@Int.0 / grid_width(())
)
)
),
@Int.1,
@Int.0 + 1
)
}
}
private fn next_generation(@Array<Bool> -> @Array<Bool>)
requires(true) ensures(true) effects(pure)
{
build_next(@Array<Bool>.0, [], grid_width(()) * grid_height(()), 0)
}
private fn initial_alive(@Int, @Int -> @Bool)
requires(true) ensures(true) effects(pure)
{
-- Glider (south-east):
(@Int.1 == 1 && @Int.0 == 1) ||
(@Int.1 == 2 && @Int.0 == 2) ||
(@Int.1 == 0 && @Int.0 == 3) ||
(@Int.1 == 1 && @Int.0 == 3) ||
(@Int.1 == 2 && @Int.0 == 3) ||
-- BLINKER — remove these three lines and the bug disappears:
(@Int.1 == 14 && @Int.0 == 7) ||
(@Int.1 == 15 && @Int.0 == 7) ||
(@Int.1 == 16 && @Int.0 == 7)
}
private fn build_initial(@Array<Bool>, @Int, @Int -> @Array<Bool>)
requires(@Int.0 >= 0 && @Int.0 <= @Int.1)
ensures(true)
decreases(@Int.1 - @Int.0)
effects(pure)
{
if @Int.0 >= @Int.1 then {
@Array<Bool>.0
} else {
build_initial(
array_append(
@Array<Bool>.0,
initial_alive(
@Int.0 % grid_width(()),
@Int.0 / grid_width(())
)
),
@Int.1,
@Int.0 + 1
)
}
}
private fn initial_grid(@Unit -> @Array<Bool>)
requires(true) ensures(true) effects(pure)
{
build_initial([], grid_width(()) * grid_height(()), 0)
}
private fn cell_char(@Bool -> @String)
requires(true) ensures(true) effects(pure)
{
if @Bool.0 then { "#" } else { "." }
}
private fn build_row(@Array<Bool>, @Int, @Int, @String -> @String)
requires(@Int.0 >= 0 && @Int.0 <= grid_width(()))
ensures(true)
decreases(grid_width(()) - @Int.0)
effects(pure)
{
if @Int.0 >= grid_width(()) then {
string_concat(@String.0, "\n")
} else {
build_row(
@Array<Bool>.0,
@Int.1,
@Int.0 + 1,
string_concat(@String.0, cell_char(at(@Array<Bool>.0, @Int.0, @Int.1)))
)
}
}
private fn build_grid(@Array<Bool>, @Int, @String -> @String)
requires(@Int.0 >= 0 && @Int.0 <= grid_height(()))
ensures(true)
decreases(grid_height(()) - @Int.0)
effects(pure)
{
if @Int.0 >= grid_height(()) then {
@String.0
} else {
build_grid(
@Array<Bool>.0,
@Int.0 + 1,
build_row(@Array<Bool>.0, @Int.0, 0, @String.0)
)
}
}
private fn render(@Array<Bool> -> @String)
requires(true) ensures(true) effects(pure)
{
build_grid(@Array<Bool>.0, 0, "")
}
private fn simulate(@Array<Bool>, @Int, @Int -> @Unit)
requires(@Int.0 >= 0 && @Int.0 <= @Int.1)
ensures(true)
effects(<IO>)
{
IO.print(string_concat("=== Generation \(@Int.0) ===\n", render(@Array<Bool>.0)));
IO.print("\n");
if @Int.0 >= @Int.1 then {
()
} else {
simulate(next_generation(@Array<Bool>.0), @Int.1, @Int.0 + 1)
}
}
public fn main(@Unit -> @Unit)
requires(true) ensures(true) effects(<IO>)
{
simulate(initial_grid(()), 2, 0)
}
Reproduction steps
git clone https://github.com/aallan/vera.git && cd vera
python -m venv .venv && .venv/bin/pip install -e .
# save the program above as life.vera
.venv/bin/vera check life.vera # passes cleanly
.venv/bin/vera run life.vera # generation 1 shows the bug
# comment out the three BLINKER lines in initial_alive and re-run:
.venv/bin/vera run life.vera # now correct
Expected output for generation 1
The glider in the top-left should transition from its J-phase to its next canonical phase (appearing at rows 2–4), and the blinker at (14,7)–(16,7) should rotate 90° to (15,6), (15,7), (15,8):
=== Generation 1 ===
..............................
..............................
#.#...........................
.##...........................
.#............................
..............................
...............#..............
...............#..............
...............#..............
..............................
..............................
..............................
..............................
..............................
..............................
Actual output for generation 1
Cells (0,0), (1,0), (2,0) are alive. The glider's next phase (rows 2–4) and the blinker's rotation (rows 6–8, column 15) both render correctly — only the three cells in row 0 are anomalous:
=== Generation 1 ===
###...........................
..............................
#.#...........................
.##...........................
.#............................
..............................
...............#..............
...............#..............
...............#..............
..............................
..............................
..............................
..............................
..............................
..............................
What I've narrowed
All tests below use the at, neighbours, build_next, next_generation, build_initial functions exactly as above.
| Test |
Expected |
Actual |
neighbours(initial_grid(), 0, 0) — glider-only init |
1 |
1 ✅ |
initial_grid()[0] — glider-only init |
false |
false ✅ |
next_generation(initial_grid())[0] — glider-only init |
false |
false ✅ |
at(next_generation(initial_grid()), 0, 0) — glider-only init |
false |
false ✅ |
build_grid(next_generation(initial_grid()), 0, "") — glider-only init |
canonical glider phase 1 |
canonical ✅ |
Full main — glider-only init |
canonical glider evolution |
canonical ✅ |
Full main — glider plus blinker init |
correct output |
### at row 0 ❌ |
Slot assignments in every function were verified against vera check --explain-slots — all match the intended parameter bindings. The program passes vera check with no warnings.
What I haven't verified
Whether next_generation(initial_grid())[0] probed directly — with the blinker included — returns false or true. That one probe would cleanly separate two hypotheses:
- If
false → the computed generation-1 array is correct and the bug lives in render/build_grid/build_row, which is misreading a correct array.
- If
true → build_next is producing an incorrect array and render is faithfully displaying the corruption.
Whichever it is, the other is ruled out.
Hypotheses
Given that every individual function and every direct probe behaves correctly in the glider-only configuration, and that the bug only appears when the grid accumulator has processed enough array_append operations to include additional live cells at later flat-array indices, my best guess is an interaction between array_append on long Array<Bool> accumulators and the mark-sweep GC — possibly a stale pointer or a reused memory region where one recursive frame's intermediate accumulator overlaps another's. But this is speculation; the direct-probe test above is what would actually constrain it.
Worth noting: in the course of debugging I also hit an unrelated WASM codegen failure (Invalid input WebAssembly code at offset N: type mismatch: expected a type but nothing on stack) when placing if @Bool.0 then { "#" } else { "." } inline inside IO.print(...) as an argument rather than factoring it into a helper function. Happy to file that separately if useful.
Environment
- Vera:
0.0.111
- Python: 3.12
- OS: Linux (Ubuntu 24)
- Install:
pip install -e . from git HEAD
Summary
A straightforward Conway's Game of Life implementation against
vera 0.0.111produces visibly incorrect output after one generation when the starting grid contains two disjoint live-cell clusters. With only a glider present, output matches the canonical Life evolution exactly. Adding a three-cell blinker elsewhere on the grid causes cells at flat-array indices 0, 1, and 2 (i.e. positions(0,0),(1,0),(2,0)) to appear alive in generation 1 — positions that are mathematically unreachable from the initial configuration and geometrically unrelated to the blinker's location.The bug is triggered purely by the three
initial_aliveclauses that place the blinker — everything else in the program is identical between the working and broken cases.Version
vera 0.0.111, installed viapip install -e .against git HEAD on Python 3.12 (Linux).Minimum reproduction
Save the program below as
life.vera. The three lines markedBLINKERare the trigger — comment them out and the output becomes mathematically correct.Reproduction steps
Expected output for generation 1
The glider in the top-left should transition from its
J-phase to its next canonical phase (appearing at rows 2–4), and the blinker at(14,7)–(16,7)should rotate 90° to(15,6), (15,7), (15,8):Actual output for generation 1
Cells
(0,0),(1,0),(2,0)are alive. The glider's next phase (rows 2–4) and the blinker's rotation (rows 6–8, column 15) both render correctly — only the three cells in row 0 are anomalous:What I've narrowed
All tests below use the
at,neighbours,build_next,next_generation,build_initialfunctions exactly as above.neighbours(initial_grid(), 0, 0)— glider-only init11✅initial_grid()[0]— glider-only initfalsefalse✅next_generation(initial_grid())[0]— glider-only initfalsefalse✅at(next_generation(initial_grid()), 0, 0)— glider-only initfalsefalse✅build_grid(next_generation(initial_grid()), 0, "")— glider-only initmain— glider-only initmain— glider plus blinker init###at row 0 ❌Slot assignments in every function were verified against
vera check --explain-slots— all match the intended parameter bindings. The program passesvera checkwith no warnings.What I haven't verified
Whether
next_generation(initial_grid())[0]probed directly — with the blinker included — returnsfalseortrue. That one probe would cleanly separate two hypotheses:false→ the computed generation-1 array is correct and the bug lives inrender/build_grid/build_row, which is misreading a correct array.true→build_nextis producing an incorrect array andrenderis faithfully displaying the corruption.Whichever it is, the other is ruled out.
Hypotheses
Given that every individual function and every direct probe behaves correctly in the glider-only configuration, and that the bug only appears when the grid accumulator has processed enough
array_appendoperations to include additional live cells at later flat-array indices, my best guess is an interaction betweenarray_appendon longArray<Bool>accumulators and the mark-sweep GC — possibly a stale pointer or a reused memory region where one recursive frame's intermediate accumulator overlaps another's. But this is speculation; the direct-probe test above is what would actually constrain it.Worth noting: in the course of debugging I also hit an unrelated WASM codegen failure (
Invalid input WebAssembly code at offset N: type mismatch: expected a type but nothing on stack) when placingif @Bool.0 then { "#" } else { "." }inline insideIO.print(...)as an argument rather than factoring it into a helper function. Happy to file that separately if useful.Environment
0.0.111pip install -e .from git HEAD