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: 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: apeloyee: well yes, i get it. but i DON'T LIKE it.
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: 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: thing is, a sparkism is not a substitute for a 'fits-in-head'-correct routine.
asciilifeform: possibly one can make a SPARKistic proof of non-aliasing , for proggy taken as a whole. i'ma look into it.
asciilifeform: but afaik no such item exists , even in '2012'
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: partially ( for array copies ) . but it gets nuked by No_Implicit_Conditionals.
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: apeloyee still wins 'most attentive eagle eye' award.
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.
asciilifeform: apeloyee: let's hear the answer to the riddle ?
asciilifeform: the proper way to enforce 'no access to Stack(0)' would be to constrain Stack_Positions to 1 .. Height. but this leaves no way to represent an empty stack.
