Proof of False

2025 April Fool's joke for unnamed.website using Ren'Py

Building: Download the Ren'Py SDK then use your smol brain

SPOILERS BELOW

Drafty stuff

Basically LD: The Video Game (since I don't want to push back making that any farther) and my proof of false in Dafny and a puzzle game and I also need to make some sort of birthday present for Isaac, so let's kill infinite birds with one stone and do it all in one.

Characters:

• Saddam Hussein's LinkedIn
• Kublai: confused and naive
• Fenwick: CS fan https://www.cs.auckland.ac.nz/~peter-f/FTPfiles/2003%20Zeckendorf.pdf
• Segtree: also a CS fan too hard to get a good photo
• Golang gopher: the dude who runs my site
• Sydney (Already used in exozyme April Fools)
• $350 llama?
• Ali?
• Benq?

So for the prof character, should I use one of my own photos or some generic Ren'Py asset? I think I have more than enough of my own characters to "sacrifice" one to be the ufologist and it's more personalized and less cringe that way. I'll try both and see which one works the best

Also, I should probably keep the number of characters small to make the story memorable and simple since I think tgbgame was too complicated and the plot wasn't memorable at all

And the talk is gonna be totally memified

I think the humor of the talk comes from some really smart guy peddling complete conspiracy theories so it needs to start pretty seriously and then devolve into ufology. If the prof is some generic anime girl I think the setup wouldn't work as well since she wouldn't have credibility as an "MIT professor" but SHL would work for this role

Can't have too many characters since it's gonna be confusing to the player. 4 seems like enough. They each need to have very distinctive personalities!

KEEP IT SHORT AND SIMPLE AND EASY TO WRITE

Conclusion: No for using free Ren'Py assets, instead I'll pick SHL? Or the leopard cat

"joining fun (mostly harmless) cults: Ali's, Zumba, 152, 854, Benq, kebab skewer debobanation, kelvins, banana snapping, Genghis Impact (ask me about these sometime!)"

OK I should actually avoid using copyrighted stuff this time and only my photos

Constraints:

• Ren'Py WASM (so no Z3 😭) and I don't want to write custom menus like the poem-writing minigame, so you can click and select from menus (but the menus can be dynamically generated, fun)
• Puzzles (come up with some gimmick and expand on it)
• Segfaulting (does this work in WASM?)

For the puzzle, I'm thinking something like Baba is You but more flexible and with higher-order functions

I like puzzle games a lot so I want to make my own. I already ruled out a lot of categories such as word puzzles, Antichamber/AAAAXY-style puzzles (too hard to write)

The idea is this:

In Baba is You (super genius idea btw), rules are of the form

noun is verb

And these rules decide how you can modify the rules through self reference but it's through an elaborate moving-a-rabbit-thingy-around system

First, we can make everything a noun, and then function application is kinda like is. Constants are just functions that take no arguments (https://microsoft.github.io/z3guide/docs/logic/Uninterpreted-functions-and-constants/) so basically everything is a function and it'll be more elegant

And we can have more direct self reference? I tried making a repo about this (set-self-win) once but it didn't get that far.

But I think there's a lot of potential with this idea and I really have to do it by April 1 anyways so let's get started

Maybe this won't work out? I think I should have a backup plan

https://probgate.org/viewproblem.php?pid=812&cid=139

so turns out lambda calc is exactly what I want since functions act on other functions

To make a good puzzle game, it should be hard but you can build up intuition. One of the reasons that Baba is You is so great is because the space of possible moves you can make is simple (move in 4 directions) but you can achieve nontrivial "higher-level" moves out of that, so you feel great when you find a clever combination of moves that does something cool

Again, for my game, you'll only be able to choose from a list of terms

My first idea is that you have a bunch of terms and then you pick a term which applies itself to all other terms and I think that makes for super difficult puzzles but it's a bit too unpredictable and complicated and it's hard to build up intuition on what will happen several moves later unlike in Baba is You

So what if you choose two terms (possibly the same) and apply one term to the other? This has the advantage that it doesn't screw up the entire game state each move, although the question is whether the function term or the arg term gets replaced with the result (so I'll have to see which one leads to interesting puzzles), anyways that's how I can introduce the self reference

Is this too abstract? With some sort of animal metaphor maybe it can work? I think this gives the player enough control so they can build up intuition but still have to think.

I also did some web searching for lambda calc games and found https://tibordp.github.io/gator-calculus/ and https://worrydream.com/AlligatorEggs/ which are cool but not exactly what I want. I feel like most lambda calc games out there are focused on teaching people lambda calc (i.e. your moves are doing beta reduction) and not about making self referential games

So I think I should just code this up and if it's super cool, then great, otherwise the story can still be fun

But yeah the puzzles should be "extremely hard" because what's the fun of easy puzzles?

solution: Memey/troll puzzles

wormgate

github.com/dafny-lang/dafny/issues/6158

// Largest power of 2 that divides i
function lsb(i: nat): nat
    requires i > 0
    ensures 0 < lsb(i) <= i
{
    if i % 2 == 1 then 1 else 2 * lsb(i / 2)
}

opaque ghost function sum(s: seq<int>): int
{
    if |s| == 0 then 0 else s[0] + sum(s[1..])
}

class fenwick {
    var N: nat
    ghost var A: seq<int>
    var F: array<int>

    constructor (A': seq<int>)
        ensures F.Length == |A'| + 1
        ensures F.Length > 0
        ensures F.Length > 0 ==> false
        ensures false
    {
        N := |A'|;
        A := A';
        F := new int[|A'| + 1](i => if 0 < i <= |A'| then A'[i - 1] else 0);
        new;

        for i := 1 to F.Length
            modifies F
            // These invariants are complete garbage and wrong
            invariant forall j :: i < j <= N && j - lsb(j) / 2 >= i ==> F[j] == A[j - 1]
            invariant forall j :: 0 < j <= i <= N ==> lsb(j) > 0 && F[j] == sum(A[j - lsb(j)..j])
            invariant forall j :: 0 < j < i && i <= j + lsb(j) <= N ==> lsb(j) <= lsb(j + lsb(j)) && F[j + lsb(j)] == A[j + lsb(j) - 1] + sum(A[j + lsb(j) - lsb(j + lsb(j))..j])
            invariant i > 0 ==> false
        {
            var j := i + lsb(i);
            if j < F.Length {
                F[j] := F[j] + F[i];
                assert F[j] == A[j - 1];
                assert false;
            }
            assert false;
        }
        assert F.Length > 0 ==> false;
    }
}

method Main()
    ensures false
{
    var FT := new fenwick([0]);
    assert false;
    assert 0 == 1;

    assert FT.N == 69;
    print FT.N; // Actually prints 1
}

In python we can assert False to crash the game and then click ignore to skip it so we can do some 4th wall stuff

Story:

• Kublai: the crooked prover
• Gopher: super hyperactive
• SHL: super smart and authoritative but also a ufologist
• Fenwick: a CS fan, the source of reason
• You!!!!!!

Kublai confused why usual site is down, the Go gopher comes over and says even he's taking the day off to attend a talk by SHL about the variational derivation of the wave equation or something cool like that in the Stata bathroom shower (they couldn't book a better venue) except she goes on a long tangent about why she's giving this talk and then UFOs!!!!

the gopher and Fenwick are a bit skeptical, but Kublai says he has a proof that UFOs exist and then he proves false in Dafny and the game crashes and locks the chars into a weird lethal logic land that they have to escape by solving puzzles

I guess then the gimmick is that the game crashes a lot intentionally? Or at least if infinite recursion happens it'll crash. Actually we should sparingly use that gimmick and only crash once

then they return back to the normal site and Kublai asks if they wanna hear the proof again and everyone screams, roll the credits, then show link to the proof of false webcomic and the usual homepage at /home.html

TODO:

• look up free Ren'Py assets?
• associate image with character object: https://www.renpy.org/doc/html/dialogue.html#say-with-image-attributes
• skip main menu: https://www.renpy.org/doc/html/label.html#special-labels
• transparentize char images
• Shower bg
• favicon

be careful about image sizes

Question: game resolution?

Hmm I should just use 2560x1400 + webp and then everything will be sharp and nice

no AVIF though sad

For webp imagemagick I either have to -define webp:lossless=true or fiddle with -quality 90 since I swear I can see artifacts