Zickzack-Chiffre

Anleitung

Implementiere die Verschlüsselung und Entschlüsselung der Rail-Fence-Chiffre.

Die Rail-Fence-Chiffre ist eine Form der Transpositionschiffre, deren Name sich davon ableitet, wie verschlüsselt wird. Bereits die alten Griechen nutzten sie.

Bei der Rail-Fence-Chiffre wird die Nachricht abwärts auf aufeinanderfolgende „Schienen“ eines gedachten Zauns geschrieben und bewegt sich, unten angekommen, wieder nach oben (wie im Zickzack). Zum Schluss wird die Nachricht zeilenweise ausgelesen.

Zum Beispiel schreibt der Verschlüsseler mit drei „Schienen“ und der Nachricht „WE ARE DISCOVERED FLEE AT ONCE“ Folgendes auf:

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .

Dann liest er ab:

WECRLTEERDSOEEFEAOCAIVDEN

Um eine Nachricht zu entschlüsseln, nimmst du die Zickzack-Form und füllst den Geheimtext entlang der Zeilen.

? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

Die erste Zeile hat sieben Plätze, die mit „WECRLTE“ gefüllt werden können.

W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

Jetzt nimmt die 2. Zeile „ERDSOEEFEAOC“ auf.

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

Für die letzte Zeile bleibt „AIVDEN“ übrig.

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .

Wenn du jetzt entlang der Zickzack-Form liest, kannst du die ursprüngliche Nachricht lesen.

Subtypen

Diese Übung definiert einen Subtype namens Positive für alle natürlichen Zahlen, die größer als 0 sind. Einen Subtype kannst du dir als ein Paar ⟨x, h⟩ vorstellen, wobei x der Wert und h der Beweis seiner Gültigkeit ist.

Auf den Wert in einem Subtype (in diesem Fall x) kannst du mit .val zugreifen, zum Beispiel mit x.val. Auf seinen Beweis kannst du mit .property zugreifen, zum Beispiel mit x.property. Auf beide kannst du wie gewohnt auch per Pattern Matching zugreifen.

Um einen Wert für einen Subtype zu konstruieren, musst du seine Gültigkeit beweisen, in diesem Fall, dass die Zahl größer als 0 ist.

Es gibt eine Reihe von Lemmata und Theoremen in Lean, die als Ausgangspunkt für diesen Beweis dienen können. Zum Beispiel ist Nat.zero_lt_succ ein Lemma, das besagt, dass für jede natürliche Zahl n gilt: 0 < n + 1.

---

Quelle

Wikipedia