3 ms·

How do we know it's actually correct?

by slopinthebag 6mo ago

perching_aix 6mo ago
By using it.
- repelsteeltje 6mo ago
  It works == it's correct?
  - mjr00 6mo ago
    This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct.
    - speedgoose 6mo ago
      use std::fs::File; use std::io::prelude::*; fn main() -> std::io::Result<()> { let mut file = File::create("content.txt")?; file.write_all(b"3!")?; Ok(()) }
      - rakel_rakel 6mo ago
        ; cat content.txt 3!;
    - dataflow 6mo ago
      > This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct. No, it doesn't even need to compile. The mere fact that it's in Rust means it's correct.
  - perching_aix 6mo ago
    Yes? What do you think fuzzing, unit testing, integration testing is for? It's an empirical evaluation of correctness. Literally just try and see. For actual correctness verification in the strong sense, you'd need to start from a specification written in a formal language so that it's machine checkable, which if I had to guess not even win.rar GmbH has.
    - repelsteeltje 6mo ago
      I hope the developers of, say, the brakes in my car don't interpret 'software correctness' the way you do. Added, later: hey you changed your comment, added a whole paragraph.
      - deleted 6mo ago
        [deleted]
      - atiedebee 6mo ago
        I hope the brakes in my car don't need developers
        pixl97 6mo ago
        I think you underestimate the complexity of modern braking systems.
        arcticbull 6mo ago
        ABS doesn't just appear organically.
      - throw1234567891 6mo ago
        They used to. Now they have systems, standards, and experience. There are only so many ways you can do brakes on the car.
      - perching_aix 6mo ago
        I added the second paragraph about formal verification at the same time you posted, in anticipation that you'd immediately dig your heels into it otherwise, despite me highlighting that the other methods are merely empirical. I was immediately proven right once I pressed "update". That said, I have now deleted my snarky response that followed. Not in the game of capitalizing off of the human equivalent of a race condition. I should make a browser addon to delay posting, this is the 2nd time this happens in the past few days. Edit: Nevermind, it's already a feature built into the site. Turned it on. I wonder if it applies to edits also... Nope, doesn't seem to. Oh well, should still help.
- slopinthebag 6mo ago
  Thus all software that can be used is correct? You know what I meant: How can we have confidence that this implementation of RAR is functionally identical to what it's based on? What would give me the confidence to use it in a critical piece of infrastructure?
  - jaggederest 6mo ago
    Validating compression systems is usually really straightforward. There are 3 layers - decode known values from compressed files (or encode, same), round trip without any alterations, and fuzzing with arbitrary binaries Because it's a defined format there can be binary exact comparisons between the input and output files - we already have an oracle in the form of proper RAR format software, so if they are identical, you don't need to look further for that specific case. You can see a version of this that I did quite similarly, for postgresql wire format, here: https://github.com/pgdogdev/pgdog/tree/main/integration/sql https://github.com/pgdogdev/pgdog/tree/main/integration/sql It validates that sql with the same setup, teardown, and test results in perfectly exact compatibility between raw postgresql as the control and various configurations of PgDog, with both the text format and binary format, so ultimately a 6-way multivariate test that should always result in binary-exact results.
    - slopinthebag 6mo ago
      Right, that's very different from "using it" and it's also different from "Have an LLM generate code that compiles".
  - perching_aix 6mo ago
    > Thus all software that can be used is correct? You also know what I meant, since I spelled it out in more detail a comment later. But even though you're being facetious, yes, that really is the case. If it works it works. That's the bar for the vast, vast majority of software, and has been since forever. Demonstrated practical correctness. If you stumble into a bug, you log it as a defect and then either wait for a fix or fix it yourself depending. That's all that regular people ever have. In the case of this project, this was achieved via fuzz testing. It's literally no different to e.g. validating the NTFS driver that ships in the Linux kernel, or validating any other (re)implementation of anything. You just do a bunch of empirical testing and hope for the best. It is also why reimplementations always lag behind, which I'm not suggesting is not a real concern (or that defects wouldn't be). It's just not a gotcha. Hell, I'm 99% sure this is exactly what the actual vendor does too, or at least I sure hope that they do have tests at least. Cause they're sure as shit not using a formally verified compiler toolchain, meaning they definitely don't have a formal proof about whether even the official implementation in itself is correct. Only empirical data at best too.
- TacticalCoder 6mo ago
  I could be correct but way too slow in edge cases (unlikely with Rust but you never know), leaking temporary files, having security holes, etc. There's much more about correctness of a piece of software than: "produces the same output as the original on x test cases". I'm not saying it's a bad implementation and, if anything, LLMs are much better at translating/porting existing code (and finding bugs) than at writing things unheard of. You're basically saying, if I may make a pun: "rust me bro, it's correct".
  - perching_aix 6mo ago
    [dead]
  - davidsong 6mo ago
    Yeah the main things are DoS attacks and path traversal issues. I intentionally guarded against these with resource limits and checks, but I can't guarantee that it's safe. I mean, basically anyone who carefully reads it knows more about it than me - you play the AI slot machine at this scale and who knows what prizes you'll win!
davidsong 6mo ago
I compressed thousands of files, went through libarchive's and Sembiance's test data at least for the decompressor side. I recompressed the files, and round-tripped them against 7zip, unrar, every later version of winrar. It failed a lot at the start, and codex burned a lot of tokens instrumenting the binaries and dividing and conquering until things settled down and round-trips worked properly. I can't really say it works in every case as I honestly didn't spend that much time on it. But it works in the majority of cases. There's likely some nasty bugs hiding in there.

