asciilifeform: ftr several different items in ffa seemed to me to be 'five-angled heptagons' (starting with how to compute the asm-less addition carries) until i solved'em

asciilifeform: ideally could somehow get rid of want() tho, AND not rely on implicit bounds checks

asciilifeform: i don't see any reason why the thing should ~rely~ on adatronicn bounds checks for correctness.

asciilifeform: easy to say on 3GHz+ pc

asciilifeform: pc arch also does not, unfortunately, give a way for userland to trap on reads/writes to specific piece of memory

asciilifeform: and at any rate the right place for such a thing is in the code, rather than in the guts of the linker

asciilifeform: there is not, afaik, a way to force stack frames to be explicitly padded

asciilifeform: the other open q is where to draw the line re 'somebody, some day, with mutilated ffa' .

asciilifeform: ( i.e. equal to the arity of the highest-arity stack op )

asciilifeform: to carry this to logical conclusion

asciilifeform: possibly there ought to be not 1 but... 4 null cells ☟︎

asciilifeform: i was about to add :

asciilifeform: the fundamental riddle is whether this is an ~avoidable~ instance of http://btcbase.org/log/2016-01-21#1379603 -ism ☝︎

asciilifeform: *preferable to

asciilifeform: this however is preferable than writing to the return addr on the stack !

asciilifeform: mine is also ugly, it is conceivable that somebody, some day, in a broken variant and running with -gnatp, ~will~ write to the zero cell

asciilifeform: as in the http://btcbase.org/log/2018-01-17#1771768 example. ☝︎

asciilifeform: i.e. if you see an array reference, you ~know~ that it is valid, because of the type of the index.

asciilifeform: ideally there would be NONE of any such thing, in the entire program.

asciilifeform: at the risk of repeating myself.

asciilifeform: the fact that an array is indexed by a type which has a range outside of the array's.

asciilifeform: currently seems to me that ~all~ of the possible variants, are similarly ugly

asciilifeform: this is not equiv to cursor behaviour in text editors, though. there, cursor always is pointing to a valid fillable cell

asciilifeform: so what would empty stack look like , in this variant ?

asciilifeform: apeloyee: afaik it isn't possible to make types 'with hole'

asciilifeform: there's an explicit range test construct, btw

asciilifeform: ( at the very least, if range checks are enabled for ffacalc )

asciilifeform: and abolish need to want()

asciilifeform: well it'd turn a pop from empty stack into a range-dipping eggog instantly

asciilifeform: then to refer to current, would be 'SP - 1' rather than 'SP'

asciilifeform: hmm, what if one were to model SP as in apeloyee's analogy, the text editor cursor. i.e. the pos of the ~next~ valid stack cell, rather than 'current'.

asciilifeform: this is true. but 1) ugly 2) possibly will get in the way of sparkism, later; it relies on type ranges for good chunk of the proofolade

asciilifeform: one way i considered doing this, is to do away with all such things as 'SP - 1', 'SP - 2', etc. and instead to have e.g. Get_Stack_First, Get_Stack_Second, etc., each of which individually would ensure that the desired element exists. but these would have to return 'access type' (pointers) which thus far i've avoided using .

asciilifeform: i'd like to resolve the apparent contradiction between 'all possible SP positions are valid dereferences' and 'stack can be empty'.

asciilifeform: ideally there would be some way to trap any reference to the zero cell, or , failing that, to prove that the zero cell cannot end up referenced.

asciilifeform: apeloyee: a long-term goal is to have the whole proggy bulletproof even after building under '-gnatp' ('disable all range checks'). relying on the range check of Stack , vs SP's range, does not go well with this

asciilifeform: i.e. in all cases where the array has a custom indexing type as the index, the array exists over the entire range of said type.

asciilifeform: apeloyee: i dunget why absurd ? my other arrays behave this way.

asciilifeform: BingoBoingo: hey they only nao plugged it back in

asciilifeform: can you think of a way to have the range of SP and of Stack be the same, but to still represent concept of 'empty' ?

asciilifeform: i'm still curious re the SP tho

asciilifeform: aha. ty apeloyee , for taking the sweat to do this.

asciilifeform: this is the #1 type of stylistic fix that i look for -- 'can this be made more obviously-correct-when-used-as-prescribed' and 'can use-as-prescribed be made more obvious'

asciilifeform: proggy ought to be written in such a way that the reader can ~see~ that it is correct.

asciilifeform: possibly one can make a SPARKistic proof of non-aliasing , for proggy taken as a whole. i'ma look into it.

asciilifeform: and afaik gnat does not know how to prevent aliasing in the general case, but only in a few specific situations ( array copies )

asciilifeform: No_Implicit_Conditionals is working as described on the box : https://docs.adacore.com/gnathie_ug-docs/html/gnathie_ug/gnathie_ug/using_gnat_pro_features_relevant_to_high_integrity.html#controlling-implicit-conditionals-and-loops

asciilifeform: ( observe , they are still present in the disasm )

asciilifeform: ( they don't appear in the code, but they exist )

asciilifeform: right, e.g. the range checks

asciilifeform: ffa itself is a sort of tightrope walk, an attempt to 'и рыбку съесть и нахуй сесть' . it isn't actually possible to make all of the routines able to take every conceivable kind of compile-time abuse ( which i'd argue overlap of arguments, is ) without conditional jumps.

asciilifeform: in the general case.

asciilifeform: afaik it isn't actually possible to write overlap-safe routines without implicit (or otherwise) branches

asciilifeform: the 1 caveat re buffers, is that there is a practical limit as to what can be made anticlobbering: if i were to do it to items that occur in inner loops of O(n^3)istic items, e.g. mux, proggy will end up 'geological' 4ever.

asciilifeform: this is a bit of a downer, i confess that i hoped apeloyee had found a more subtle, lethal boojum.

asciilifeform: the cost is small in comparison with the mod-exping per se

asciilifeform: but i can't help but agree with apeloyee re the Product in FZ_Mod_Exp , it gotta be buffered.

asciilifeform: because there isn't actually a limit as to what less-clueful people can break, regardless of what i do

asciilifeform: has apeloyee found a specific instance where it can be made to eggog ? or is this a hypothetical 'once less clueful people start changing things' observation ? ☟︎

asciilifeform: used extensively ? where, other than the stack ops ?

asciilifeform: i never proclaimed, fwiw, that all ffa routines must be able to cleanly walk over own inputs.

asciilifeform: though it is a waste of space and time.

asciilifeform: prolly FZ_Mod_Exp oughta accumulate Product in a temp, and shit it out in 1shot in the end, like FZ_Mod_Mul.

asciilifeform: it is not my place to make every possible mutilation of the program, safe. ( and is quite impossible )

asciilifeform: could just as easily not, with temp buffer. but why.