6 ms·
Static Integer Types
- thrower123 5y agoOne feature I wish was more common is the ability to easily range-restrict primitive types, without all the boxing and boilerplate and operator overloading. I can write a type that only handles integers 0-10, or floats [0...1], but it is more of a lift than I'd like to do in most cases, inefficient, and so I don't, even though it would be a boon for correctness and avoiding idiot bugs.
- touisteur 5y agoAda is for you then : https://learn.adacore.com/courses/intro-to-ada/chapters/strongly_typed_language.html#integers https://learn.adacore.com/courses/intro-to-ada/chapters/stro...
- _0ffh 5y agoOr Nim's subrange types. https://nim-lang.org/docs/manual.html#types-subrange-types https://nim-lang.org/docs/manual.html#types-subrange-types
- mixedCase 5y agoOr Idris dependent types, which allows you to prove properties of any value, not just numbers.
- zokier 5y agoAfaik refinement types (e.g. LiquidHaskell) are bit more appropriate than dependent types for this sort of thing
- goodpoint 5y agoPlus, Nim supports formal proof natively https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html
- touisteur 5y agoHey, great for Nim. Though I hope they're not /too/ tied to z3. Why3 seems to be the standard SOTA tool for proof: it can harness lots of different SMT solvers (each with their strengths and weaknesses) including z3, cvc4, alt-ergo, but also specific solvers (grappa?). It is at the heart of Frama-C and Spark2014. I also think that not having executable contracts by default (and defining whether you want them in your final program or not - see ghost code) is going to be a pain point in the future. I don't know nim enough to see if the syntax for provable properties is different from nim's ordinary syntax but I feel that it can also be a trap, to have your users learn yet another language for proof. I'm hoping for the best here, and I must say, I'm quite happy to see other languages/environment jump in ! Some years ago you had only industrial support for Frama-C, Spark, and some academic success around JML? I don't know Eiffel's Eve enough to say whether I would consider it 'mature'. Nowadays with the work on Rust by Alastair Reid we're getting some new energy in the domain. Great!
- goodpoint 5y ago> I hope they're not /too/ tied to z3 If you mean having a hard dependency on z3 at compile time or something similar - no, it's not. :)
- touisteur 5y agoI was more thinking of having written the whole verifier to fit/please z3. It can be hard/daunting to move to more 'generic' SMT drivers if done late in a project.
- mpweiher 5y agoAda? Newfangled nonsense. :-)) Pascal! http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/ref_data.doc.html#1143 http://www.dcs.ed.ac.uk/home/SUNWspro/3.0/pascal/lang_ref/re...
- touisteur 5y agoTIL Pascal had those. I'll need to check Turbo Pascal some day. I could have the joys of static bondage typing sooner.
- staticassertion 5y agoRust's const generics eval is quite powerful. It may be able to represent this.
- nynx 5y agoIt probably can't yet on stable, but it will be able to within the next year or so.
- staticassertion 5y agoOh yeah, I guess I should have mentioned I'm talking explicitly about the nightly const feature.
- steerablesafe 5y ago> If you dive into the C specification, you'll discover that the values I tried to cast lead to undefined behaviour [10] which means that my program could have done anything. In practice, the behaviour I observed can be explained very simply. This is not entirely correct. Note that this is integer conversion as opposed to signed integer arithmetic overflow. The latter is indeed undefined behavior, while the former is implementation defined. https://cigix.me/c17#6.3.1.3.p3 https://cigix.me/c17#6.3.1.3.p3 > Otherwise, the new type is signed and the value cannot be represented in it; either the result is implementation-defined or an implementation-defined signal is raised. In C++ since C++20 the result is defined. Before that the result was implementation-defined (without the option to raise a signal). AFAIK all major compilers do the obvious thing in both C and C++. The undefined behavior of signed integer overflow is indeed used by compiler optimizations.
- goldenkey 5y agoThe author of this post is oblivious to fractional bit encodings. When encoding an array of items, you can always encode the array optimally, only wasting less than 1 bit. For example, if we had an array of n test scores from 1-100, we only need ceil(n*log2(100)) bits. The key is that when reading the values, instead of shifting like we would normally to iterate an array, we instead divide by 100. Instead of masking bits, we get the current value by doing mod 100. Its equivalent to shifting/masking for a power of 2, but extends packing to fractional bits. It's quite beautiful. Take a look at this blog post to understand more about fractional bit representations: https://hbfs.wordpress.com/2011/11/01/fractional-bits-part-i/ https://hbfs.wordpress.com/2011/11/01/fractional-bits-part-i...
- jerf 5y agoSpeaking from experience on this... you get some crazy looks from code reviewers. I got perhaps overclever with this at one point using it to generate passwords by extracting log2(44) bits progressive out of a random number to choose from my blessed set of characters for passwords and it took some patience with the security team to verify that it was safe. I did it just because it's one of the more elegant ways out of the problem of truncation of bits when you have a non-even-power-of-two set of possibilities to choose from, especially when you need to do it repeatedly from a random source. Instead of discarding or fussing about, if you need fractional bits from a given random source of bits, you just... take fractional bits. No fuss. No muss.
- jhgb 5y ago> by extracting log2(44) bits progressive out of a random number to choose from my blessed set of characters for passwords and it took some patience with the security team to verify that it was safe. It's safe but if you somehow depended on all the passwords having exactly equal probability, you'd be wrong (unless you're already using a random number from a limited range). Of course this is easily fixed by a range check on the random number and generating it again if it failed the check.
- goldenkey 5y agoI also have written about using pairing functions to extract multiple random numbers from a single rand() call Your method is more concrete than mine, mine is math, yours is binary-based CS. https://churchofthought.org/blog/2019/07/24/an-ordered-variant-of-the-cantor-pairing-function/ https://churchofthought.org/blog/2019/07/24/an-ordered-varia...
- chrismorgan 5y agoOn Rust’s pointer-sized integer types, the design was subject to much agonising in 2013–2014. If you’re interested in the history, the end point is https://rust-lang.github.io/rfcs/0544-rename-int-uint.html https://rust-lang.github.io/rfcs/0544-rename-int-uint.html, and the GitHub comments on that RFC and earlier proposals, and earlier discussions on discuss.rust-lang.org as it was at the time (now renamed without redirect (grr!), change any links to internals.rust-lang.org). Beyond this, I speak as one who hasn’t done any embedded work or touched a platform where what this article calls “data width” and “address width” differ. I suspect that the key here for Rust is that it simply doesn’t have a type for what this article calls “data width”, because it wasn’t found to be useful. I’m not certain why you’d actually need such a type; I’m guessing that the only place it matters is the size of registers, which surface-level Rust doesn’t need to worry about, though I’m not sure if asm! has anything to do with it. I can imagine that things like GPIO pins which might need data width? will be done in a library for a specific board, and can thus define the type themselves. I also have a vague feeling that there’s also a third concept here, not just the two: that what I’ve called “data width” in the previous paragraph is actually “word size”, which could potentially be smaller again. Something about an 8-bit architecture with 16-bit address space and 32-bit pointers. Can’t remember if register sizes are consistent, either. I’m writing fairly incoherently and inaccurately here because I really don’t know what I’m talking about. :-)
- Someone 5y agoOne can also argue data width is the size of cache lines, which nowadays often are larger than registers (and might even be different in the various caches, but I don’t know whether such architectures exist)
- myrrlyn 5y agoI am the author of a library that requires knowledge and awareness of integers that are strictly not wider than the general purpose register on the processor; the fact that `usize` is "the largest GPR" on every target Rust knows about is great but I'd still appreciate a distinction between "this fits in exactly one GPR" vs "this fits in the address bus" _especially_ since the library in question creates pointers that are wider than `usize`
- nightpool 5y ago> Let’s start with Rust, which offers the usize type, defining it as “The pointer-sized unsigned integer type. The size of this primitive is how many bytes it takes to reference any location in memory.” That definition is based on the assumption that a machine’s address and data widths are the same Is this true? I don't know the history here, but just from reading that definition, it seems like `usize` is tied only to the address width. Where does the data width come in?
- gautamcgoel 5y agoYeah I didn't understand that part either. The quote doesn't mention data width at all...
- magicalhippo 5y agoI might be wrong but what came to mind was segmented memory, ie like 8086 where registers are 16bit but (far) pointers are 16:16 (ignoring the quirk with overlapping segments).
- moring 5y agoThat would make usize a 32-bit integer, regardless of the data width. It does make other hidden assumptions though, such as that there is a single "memory" that is uniquely identified by a usize value, regardless of the way it is accessed. For x86, for example, the same address could either refer to a location in memory or to a location in an I/O device, depending on whether in/out instructions or "normal" instructions were used.
- magicalhippo 5y ago> That would make usize a 32-bit integer, regardless of the data width. Doh, long day at work, misinterpreted "data width".
- fanf2 5y agoRust’s usize does the jobs of both uintptr_t (a pointer-width type) and size_t (a data-width type)
- oj002 5y ago> As far as I can see, the fast types are a failure, and the least types are unused, possibly because no-one can understand exactly what the latter mean. I personally quite like that we have the fast/least types, because they allow you to write portable code, that would otherwise require uintN_t types, which are only defined if the platform supports the specific width of the type. Let's say you want to implement a cryptographic (often require 32/64 bit modular arithmetic) algorithm that works on any confirming c compiler. uint32_t isn't guaranteed to be defined, but uint_least32_t is. You can now use uint_least32_t instead of uint32_t and mask out the upper bits that may exist when necessary. You'd do this with e.g. UINT32_C(0xFFFFFFFF), which ~~coincidentally~~ by design also has the type uint_least32_t. This would result in "perfect" code gen on any platform that has a 32-bit unsigned integer type (given a reasonable optimizing compiler), since in that case uint_least32_t is the same type as uint32_t, and otherwise it will still work. The fast types could be used for something similar, if they were properly defined. But C has a history of compilers implementing features not as intended, I'm looking at you rand(): "The C89 Committee decided that an implementation should be allowed to provide a rand function which generates the best random sequence possible in that implementation, and therefore mandated no standard algorithm" (c99 rational). Edit: Note that you also need to make sure that the variables aren't promoted to signed integers, e.g. x << 3 should be 1u*x << 3.
- steerablesafe 5y agoWell, rand has problems other than just being a poor random generator.
- nayuki 5y agoI found that types like uint32_least_t to be much less useful after learning that standard C/C++ types already have these guarantees. Namely: char is at least 8 bits wide, short is at least 16 bits wide, int is at least 16 bits wide, long is at least 32 bits wide, long long is at least 64 bits wide. Implementing cryptographic algorithms using uint32_least_t can be dangerous. Suppose that short is 32 bits wide and int is 48 bits wide. Your uint32_least_t might be mapped to unsigned short. When you do something like (x << 31), x gets promoted to signed int, and then you might be shifting a 1 into the sign bit, which is undefined behavior. So I would say that a better idea is to use unsigned long, which is guaranteed not to promote to a higher-rank type.
- bmc7505 5y agoI thought this blog post would discuss type-level integers but I didn’t see anything about that: https://users.rust-lang.org/t/notes-on-type-level-integral-numbers/5353/12 https://users.rust-lang.org/t/notes-on-type-level-integral-n...