How do we know it's actually correct?

perching_aix 6mo ago

By using it.

repelsteeltje 6mo ago
It works == it's correct?
- mjr00 6mo ago
  This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct.
  - speedgoose 6mo ago
    use std::fs::File; use std::io::prelude::*; fn main() -> std::io::Result<()> { let mut file = File::create("content.txt")?; file.write_all(b"3!")?; Ok(()) }
    - rakel_rakel 6mo ago
      ; cat content.txt 3!;
  - dataflow 6mo ago
    > This is Rust we're talking about. It doesn't even need to work; as long as it compiles, it's correct. No, it doesn't even need to compile. The mere fact that it's in Rust means it's correct.
- perching_aix 6mo ago
  Yes? What do you think fuzzing, unit testing, integration testing is for? It's an empirical evaluation of correctness. Literally just try and see. For actual correctness verification in the strong sense, you'd need to start from a specification written in a formal language so that it's machine checkable, which if I had to guess not even win.rar GmbH has.
  - repelsteeltje 6mo ago
    I hope the developers of, say, the brakes in my car don't interpret 'software correctness' the way you do. Added, later: hey you changed your comment, added a whole paragraph.
    - deleted 6mo ago
      [deleted]
    - atiedebee 6mo ago
      I hope the brakes in my car don't need developers
      - pixl97 6mo ago
        I think you underestimate the complexity of modern braking systems.
      - arcticbull 6mo ago
        ABS doesn't just appear organically.
    - throw1234567891 6mo ago
      They used to. Now they have systems, standards, and experience. There are only so many ways you can do brakes on the car.
    - perching_aix 6mo ago
      I added the second paragraph about formal verification at the same time you posted, in anticipation that you'd immediately dig your heels into it otherwise, despite me highlighting that the other methods are merely empirical. I was immediately proven right once I pressed "update". That said, I have now deleted my snarky response that followed. Not in the game of capitalizing off of the human equivalent of a race condition. I should make a browser addon to delay posting, this is the 2nd time this happens in the past few days. Edit: Nevermind, it's already a feature built into the site. Turned it on. I wonder if it applies to edits also... Nope, doesn't seem to. Oh well, should still help.
slopinthebag 6mo ago
Thus all software that can be used is correct? You know what I meant: How can we have confidence that this implementation of RAR is functionally identical to what it's based on? What would give me the confidence to use it in a critical piece of infrastructure?
- jaggederest 6mo ago
  Validating compression systems is usually really straightforward. There are 3 layers - decode known values from compressed files (or encode, same), round trip without any alterations, and fuzzing with arbitrary binaries Because it's a defined format there can be binary exact comparisons between the input and output files - we already have an oracle in the form of proper RAR format software, so if they are identical, you don't need to look further for that specific case. You can see a version of this that I did quite similarly, for postgresql wire format, here: https://github.com/pgdogdev/pgdog/tree/main/integration/sql https://github.com/pgdogdev/pgdog/tree/main/integration/sql It validates that sql with the same setup, teardown, and test results in perfectly exact compatibility between raw postgresql as the control and various configurations of PgDog, with both the text format and binary format, so ultimately a 6-way multivariate test that should always result in binary-exact results.
  - slopinthebag 6mo ago
    Right, that's very different from "using it" and it's also different from "Have an LLM generate code that compiles".
- perching_aix 6mo ago
  > Thus all software that can be used is correct? You also know what I meant, since I spelled it out in more detail a comment later. But even though you're being facetious, yes, that really is the case. If it works it works. That's the bar for the vast, vast majority of software, and has been since forever. Demonstrated practical correctness. If you stumble into a bug, you log it as a defect and then either wait for a fix or fix it yourself depending. That's all that regular people ever have. In the case of this project, this was achieved via fuzz testing. It's literally no different to e.g. validating the NTFS driver that ships in the Linux kernel, or validating any other (re)implementation of anything. You just do a bunch of empirical testing and hope for the best. It is also why reimplementations always lag behind, which I'm not suggesting is not a real concern (or that defects wouldn't be). It's just not a gotcha. Hell, I'm 99% sure this is exactly what the actual vendor does too, or at least I sure hope that they do have tests at least. Cause they're sure as shit not using a formally verified compiler toolchain, meaning they definitely don't have a formal proof about whether even the official implementation in itself is correct. Only empirical data at best too.
TacticalCoder 6mo ago
I could be correct but way too slow in edge cases (unlikely with Rust but you never know), leaking temporary files, having security holes, etc. There's much more about correctness of a piece of software than: "produces the same output as the original on x test cases". I'm not saying it's a bad implementation and, if anything, LLMs are much better at translating/porting existing code (and finding bugs) than at writing things unheard of. You're basically saying, if I may make a pun: "rust me bro, it's correct".
- perching_aix 6mo ago
  [dead]
- davidsong 6mo ago
  Yeah the main things are DoS attacks and path traversal issues. I intentionally guarded against these with resource limits and checks, but I can't guarantee that it's safe. I mean, basically anyone who carefully reads it knows more about it than me - you play the AI slot machine at this scale and who knows what prizes you'll win!

davidsong 6mo ago

I compressed thousands of files, went through libarchive's and Sembiance's test data at least for the decompressor side. I recompressed the files, and round-tripped them against 7zip, unrar, every later version of winrar. It failed a lot at the start, and codex burned a lot of tokens instrumenting the binaries and dividing and conquering until things settled down and round-trips worked properly. I can't really say it works in every case as I honestly didn't spend that much time on it. But it works in the majority of cases. There's likely some nasty bugs hiding in there.