// Copyright (c) 2026 Petr BalvĂ­n (https://petrbalvin.org) // SPDX-License-Identifier: BSD-3-Clause package verify import ( "os" "os/exec" "testing" ) // goobjAtomicMainSrc is the Go side of the LSE regression. The kernel // drives a counter with LDADDALD and mixes the accumulated total; main // derives the same value in Go and panics on any divergence before // printing the deterministic line the baseline and the gasm-linked // binaries must agree on. const goobjAtomicMainSrc = `package main func caller(p *int64, addv int64, times int64) int64 func main() { addv, times := int64(3), int64(5) v := int64(0) got := caller(&v, addv, times) oldsum, cur := int64(0), int64(0) for i := int64(0); i < times; i++ { oldsum += cur cur += addv } k := uint64(0x9e3779b97f4a7c15) want := int64(uint64(oldsum+cur) * k) if got != want { panic("atomic") } println("ok", caller(&v, addv, times)) } ` // TestGOOBJLinkAtomicKernel proves the arm64 LSE atomic families are proven // end to end: the kernel assembles by gasm into a GOOBJ object, substitutes // byte-wise into a real go build archive, relinks with cmd/link and the // linked binary computes the same atomic total as the toolchain-built one // under qemu-user, with the documented degradation on emulators without // LSE (the baseline run fails first and the claim drops to link-only). func TestGOOBJLinkAtomicKernel(t *testing.T) { if testing.Short() { t.Skip("builds the gasm binary and links Go programs") } if os.Getenv("GASM_LINK_PARITY") == "" { t.Skip("deliberate verification: set GASM_LINK_PARITY=1 (just link-parity)") } goBin, err := exec.LookPath("go") if err != nil { t.Skip("no Go toolchain available") } gasmBin := buildLinkParityGasm(t, goBin) t.Run("arm64", func(t *testing.T) { goobjLinkKernel(t, goBin, gasmBin, "arm64", "linkatomic_arm64.s", goobjAtomicMainSrc) }) }