Login
You're viewing the slime.global public feed.
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:17 AM

    Okay. Whatever. Whatever!! At this point I go on tilt. I can't decode this documentation, I can't figure out why `idris2 -o` ignores my ipkg and `pack exec` fails without printing error messages. I know SML/NJ! I write my own list-equality helper. It takes seconds.

    …oh wait, it's not letting me use the Eq interface. Odd. Fine, I'll compare ints.

    …oh, there's… no such thing as… equality on ints. fine. Fine! I wanted Bits64s anyway. I—

    OH COME ON HOW IS THAT NOT A COVERING FUNCTION??

    -- True if two Lists are equal listEq : List (Eq a) -> List (Eq a) -> Bool listEq a b = case (a, b) of ([], []) => True (_::[], []) => False ([], _::[]) => False (a1::ar, b1::br) => if a1==b1 then listEq ar br else False It fails with: Can't find an implementation for Eq (Eq a)
    Same function but "Eq a" is replaced with "int". Error: "Can't find an implementation for Eq int".
    Same again but "int" is replaced with "Bits64". It says "main,listEq is not covering"
    💬 2🔄 0⭐ 0

Replies

  • mccmcc@mastodon.social
    Oct 20, 2026, 3:20 AM

    At about this point a very nice types.pl user replies to point out that the reason my original == code, with Data.List.Equalities, did not work was because I mixed up |> and <|. Again.

    …I…

    I'm frustrated. At this point. I'm not concentrating well. I'm trying not to mention "COVID-19 post-viral syndrome" in this thread, or how much Benadryl I'm on.

    Okay. Okay. It works now. As long as I run "pack exec". Which means I am now banned from getting error messages in the command line. Okay. Fine.

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:22 AM

    Please excuse me for my unprofessional outburst. With regard to whether my "listEq" implementation was a covering function. Although I'm still right.

    EDIT: Im wrong. I was given a counterexample. I think what I should have matched in cases two and three was (_, []) and ([], _); since the case ([], []) was already excluded, those patterns can only match "lists of 1 or more items" in the _ positions, and it will work. I did not test it.

    💬 2🔄 0⭐ 2
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:26 AM

    Also this… this is correct. This is absolutely correct. The problem was my |> / <| mixup, not which modules I had imported, and I don't have any need whatsoever for contrib, so I'm out of `pack` jail now. Okay. Alright. That's good. Okay. types.pl/@ionchy/1174710916268

    [QRT inset not provided because of the Mastodon 5 GUI reset dropping tomorrow. I've switched to masto-fe and can no longer quote boost.]

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:28 AM

    Hey question if in Idris you feed the |> function into the <| function, like you execute <| |>

    Does it unlock a quantum computing library

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:41 AM

    So. The story so far: In part 1, I made an emulator for a gross ass mini CPU. I'm given a program for it. In part 2, AOC guy informs me this program is SUPPOSED to be a quine, but it has a bug; the initial "register A" value is wrong. I need to find the A that reproduces the program. So I run the program in a loop, incrementing A each time until the program output equals its own code. I know this works; it works on the sample.

    But on my *assigned*program… well…

    lots of lines like "Success 15943678 [5, 0, 7, 7, 1, 1, 1, 3] eq? True"
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:44 AM

    (Ignore the "eq? True" there, I forgot a "not", it's repeating until it prints False).

    I didn't finish my program, as of this second. I didn't get around to implementing the code to recover after invalid-program or infinite-loop failures (but that's ok, because it appears those failures never never happen on the program input). I have it printing output on every line, and STDOUT is *definitely* slowing me down.

    Looking at the output, it's clear I don't need any of that.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:47 AM

    Although there are many programs this "cpu" COULD execute, the AOC guy clearly designed it to run this one program, or variants on this one program. The program is clearly expressing some function. You can like… *see*, the relationship between input (A value) and output (printed list). It's not linear, or smooth, but it's close. It's hard to express from a screenshot. I can see the output string herky-jerky growing as A linearly increases.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:51 AM

    The instruction set consists of a function that divides A by two, and a bunch of XOR ops. There's a jump function that jumps if A is nonzero. Implication: A is like a sort of logarithmic counter; the program whittles away dividing repeatedly by two until A hits zero. It's very clear the number of output digits scales linearly with the number of digits in A.

    This means a linear scan is out. After running a pretty long time, my output has 8 digits. My target string has 16.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 3:56 AM

    So even if I'm more efficient and am not waiting on STDOUT, I can't (shouldn't?) count up to 16 digits by hand.

    However, I'm *mostly* sure I can do something like a binary search. The XORs mean the output isn't smoothly increasing, but it's increasing on average, so a binary search will get me into the neighborhood, and maybe that'll identify a block of, I dunno, a thousand or a hundred "A" values that I can linearly scan and find my result.

    …tomorrow.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:21 AM

    …okay. I am *completely certain* the correct answer is somewhere between 35,184,372,088,831 and 281,474,976,710,656, noninclusive.

    💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:27 AM

    I'm laying in bed. I think about how the values in the input/output lists are all in the range 0-7, and wonder if the AOC taskmaster wants us to be thinking of them as an octal number.

    I think about "comparing" lists. I realize I don't know which end to compare from. I make a decision. I get up and start doing a *manual* binary search. Why not?

    I quickly find the numbers don't behave the way I hoped. Most numbers I pick turn into long strings of 4s, for some reason.

    But.

    Page full of numbers and comma-separated strings of numbers.
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:30 AM

    Treating my "goal" string as an octal number and looking at it in different bases revealed nothing interesting.

    A regular binary search really gets me nowhere. I think: Wait, isn't this math bitwise/logarithmic? I try doing a "binary" search picking midpoints with 10^((log10(a)+log10(b))/2). [block 1 in image above]

    That goes better, but not good enough. I quickly get two *broad* endpoints of my range, but can't reduce it further. [block 2 in image above]

    But then—

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:34 AM

    [block 3 in image above] I try looking at my input numbers in octal. I *immediately* realize that the number of printed "digits" in the output is exactly equal to the number of digits in my "A register" number represented as base 8. Hence: My answer will be n where
    octal 1000000000000000 <= n < octal 7777777777777777. 15 digits.

    This is the first concretely useful thing I've worked out so far.

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 6:39 AM

    I'm unsure what to do next. I still think I need to do some kind of directed search, but maybe instead of thinking about magnitude I measure bit similarity and toggle bits one by one. I imagine implementing this in JS and making 48 checkboxes for input bits I can play with. I imagine my linear scan emitting a Unicode bitmap.

    I have until 6 PM tomorrow to meet my one-week deadline.

    I worry I'm going to have to *read* the program and figure out what it's *actually doing*.

    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 7:18 AM

    Okay. Here's the commented "decomp" of the program I'm executing.

    This is… not so bad. The only particularly "chaotic" step is 2. Critically, all of this math works on only one "octal" digit at a time. Each output "digit" is dependent on a single octal input digit, plus one other, *higher-magnitude* 3-bit slice cmhosen chaotically on step 2.

    This means, I think, if I start with the most-significant digit and work "right", each output digit will "lock" and not change again.

    Register A: [THIS IS THE NUMBER I'M TRYING TO FIND] Register B: 0 Register C: 0 Program: 0 2,4 B = A % 8 1 1,1 B = B xor 1 2 7,5 C = A / (1 << B) 3 1,5 B = B xor 5 [0b101] 4 4,1 B = B xor C 5 5,5 output( B ) 6 0,3 A = A / 8 7 3,0 if ( A > 0 ) goto 0
    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 7:20 AM

    There's a word for this. In cryptanalysis/security. There's a word for a very old type of attack where you're trying to guess a password, but you figure out you can get a confirmation if the first character of the password is correct, so if there are 26 choices for N characters the complexity to guess it is 26*N instead of 26^N. What the heck is that called. The term stopped being used in the 00s because nobody serious has made this mistake since the 1980s.

    💬 5🔄 0⭐ 0
  • 💬 2🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 1:38 PM

    Padding Oracle Attack. That's the term I was looking for. Although rereading the Wikipedia page it looks like I may have been confused about the term, and it may just be an *example* of this attack class rather than a *term* for this attack class.

    defcon.social/@retsel/11747283

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 2:13 PM

    So here's what I did. I changed my linear scan so instead of just counting up from 0, it takes a list of numbers from STDIN. This allowed me to make a file containing a batch of numbers I want to check all at once (which I filter through perl -e 'while (<>) { last unless /\d/; $_ = oct($_); print "$_\n"; }', since I never figured out how to access the documented octal support library in Idris). This lets me test every leftmost digit, every one-right-of-leftmost digit, etc…

    A block of numbers 0000000000000000 through 7000000000000000, with only the first digit varying. The one beginning with "4 is highlighted; below, are some comma separated lists, one labeled "GOAL" and the others labeled with numbers. A highlight shows the rightmost digit for both GOAL and list "4" are 0.
    The numbers are filled out more on the left now; you see 4550000000000000 through 4550700000000000,again with only one digit varying. A highlight shows that list "5" (corresponding to 4550500000000000) matches on the right side with the "GOAL", on numbers 5,0,3,3,0.
    A harder number to parse. There are 16 numbers up to instead of 8, all but the final two terminal 0s are filled out now, and there are six separate highlights showing long matches on the right with the goal string.
    All digits in the numbers list are filled out; 4550533133267675 is highlighted, and below it's shown the corresponding list matches the goal exactly.
    💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Brian Swetlandswetland@chaos.social
    Oct 20, 2026, 7:30 AM

    @mcc I don't recall the term, but it has cropped up more recently than that. One of the original BLE pairing methods was vulnerable to this sort of incremental attack.

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Jamie is a friendly nutInfiniteNutshell@mastodon.social
    Oct 21, 2026, 1:10 PM

    @mcc because I am catching up on my feed a day late, I had to check the timestamp to see if this keysmash was still about the problem you were working on or if it was about private key = 4

    either way I'm counting this thread as dramatic irony for real life

    💬 1🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 21, 2026, 1:21 PM

    @InfiniteNutshell Ironically I actually could have finished this last night within my deadline but I was too busy updating my servers for PHP and "4"

    💬 0🔄 0⭐ 0
  • retselretsel@defcon.social
    Oct 20, 2026, 10:46 AM

    @mcc I was going to say padding oracle, but then that didn't sound quite right... Some sort of oracle... or side-channel if it's timing based?

    💬 0🔄 0⭐ 0
  • ROTOPE~1 ⭐️rotopenguin@mastodon.social
    Oct 20, 2026, 3:44 AM

    @mcc perl has the "spaceship" operator, it only makes sense that somebody else would have the Cosmic Ark operator

    Image attached toot
    💬 1🔄 1⭐ 0
  • Tim Ch-AI-se (now with bonus spooky) 👻gumnos@bsd.cafe
    Oct 20, 2026, 12:26 PM

    @mcc

    Hah, I dropped into the thread with @rotopenguin's post, expecting some light-hearted programming-language humor, not some "Epic trials of MCC" thread with 1.414×10⁴ posts 😆

    You have a great deal more fortitude for this adventure than I would ever have, but it sounds like you're having fun and learning stuff which is the important bit 😁

    💬 0🔄 0⭐ 0
  • mccmcc@mastodon.social
    Oct 20, 2026, 12:56 PM

    @gumnos the other "weeks" in this project have not gone off the rails in quite this way

    💬 0🔄 0⭐ 0
  • typeswitchtypeswitch@gamedev.lgbt
    Oct 20, 2026, 3:34 AM

    @mcc what about listEq [] [1,2] or listEq [1,2] []. these are not handled in the case blocks above. (the left hand side of the two False cases is not general enough).

    also it couldn't find Eq int because int is not Int (need to capitalize type names, lowercase types are type variables)

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • jjjjjj@functional.cafe
    Oct 20, 2026, 5:57 AM

    @mcc Disregarding my previous promise to know what I am talking about:
    For your code that starts with

    listEq : List (Eq a) -> List (Eq a) -> Bool

    I think the interface restriction needs to be written like this:

    listEq : Eq a => List a -> List a -> Bool

    For your specialized integer code, I think you need to capitalize your int as Int or maybe Integer (so List int should be List Int)

    Both these suggestions based on what I skimmed at idris2.readthedocs.io/en/lates

    As for the covering, I don't know.

    I really like following you Idris 2 adventure, I wish to learn it myself some day.

    I remember my intense struggles and frustration when learning Haskell a long while ago.

    💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0