Κρυπτογράφημα Rail Fence

Οδηγίες

Υλοποίησε την κωδικοποίηση και την αποκωδικοποίηση για τον κρυπτογράφο Rail Fence.

Ο κρυπτογράφος Rail Fence είναι μια μορφή κρυπτογράφου μετάθεσης, που πήρε το όνομά του από τον τρόπο με τον οποίο γίνεται η κωδικοποίηση. Τον χρησιμοποιούσαν ήδη οι αρχαίοι Έλληνες.

Στον κρυπτογράφο Rail Fence, το μήνυμα γράφεται προς τα κάτω σε διαδοχικές "ράγες" ενός φανταστικού φράχτη και μετά κινείται προς τα πάνω όταν φτάνουμε στον πάτο (σαν ζιγκ-ζαγκ). Τέλος, το μήνυμα διαβάζεται κατά σειρές.

Για παράδειγμα, χρησιμοποιώντας τρεις "ράγες" και το μήνυμα "WE ARE DISCOVERED FLEE AT ONCE", όποιος κρυπτογραφεί γράφει:

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 . .

Στη συνέχεια διαβάζει:

WECRLTEERDSOEEFEAOCAIVDEN

Για να αποκρυπτογραφήσεις ένα μήνυμα, παίρνεις το σχήμα του ζιγκ-ζαγκ και γεμίζεις το κρυπτοκείμενο κατά μήκος των σειρών.

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

Η πρώτη σειρά έχει επτά θέσεις που μπορούν να γεμίσουν με "WECRLTE".

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

Τώρα η δεύτερη σειρά παίρνει "ERDSOEEFEAOC".

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

Αφήνοντας το "AIVDEN" για την τελευταία σειρά.

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 . .

Αν τώρα διαβάσεις κατά μήκος του σχήματος του ζιγκ-ζαγκ, μπορείς να διαβάσεις το αρχικό μήνυμα.

Υποτύποι

Αυτή η άσκηση ορίζει έναν υποτύπο που ονομάζεται Positive, για όλους τους φυσικούς αριθμούς μεγαλύτερους του 0. Ένας υποτύπος μπορεί να θεωρηθεί ως ένα ζεύγος ⟨x, h⟩, όπου x είναι η τιμή και h είναι η απόδειξη της εγκυρότητάς της.

Μπορείς να αποκτήσεις πρόσβαση στην τιμή μέσα σε έναν υποτύπο (x, στην περίπτωση αυτή) χρησιμοποιώντας .val, για παράδειγμα, x.val. Μπορείς να αποκτήσεις πρόσβαση στην απόδειξή του χρησιμοποιώντας .property, για παράδειγμα, x.property. Μπορείς επίσης να αποκτήσεις πρόσβαση και στα δύο μέσω αντιστοίχισης προτύπων, όπως συνήθως.

Για να κατασκευάσεις μια τιμή για έναν υποτύπο, είναι απαραίτητο να αποδείξεις την εγκυρότητά της, στην περίπτωση αυτή, ότι ο αριθμός είναι μεγαλύτερος του 0.

Υπάρχουν αρκετά λήμματα και θεωρήματα στη Lean που μπορούν να χρησιμεύσουν ως σημείο εκκίνησης γι' αυτή την απόδειξη. Για παράδειγμα, το Nat.zero_lt_succ είναι ένα λήμμα που δηλώνει ότι για κάθε φυσικό αριθμό n: 0 < n + 1.

---

Πηγή

Wikipedia