JRahm
Admin
Admin% set ip "10.10.11.70"
10.10.11.70
% scan $ip {%d.%d.%d.%d} a b c d
4
% set srcsnat "2001:111:111:22:[format %02x $a][format %02x $b]:[format %02x $c][format %02x $d]::"
2001:111:111:22:0a0a:0b46::
The leading 0's are in there, which isn't exactly what you wanted, but best to leave for IP octets that don't fit nicely in a single character.