The Unclear Impact

Kristóf Marussy ferdium🎀 |

I'm a researcher working on the extra-functional requirements and formal verification of cyber-physical system architectures.
I also like free (as in liberty) software, privacy enhancing technologies, and cryptography.

I may not be trans but transgender hating script kiddies are too incompetent to tell the difference. Donkey Kong says trans rights = human rights.

@tuxedocomputers one more silly question about the firmware: if I get the ibp 14 gen8 without an nvidia GPU, will it still boot with secure boot enabled if i load my custom PK and KEK?

i understand that you don’t distribute kernel images signed by microsoft for your own distro ( – “Secure Boot must be disabled in your computer’s UEFI firmware”), but i’m planning to sign my own kernel images anyway and get rid of the microsoft PK/KEK entirely

this works nicely on my ibp 14 v4 (apparently it doesn’t have anything onboard that needs a microsoft KEK to initialize properly with uefi), but that’s a clevo motherboard, not a uniwill one. does the ibp 14 gen8 firmware has anything signed with microsoft’s keys that would break if i removed the keys?

@juliank the tricky thing is what would happen if you backtrack and the clauses that were in conflict get removed (if you remove versions of packages you decide not necessarily to install on backtracking).

in this case the conflict cause would become useful once you decide to install the same package at some other branch of the search when the variables and clauses get added back again. until then, some variables would be “dangling” (appear in the lemma, but not in the problem proper)

but i guess this is not actually a problem if variables can be uniquely identified (so it is apparent when they are re-added to the problem) and you never branch on “dangling” variables blobfoxthinkgoogly

SAT solvers are weird, man

@juliank ah, materializing further clauses sound reasonable, especially if solutions have a fairly regular structure. i guess your alternative would be to pull in clauses for all transitive dependencies, which sounds a lot more painful

a tricky thing is how to represent useful lemmas (CDCL-style) when some variables from the learned clause might not even be in the original problem (pulled in by a transitive dependency in your case).

the very least, i’m having a lot of trouble with that on the first-order model generator that we’re working on (i can’t even pull in all clauses eagerly in the beginning, because i don’t know the model size in advance and a FOL quantifier could match any model element)

2**32 levels of backtracking.

holy (super) cow! is that a state space of 2**(2**32)?

@juliank A->B|...|Z looks suspiciously like a dual-Horn clause !A | B | ... | Z (although I don’t know what to make of A->!B, other than just !A | !B). but it’s defnitely no accident that your algorithm is pretty much DPLL, given that your input is already basically in CNF blobfoxscience

maybe this is a good time for CDCL?


btw (commenting here because i’m not logging into my reddit account any time soon after the API debacle), it seems like the issue you linked in is not publicly accessible. i assume this should land in the next firmware update anyways?

Happy Enshittification Day! 💥

July 1, 2023: Reddit cuts off API access, Twitter requires login, Youtube may ban ad-blockers, Meta & Google block news in Canada...

A half-year since Cory Doctorow's seminal thesis on , how corporate platforms die (, and every corporate site seems hell bend on its own destruction.

Celebrate by going to [instance address]/about, find the donations link, and make your contribution to open social media!

mopidy lets me queue #bandcamp song previews with mopidy-bandcamp, but is currently nearly broken with #ncpmcpp for my use-cases (like the tag editor)

i resolved this conundrum for now by blobfoxcomfycofe (using bandcamp-dl and python-mpd2)

this doesn’t support adding V0 streams for songs i bought, but i don’t really need that. all songs i bought are downloaded in flac anyways. however, listening to 128k previews before i buy stuff bandcamp friday come is comfy

second student so far in the exam i’m correcting who claims that graph isomorphism is NP-complete

either they know something i don’t or they prepared for the exam… poorly blobfoxscience

Re: trademarks

@Techmeme company named after fruit allegedly more strongly represented by a depiction of fruit than the actual fruit – truly a hyperreal nightmare blobfoxcursedowo

not sure if i’m doing #pleroma -> #lemmy federation right blobfoxthonking

@ShittyKopper arch linux with sandboxed systemd units for most purposes. I should really set up podman to be rootless, but for now I can still enjoy running containers as systemd services, albeit unsandboxed on the systemd level


not sure whether i should try commenting on #lemmy with my poor self-hosted #pleroma instance (forcing it to locally store lemmy communities due to federation), or just create an account on a lemmy instance and leave system administration to more capable people blobfoxgooglymlem

@tuxedocomputers @tylerwolf is this still on the radar?

Is there any chance of an IBP 14 gen8 with an ANSI keyboard, or is this the final nudge for me to get into Colemak Mod-DH? blobfoxcomputerowo


thesis offense averted ablobcatwave

bandcamp won their union! bandcamp won their union!!

i'm so fucking happy for them, and also for the possible knock-on effects of some of epic game's holdings unionizing

their full statement -

WE WON 31-7 “Bandcamp United and Bandcamp management are committed to working together to continue to advance fair economic conditions for our workers and the artists who rely on us. We look forward to negotiating with an open mind and working in good faith to promote the best interests of all of our staff and the artist and label community we serve.”

yt-dlp -x -f bestaudio -o "%(playlist_index)02d. %(title)s.%(ext)s" 

is so comfy blobfoxcomfysmug

once more for the backrow hecklers

nvidia _choose_ to not support the wayland stack. or well more generally, the new linux kms+egl gpu stack, since there's a lot other cool things you can built on top of it that aren't wayland

nvidia _choose_ to implement crypto locked down fw in a way that blocks open drivers (even apple got this right!). and no one else can fix it, because it's actual real crypto

nvidia _choose_ to not fix any of this

don't buy nvidia if you don't like this

Scientific/academic journals charge but don’t give any money to the authors. Just email them and ask for a copy of the paper for free

realizing I need Emacs for playing around with Agda, I spent a good chunk of today declaring Emacs bankruptcy and setting up a new init.el

blobfoxhappy I have a much more lightweight but functional Emacs config now

blobfoxsad I still don’t know Agda