Vertragsgestaltung durch Vertrag -> Korrektheit und maximaler Gasverbrauch

Diese Frage ist eine allgemeine Designfrage, die sich auf die Vertragskorrektheit bezieht , und die hier aufgeführten Funktionen sind nur Beispiele.

Während ich auf Ethereum entwickle, wird mir klar, dass es relativ einfach sein kann, einen Vertrag falsch zu gestalten, der sich selbst blockiert, weil notwendige Schlüsselfunktionen plötzlich nicht mehr aufrufbar sind, weil ihre Ausführung plötzlich das Gaslimit überschreitet.

Das führt mich zu der wahrscheinlich schwierigen Frage:

Wie kann ich behaupten , dass eine bestimmte Funktion nie mehr als eine bestimmte Menge Gas verbraucht? Dies scheint eine entscheidende Notwendigkeit für die Vertragskorrektheit zu sein.

Zum Beispiel

function unbound() returns (uint256) {
    uint256 total = 0;
    for (uint i=0; i < users.length; i++) {
        total+= users[i].value;
    }
    return total;
}

Das Aufrufen dieser Funktion hat undeterministische Gaskosten und könnte irgendwann leicht nicht mehr aufrufbar werden. Natürlich ist es in einem so einfachen Beispiel wie diesem einfach, diese Summe umzugestalten und nicht in einer Schleife, sondern auf andere Weise zu berechnen. Aber Schleifen lassen sich nicht immer vermeiden. Die Frage ist, wie schreibt man in diesem Fall korrekte Funktionen?

Beispielsweise könnte das System so konzipiert sein, dass es nie mehr als 6 Benutzer gibt. In diesem Fall ist die Schleife gebunden und die Ausführungskosten deterministisch. Wenn ich also Folgendes habe:

function bound() returns (uint256) {
    uint256 total = 0;
    assert(users.length < 6);
    for (uint i=0; i < users.length; i++) {
        total+= users[i].value;
    }
    return total;
}

Diese Funktion verwendet eine Schleife, hat aber eine deterministische Obergrenze für den Gasverbrauch.

A: Wie kann ich die maximale Gasmenge berechnen, die beim Aufrufen dieser Funktion verbraucht wird?

B: Wie kann ich dieses Maximum den Kunden der Funktion mitteilen?

Kann ich sowas irgendwie machen:

function bound() returns (uint256) {
    uint256 total = 0;
    for (uint i=0; i < users.length; i++) {
        total+= users[i].value;
    }
    assert(gasConsumend < 1234);
    return total;
}

?

Schließlich schreiben wir Verträge, und Vor- und Nachbedingungen sind ein integraler Bestandteil von Design by Contract . Wir können Vorbedingungen mit require() und Nachbedingungen mit assert() schreiben - aber für die Korrektheit auf Ethereum scheint es auch notwendig zu sein, einen maximalen Gasverbrauch anzugeben. Wie?