Gimli is a 384-bit permutation that makes use of an internal 96-bit permutation which works on columns. Every 4 rounds starting from the 1st a "small swap" is performed and every 4 rounds starting from the 3rd round a "big swap" is performed, these work on the first 32-bits of each column (see https://gimli.cr.yp.to/linear.png)
The Chacha20 permutation is a 512-bit permutation with an internal 128-bit permutation which works on rows every odd round and diagonally every even round.
If we assume that the internal permutation of each algorithm is absolutely random, would the whole design be considered provably safe? What kind of safety margin does each design allow for? For example, would chacha20 with a random 128-bit internal permutation be just as secure as a 512-bit random permutation, and would Gimli with a random 96-bit internal permutation be just as secure as a 384-bit random permutation? If neither of the above designs is provably safe, is there something else that offers a provably secure way of constructing a bigger permutation out of a smaller one?